Refereed Journal, Conference and Workshop Publications
[1]
|
Jonathan Chan and Stephanie Weirich.
Stratified Type Theory.
In Viktor Vafeiadis, editor, European Symposium on Programming
Languages and Systems, ESOP 2025, May 2025.
To Appear.
|
[2]
|
Cassia Torczon, Emmanuel Suárez Acevedo, Shubh Agrawal, Joey
Velez-Ginorio, and Stephanie Weirich.
Effects and Coeffects in Call-By-Push-Value.
Proc. ACM Program. Lang., 8(OOPSLA), October 2024.
To Appear.
|
[3]
|
Li-Yao Xia, Laura Israel, Maite Kramarz, Nathan Coltharp, Koen Claessen,
Stephanie Weirich, and Yao Li.
Story of Your Lazy Function's Life: A Bidirectional Demand
Semantics for Mechanized Cost Analysis of Lazy Programs.
Proc. ACM Program. Lang., 8(ICFP), August 2024.
[ DOI
PDF ]
Lazy evaluation is a powerful tool that enables better
compositionality and potentially better performance in
functional programming, but it is challenging to analyze its
computation cost. Existing works either require manually
annotating sharing, or rely on separation logic to reason
about heaps of mutable cells. In this paper, we propose a
bidirectional demand semantics that allows for extrinsic
reasoning about the computation cost of lazy programs
without relying on special program logics. To show the
effectiveness of our approach, we apply the demand semantics
to a variety of case studies including insertion sort,
selection sort, Okasaki’s banker’s queue, and the implicit
queue. We formally prove that the banker’s queue and the
implicit queue are both amortized and persistent using the
Rocq Prover (formerly known as Coq). We also propose the
reverse physicist’s method, a novel variant of the classical
physicist’s method, which enables mechanized, modular and
compositional reasoning about amortization and persistence
with the demand semantics.
Keywords: formal verification, computation cost, lazy evaluation, amortized analysis
|
[4]
|
Yiyun Liu, Jonathan Chan, Jessica Shi, and Stephanie Weirich.
Internalizing Indistinguishability with Dependent Types.
Proc. ACM Program. Lang., 8(POPL), January 2024.
[ DOI
PDF ]
In type systems with dependency tracking, programmers can assign
an ordered set of levels to computations and prevent
information flow from high-level computations to the
low-level ones. The key notion in such systems is
indistinguishability: a definition of program equivalence
that takes into account the parts of the program that an
observer may depend on. In this paper, we investigate the
use of dependency tracking in the context of
dependently-typed languages. We present the Dependent
Calculus of Indistinguishability (DCOI), a system that
adopts indistinguishability as the definition of equality
used by the type checker. DCOI also internalizes that
relation as an observer-indexed propositional equality type,
so that programmers may reason about indistinguishability
within the language. Our design generalizes and extends
prior systems that combine dependency tracking with
dependent types and is the first to support conversion and
propositional equality at arbitrary observer levels. We have
proven type soundness and noninterference theorems for DCOI
and have developed a prototype implementation of its type
checker.
Keywords: Coq, Dependent Types, Formalization, Modes
|
[5]
|
Yiyun Liu and Stephanie Weirich.
Dependently-Typed Programming with Logical Equality Reflection.
Proc. ACM Program. Lang., 7(ICFP), August 2023.
[ DOI
PDF ]
In dependently-typed functional programming languages that
allow general recursion, programs used as proofs must be
evaluated to retain type soundness. As a result, programmers
must make a trade-off between performance and safety. To
address this problem, we propose System DE, an
explicitly-typed, moded core calculus that supports
termination tracking and equality reflection. Programmers
can write inductive proofs about potentially diverging
programs in a logical sublanguage and reflect those proofs
to the type checker, while knowing that such proofs will be
erased by the compiler before execution. A key feature of
System DE is its use of modes for both termination and
relevance tracking, which not only simplifies the design but
also leaves it open for future extension. System DE is
suitable for use in the Glasgow Haskell Compiler, but could
serve as the basis for any general purpose dependently-typed
language.
Keywords: Modes, Equality Reflection, Haskell, Dependent Types
|
[6]
|
Yao Li and Stephanie Weirich.
Program Adverbs and Tlön Embeddings.
Proc. ACM Program. Lang., 6(ICFP), September 2022.
Distinguished Paper Award. Artifact available.
[ DOI
PDF ]
Free monads (and their variants) have become a popular
general-purpose tool for representing the semantics of
effectful programs in proof assistants. These data
structures support the compositional definition of semantics
parameterized by uninterpreted events, while admitting a
rich equational theory of equivalence. But monads are not
the only way to structure effectful computation, why should
we limit ourselves? In this paper, inspired by applicative
functors, selective functors, and other structures, we
define a collection of data structures and theories, which
we call program adverbs, that capture a variety of
computational patterns. Program adverbs are themselves
composable, allowing them to be used to specify the
semantics of languages with multiple computation
patterns. We use program adverbs as the basis for a new
class of semantic embeddings called Tlön
embeddings. Compared with embeddings based on free monads,
Tlön embeddings allow more flexibility in computational
modeling of effects, while retaining more information about
the program’s syntactic structure.
|
[7]
|
Pritam Choudhury, Harley Eades III, and Stephanie Weirich.
A Dependent Dependency Calculus.
In Ilya Sergey, editor, Programming Languages and Systems, ESOP
2022, volume 13240 of Lecture Notes in Computer Science, pages
403--430, Cham, 2022. Springer International Publishing.
Artifact available.
[ DOI
http ]
Over twenty years ago, Abadi et al. established the Dependency
Core Calculus (DCC) as a general purpose framework for
analyzing dependency in typed programming languages. Since
then, dependency analysis has shown many practical benefits
to language design: its results can help users and compilers
enforce security constraints, eliminate dead code, among
other applications. In this work, we present a Dependent
Dependency Calculus (DDC), which extends this general idea
to the setting of a dependently-typed language. We use this
calculus to track both run-time and compile-time
irrelevance, enabling faster type-checking and program
execution.
|
[8]
|
Yao Li, Li-yao Xia, and Stephanie Weirich.
Reasoning about the garden of forking paths.
Proc. ACM Program. Lang., 5(ICFP), August 2021.
[ DOI
PDF ]
Lazy evaluation is a powerful tool for functional
programmers. It enables the concise expression of on-demand
computation and a form of compositionality not available
under other evaluation strategies. However, the stateful
nature of lazy evaluation makes it hard to analyze a
program’s computational cost, either informally or
formally. In this work, we present a novel and simple
framework for formally reasoning about lazy computation
costs based on a recent model of lazy evaluation:
clairvoyant call-by-value. The key feature of our framework
is its simplicity, as expressed by our definition of the
clairvoyance monad. This monad is both simple to define
(around 20 lines of Coq) and simple to reason about. We show
that this monad can be effectively used to mechanically
reason about the computational cost of lazy functional
programs written in Coq.
|
[9]
|
Richard A. Eisenberg, Guillaume Duboc, Stephanie Weirich, and Daniel Lee.
An Existential Crisis Resolved: Type inference for first-class
existential types.
Proc. ACM Program. Lang., 5(ICFP), August 2021.
Distinguished Paper Award.
[ DOI
PDF ]
Despite the great success of inferring and programming with universal types, their dual—existential types—are much harder to work with. Existential types are useful in building abstract types, working with indexed types, and providing first-class support for refinement types. This paper, set in the context of Haskell, presents a bidirectional type-inference algorithm that infers where to introduce and eliminate existentials without any annotations in terms, along with an explicitly typed, type-safe core language usable as a compilation target. This approach is backward compatible. The key ingredient is to use strong existentials, which support (lazily) projecting out the encapsulated data, not weak existentials accessible only by pattern-matching.
|
[10]
|
Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John
Wiegley, Joshua Cohen, and Stephanie Weirich.
Ready, Set, Verify! Applying Hs-to-coq to Real-world Haskell
Code.
Journal of Functional Programming, 31:1--40, February 2021.
[ DOI
.pdf ]
|
[11]
|
Pritam Choudhury, Harley D. Eades III, Richard A. Eisenberg, and Stephanie
Weirich.
A Graded Dependent Type System with a Usage-Aware Semantics.
Proc. ACM Program. Lang., 5(POPL), January 2021.
Artifact available.
[ DOI
http ]
|
[12]
|
Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, and Stephanie Weirich.
Eta-equivalence in Core Dependent Haskell.
In Marc Bezem and Assia Mahboubi, editors, Post-proceedings of
the 25th International Conference on Types for Proofs and Programs (TYPES
2019), volume 175 of Leibniz International Proceedings in Informatics,
pages 7:1--7:32, Dagstuhl, Germany, sep 2020. Schloss Dagstuhl -
Leibniz-Zentrum für Informatik.
[ DOI
http ]
|
[13]
|
Stephanie Weirich, Pritam Choudhury, Antoine Voizard, and Richard Eisenberg.
A Role for Dependent Types in Haskell.
Proc. ACM Program. Lang., 3(ICFP), 2019.
[ DOI
.pdf ]
|
[14]
|
Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John
Wiegley, and Stephanie Weirich.
Ready, Set, Verify! Applying Hs-to-coq to Real-world Haskell
Code (Experience Report).
Proc. ACM Program. Lang., 2(ICFP):89:1--89:16, July 2018.
Artifact Available.
[ DOI
http ]
Keywords: Coq, Haskell, verification
|
[15]
|
Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and Stephanie
Weirich.
Total Haskell is Reasonable Coq.
In Proceedings of 7th ACM SIGPLAN International Conference on
Certified Programs and Proofs (CPP'18). ACM, 2018.
New York, NY, USA.
[ DOI
PDF ]
|
[16]
|
Stephanie Weirich, Antoine Voizard, Pedro Henrique Avezedo de Amorim, and
Richard A. Eisenberg.
A Specification for Dependent Types in Haskell.
Proc. ACM Program. Lang., 1(ICFP):31:1--31:29, August 2017.
Artifact evaluated as "Available" and Reusable".
[ DOI
http ]
Keywords: Dependent Types, Haskell
|
[17]
|
Andrew W. Appel, Lennart Beringer, Adam Chlipala, Benjamin C. Pierce, Zhong
Shao, Stephanie Weirich, and Steve Zdancewic.
Position paper: the science of deep specification.
Philosophical Transactions of the Royal Society of London A:
Mathematical, Physical and Engineering Sciences, 375(2104), 2017.
[ DOI
arXiv
http ]
We introduce our efforts within the project The science of deep specification to work out the key formal underpinnings of industrial-scale formal specifications of software and hardware components, anticipating a world where large verified systems are routinely built out of smaller verified components that are also used by many other projects. We identify an important class of specification that has already been used in a few experiments that connect strong component-correctness theorems across the work of different teams. To help popularize the unique advantages of that style, we dub it deep specification, and we say that it encompasses specifications that are rich, two-sided, formal and live (terms that we define in the article). Our core team is developing a proof-of-concept system (based on the Coq proof assistant) whose specification and verification work is divided across largely decoupled subteams at our four institutions, encompassing hardware microarchitecture, compilers, operating systems and applications, along with cross-cutting principles and tools for effective specification. We also aim to catalyse interest in the approach, not just by basic researchers but also by users in industry.This article is part of the themed issue Verified trustworthy software systems.
|
[18]
|
Richard A. Eisenberg, Stephanie Weirich, and Hamidhasan G. Ahmed.
Visible Type Application.
In European Symposium on Programming (ESOP), pages 229--254,
April 2016.
[ DOI
PDF ]
|
[19]
|
Steven Keuchel, Stephanie Weirich, and Thomas Tom Schrijvers.
Needle and Knot: Binder Boilerplate Tied Up.
In European Symposium on Programming (ESOP), pages 419--445,
April 2016.
[ DOI ]
|
[20]
|
Simon Peyton Jones, Stephanie Weirich, Richard A. Eisenberg, and Dimitrios
Vytiniotis.
A Reflection on Types.
In Sam Lindley, Conor McBride, Phil Trinder, and Don Sannella,
editors, WadlerFest 2016: A list of successes that can change the
world, LNCS, pages 292--317. Springer, 2016.
[ DOI
PDF ]
|
[21]
|
Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie
Weirich.
Safe zero-cost coercions for Haskell.
Journal of Functional Programming, 26, 2016.
[ DOI
PDF
http ]
AbstractGenerative type abstractions – present in Haskell, OCaml, and other languages – are useful concepts to help prevent programmer errors. They serve to create new types that are distinct at compile time but share a run-time representation with some base type. We present a new mechanism that allows for zero-cost conversions between generative type abstractions and their representations, even when such types are deeply nested. We prove type safety in the presence of these conversions and have implemented our work in GHC.
|
[22]
|
Vilhelm Sjöberg and Stephanie Weirich.
Programming up to Congruence.
In POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages, pages 369--382, Mumbai, India, January 2015.
Artifact Evaluated.
[ DOI
PDF ]
|
[23]
|
Wenrui Meng, Junkil Park, Oleg Sokolsky, Stephanie Weirich, and Insup Lee.
Verified ROS-Based Deployment of Platform-Independent Control
Systems.
In Seventh NASA Formal Methods Symposium, pages 248--262,
Pasadena, CA, 2015.
[ PDF ]
|
[24]
|
Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich.
Combining Proofs and Programs in a Dependently Typed Language.
In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL '14, page 33–45, New York, NY,
USA, 2014. Association for Computing Machinery.
[ DOI
.pdf ]
Most dependently-typed programming languages either require that all expressions terminate (e.g. Coq, Agda, and Epigram), or allow infinite loops but are inconsistent when viewed as logics (e.g. Haskell, ATS, Ωmega. Here, we combine these two approaches into a single dependently-typed core language. The language is composed of two fragments that share a common syntax and overlapping semantics: a logic that guarantees total correctness, and a call-by-value programming language that guarantees type safety but not termination. The two fragments may interact: logical expressions may be used as programs; the logic may soundly reason about potentially nonterminating programs; programs can require logical proofs as arguments; and "mobile" program values, including proofs computed at runtime, may be used as evidence by the logic. This language allows programmers to work with total and partial functions uniformly, providing a smooth path from functional programming to dependently-typed programming.
Keywords: termination, dependent types, general recursion
|
[25]
|
Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, and Stephanie
Weirich.
Closed type families with overlapping equations.
In POPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages, pages 671--683, San Diego, CA, USA, January 2014.
[ PDF ]
|
[26]
|
Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie
Weirich.
Safe Zero-Cost Coercions for Haskell.
In Proceedings of the 19th ACM SIGPLAN International Conference
on Functional Programming, ICFP '14, page 189–202, New York, NY, USA,
2014. Association for Computing Machinery.
[ DOI
http ]
Generative type abstractions -- present in Haskell, OCaml, and other languages -- are useful concepts to help prevent programmer errors. They serve to create new types that are distinct at compile time but share a run-time representation with some base type. We present a new mechanism that allows for zero-cost conversions between generative type abstractions and their representations, even when such types are deeply nested. We prove type safety in the presence of these conversions and have implemented our work in GHC.
Keywords: type class, coercion, newtype deriving, haskell
|
[27]
|
Garrin Kimmel, Aaron Stump, Harley D. Eades, Peng Fu, Tim Sheard, Stephanie
Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathin Collins, and Ki Yunh
Anh.
Equational reasoning about programs with general recursion and
call-by-value semantics.
Progress in Informatics, (10):19--48, March 2013.
[ http ]
|
[28]
|
Zhengjiang Hu, Shin-Cheng Mu, and Stephanie Weirich.
Guest Editorial: Advanced programming techniques for
construction of robust, generic and evolutionary programs.
Progress in Informatics, (10):1--2, March 2013.
[ DOI
http ]
|
[29]
|
Miroslav Pajic, Nicola Bezzo, James Weimer, Rajeev Alur, Rahul Mangharam,
Nathan Michael, George J. Pappas, Oleg Sokolsky, Paulo Tabuada, Stephanie
Weirich, and Insup Lee.
Towards synthesis of platform-aware attack-resilient control
systems: extended abstract.
In HiCoNS '13: Proceedings of the 2nd ACM international
conference on High confidence networked systems, pages 75--76, New York, NY,
USA, 2013.
|
[30]
|
Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg.
System FC with Explicit Kind Equality.
In Proceedings of the 18th ACM SIGPLAN International Conference
on Functional Programming, ICFP '13, page 275–286, New York, NY, USA,
2013. Association for Computing Machinery.
[ DOI
PDF
http ]
System FC, the core language of the Glasgow Haskell Compiler, is an explicitly-typed variant of System F with first-class type equality proofs called coercions. This extensible proof system forms the foundation for type system extensions such as type families (type-level functions) and Generalized Algebraic Datatypes (GADTs). Such features, in conjunction with kind polymorphism and datatype promotion, support expressive compile-time reasoning.However, the core language lacks explicit kind equality proofs. As a result, type-level computation does not have access to kind-level functions or promoted GADTs, the type-level analogues to expression-level features that have been so useful. In this paper, we eliminate such discrepancies by introducing kind equalities to System FC. Our approach is based on dependent type systems with heterogeneous equality and the "Type-in-Type" axiom, yet it preserves the metatheoretic properties of FC. In particular, type checking is simple, decidable and syntax directed. We prove the preservation and progress theorems for the extended language.
Keywords: equality, dependent types, haskell
|
[31]
|
Richard A. Eisenberg and Stephanie Weirich.
Dependently typed programming with singletons.
In Haskell Symposium, pages 117--130, Copenhagen, Denmark,
September 2012.
[ PDF ]
|
[32]
|
Michael Greenberg, Benjamin C. Pierce, and Stephanie Weirich.
Contracts made manifest.
Journal of Functional Programming, 22(3):225--274, May 2012.
|
[33]
|
Stephanie Weirich and Chris Casinghino.
Generic Programming with Dependent Types.
In Jeremy Gibbons, editor, Generic and Indexed Programming,
number 7470 in Lecture Notes in Computer Science, pages 217--258.
Springer-Verlag Berlin Heidelberg, 2012.
[ PDF ]
|
[34]
|
Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones,
Dimitrios Vytiniotis, and José Pedro Magalhaes.
Giving Haskell A Promotion.
In Seventh ACM SIGPLAN Workshop on Types in Language Design and
Implementation (TLDI '12), pages 53--66, 2012.
[ PDF ]
|
[35]
|
Garrin Kimmell, Aaron Stump, Harley D. Eades III, Peng Fu, Tim Sheard,
Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathan Collins, and
Ki Yung Ahn.
Equational Reasoning about Programs with General Recursion and
Call-by-value Semantics.
In Sixth ACM SIGPLAN Workshop Programming Languages meets
Program Verification (PLPV '12), pages 15--26, 2012.
[ PDF ]
|
[36]
|
Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley
D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, and Stephanie
Weirich.
Irrelevance, Heterogenous Equality, and Call-by-value Dependent
Type Systems.
In Fourth workshop on Mathematically Structured Functional
Programming (MSFP '12), pages 112--162, 2012.
[ PDF ]
|
[37]
|
Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich.
Step-Indexed Normalization for a Language with General
Recursion.
In Fourth workshop on Mathematically Structured Functional
Programming (MSFP '12), pages 25--39, 2012.
[ PDF ]
|
[38]
|
Umut A. Acar, James Cheney, and Stephanie Weirich.
Editorial - Special issue dedicated to ICFP 2010.
J. Funct. Program., 22(4-5):379--381, 2012.
[ DOI ]
|
[39]
|
Benjamin C. Pierce and Stephanie Weirich.
Preface to Special Issue on the POPLMark Challenge.
J. Autom. Reasoning, 49(3):301--302, 2012.
|
[40]
|
Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, and Steve
Zdancewic.
Generative Type Abstraction and Type-level Computation.
In POPL 11: 38th ACM SIGACT-SIGPLAN Symposium on Principles of
Programming Languages, January 26--28, 2011. Austin, TX, USA., pages
227--240, January 2011.
[ PDF ]
Modular languages support generative type abstraction,
ensuring that an abstract type is distinct from its
representation, except inside the implementation where the
two are synonymous. We show that this well-established
feature is in tension with the non-parametric features
of newer type systems, such as indexed type families and GADTs.
In this paper we solve the problem by using kinds to
distinguish between parametric and non-parametric contexts.
The result is directly applicable to Haskell, which is rapidly
developing support for type-level computation, but the same
issues should arise whenever generativity and non-parametric features
are combined.
|
[41]
|
Stephanie Weirich, Brent A. Yorgey, and Tim Sheard.
Binders Unbound.
In Proceeding of the 16th ACM SIGPLAN International Conference
on Functional Programming, ICFP '11, pages 333--345, New York, NY, USA,
2011.
[ PDF ]
Keywords: generic programming, haskell, name binding, patterns
|
[42]
|
Tim Sheard, Aaron Stump, and Stephanie Weirich.
Language-Based Verification Will Change The World.
In 2010 FSE/SDP Workshop on the Future of Software Engineering
Research, pages 343--348, November 2010.
Position paper.
[ PDF ]
|
[43]
|
Aaron Stump, Vilhelm Sjöberg, and Stephanie Weirich.
Termination Casts: A Flexible Approach to Termination with
General Recursion.
In Workshop on Partiality and Recursion in Interactive Theorem
Provers, pages 76--93, Edinburgh, Scotland, July 2010.
[ PDF ]
This paper proposes a type-and-effect system that
distinguishes terminating terms and total functions from possibly
diverging terms and partial functions, for a lambda calculus with
general recursion and equality types. The central idea is to include
a primitive type-form “Terminates t”, expressing that term t is
terminating; and then allow terms t to be coerced from possibly
diverging to total, using a proof of Terminates t. We call such
coercions termination casts, and show how to implement
terminating recursion using them. For the meta-theory of the system,
we describe a translation from this system to a logical theory of
termination for general recursive, simply typed functions. Every
typing judgment of this system is translated to a theorem expressing the
appropriate termination property of the computational part of the
term.
|
[44]
|
Dimitrios Vytiniotis and Stephanie Weirich.
Parametricity, Type Equality and Higher-order Polymorphism.
Journal of Functional Programming, 20(2):175--210, March 2010.
[ PDF ]
Propositions that express type equality are a frequent ingredient of
modern functional programming---they can encode generic
functions, dynamic types, and GADTs. Via the Curry-Howard
correspondence, these propositions are ordinary types
inhabited by proof terms, computed using runtime type
representations. In this paper we show that two examples of type
equality propositions actually do reflect type equality; they are
only inhabited when their arguments are equal and their proofs are
unique (up to contextual equivalence.) We show this result in the
context of a strongly normalizing language with higher-order
polymorphism and primitive recursion over runtime type
representations by proving Reynolds's abstraction theorem. We then
use this theorem to derive “free” theorems about equality types.
|
[45]
|
Stephanie Weirich and Chris Casinghino.
Arity-generic type-generic programming.
In ACM SIGPLAN Workshop on Programming Languages Meets Program
Verification (PLPV), pages 15--26, January 2010.
[ PDF ]
|
[46]
|
Limin Jia, Jianzhou Zhao, Vilhem Sjöberg, and Stephanie Weirich.
Dependent types and Program Equivalence.
In 37th ACM SIGACT-SIGPLAN Symposium on Principles of
Programming Languages (POPL), pages 275--286, Madrid, Spain, January 2010.
[ PDF ]
The definition of type equivalence is one of the most important design
issues for any typed language. In dependently-typed languages, because
terms appear in types, this definition must rely on a definition of
term equivalence. In that case, decidability of type checking requires
decidability for the term equivalence relation.
Almost all dependently-typed languages require this relation to be
decidable. Some, such as Coq, Epigram or Agda, do so by employing
analyses to force all programs to terminate. Conversely, others, such
as DML, ATS, Omega, or Haskell, allow nonterminating computation, but
do not allow those terms to appear in types. Instead, they identify a
terminating index language and use singleton types to connect indices
to computation. In both cases, decidable type checking comes at a
cost, in terms of complexity and expressiveness.
Conversely, the benefits to be gained by decidable type checking are
modest. Termination analyses allow dependently typed programs to
verify total correctness properties. However, decidable type checking
is not a prerequisite for type safety. Furthermore, decidability does
not imply tractability. A decidable approximation of program
equivalence may not be useful in practice.
Therefore, we take a different approach: instead of a fixed notion for
term equi valence, we parameterize our type system with an abstract
relation that is not n ecessarily decidable. We then design a novel
set of typing rules that require on ly weak properties of this
abstract relation in the proof of the preservation an d progress
lemmas. This design provides flexibility: we compare valid instantiat
ions of term equivalence which range from beta-equivalence, to
contextual equiva lence, to some exotic equivalences.
|
[47]
|
Michael Greenberg, Benjamin Pierce, and Stephanie Weirich.
Contracts Made Manifest.
In 37th ACM SIGACT-SIGPLAN Symposium on Principles of
Programming Languages (POPL), pages 353--364, Madrid, Spain, January 2010.
[ PDF ]
Since Findler and Felleisen introduced higher-order contracts, many
variants have been proposed. Broadly, these fall into two groups:
some follow Findler and Felleisen in using latent contracts, purely
dynamic checks that are transparent to the type system; others use
manifest contracts, where refinement types record the most recent
check that has been applied to each value. These two approaches are
commonly assumed to be equivalent---different ways of implementing the
same idea, one retaining a simple type system, and the other providing
more static information. Our goal is to formalize and clarify this
folklore understanding.
Our work extends that of Gronski and Flanagan, who defined a latent
calculus lambdac and a manifest calculus lambdah, gave a translation
phi from lambdac to lambdah, and proved that, if a lambdac term
reduces to a constant, then so does its phiimage. We enrich their
account with a translation psi from lambdah to lambdac and prove an
analogous theorem.
We then generalize the whole framework to dependent contracts, whose
predicates can mention free variables. This extension is both
pragmatically crucial, supporting a much more interesting range of
contracts, and theoretically challenging. We define dependent
versions of lambdah and two dialects (“lax” and “picky”) of
lambdac, establish type soundness---a substantial result in itself,
for lambdah---and extend phi and psi accordingly. Surprisingly, the
intuition that the latent and manifest systems are equivalent now
breaks down: the extended translations preserve behavior in one
direction but, in the other, sometimes yield terms that blame more.
|
[48]
|
Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjöberg, Stephanie Weirich, and
Steve Zdancewic.
Reactive Noninterference.
In 16th ACM Conference on Computer and Communications Security,
pages 79--90, November 2009.
[ PDF ]
Many programs operate reactively---patiently waiting for user input, running
for a while producing output, and eventually returning to a state where they
are ready to accept another input (or occasionally diverging). When a
reactive program communicates with multiple parties, we would like to be
sure that it can be given secret information by one without leaking it to
others.
Motivated by web browsers and client-side web applications,
we explore definitions of noninterference for reactive programs and
identify two of special interest---one corresponding to
termination-insensitive noninterference for a simple sequential language,
the other to termination-sensitive noninterference. We focus on the former
and develop a proof technique for showing that program behaviors are secure
according to this definition. To demonstrate the viability of the approach,
we define a simple reactive language with an information-flow type system
and apply our proof technique to show that well-typed programs are secure.
|
[49]
|
Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones.
FPH: First-class polymorphism for Haskell.
In ICFP 2008: The 13th ACM SIGPLAN International Conference on
Functional Programming, pages 295--306, Victoria, BC, Canada, September
2008.
[ PDF ]
Languages supporting polymorphism typically have ad-hoc restrictions
on where polymorphic types may occur. Supporting “first-class” polymorphism,
by lifting those restrictions, is obviously desirable, but it is hard
to achieve this without sacrificing type inference. We present a new
type system for higher-rank and impredicative polymorphism that improves
on earlier proposals: it is an extension of Damas-Milner;
it relies only on System F types; it has a simple, declarative specification;
it is robust to program transformations; and it enjoys a complete and decidable
type inference algorithm.
|
[50]
|
Daniel S. Dantas, David Walker, Geoffrey Washburn, and Stephanie Weirich.
AspectML: A Polymorphic Aspect-oriented Functional Programming
Language.
ACM Transactions on Programming Languages, 30(3):1--60, May
2008.
[ Project
PDF ]
This paper defines Aspectml, a typed functional, aspect-oriented
programming language. The main contribution of Aspectml is the
seamless integration of polymorphism, run-time type analysis
and aspect-oriented programming language features. In particular,
Aspectml allows programmers to define type-safe polymorphic advice
using pointcuts constructed from a collection of polymorphic join
points. Aspectml also comes equipped with a type inference algorithm
that conservatively extends Hindley-Milner type inference. To support
first-class polymorphic point-cut designators, a crucial feature for
developing aspect-oriented profiling or logging libraries, the
algorithm blends the conventional Hindley-Milner type inference
algorithm with a simple form of local type inference.
We give our language operational meaning via a type-directed
translation into an expressive type-safe intermediate language. Many
complexities of the source language are eliminated in this
translation, leading to a modular specification of its semantics. One
of the novelties of the intermediate language is the definition of
polymorphic labels for marking control-flow points. These labels are
organized in a tree structure such that a parent in the tree serves as
a representative for all of its children. Type safety requires that
the type of each child is less polymorphic than its parent
type. Similarly, when a set of labels is assembled as a pointcut, the
type of each label is an instance of the type of the pointcut.
|
[51]
|
Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and
Stephanie Weirich.
Engineering Formal Metatheory.
In ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages (POPL), pages 3--15, January 2008.
[ Project
PDF ]
Machine-checked proofs of properties of programming languages have become a
critical need, both for increased confidence in large and complex designs
and as a foundation for technologies such as proof-carrying code. However,
constructing these proofs remains a black art, involving many choices in the
formulation of definitions and theorems that make a huge cumulative
difference in the difficulty of carrying out large formal developments. The
representation and manipulation of terms with variable binding is a
key issue.
We propose a novel style for formalizing metatheory, combining
locally nameless representation of terms and
cofinite quantification of free variable names in inductive
definitions of relations on terms (typing, reduction, ...). The
key technical insight is that our use of cofinite quantification
obviates the need for reasoning about equivariance (the fact that free
names can be renamed in derivations); in particular, the structural
induction principles of relations defined using cofinite
quantification are strong enough for metatheoretic reasoning, and
need not be explicitly strengthened.
Strong inversion principles follow (automatically, in Coq) from the
induction principles. Although many of the underlying ingredients of
our technique have been used before, their combination here yields a
significant improvement over existing methodology, leading to
developments that are faithful to informal practice, yet require no
external tool support and little infrastructure within the proof
assistant.
We have carried out several large developments in this style using the Coq
proof assistant and have made them publicly available. Our developments
include type soundness for and ML (with references, exceptions,
datatypes, recursion and patterns) and subject reduction for the Calculus of
Constructions. Not only do these developments demonstrate the
comprehensiveness of our approach; they have also been optimized for clarity
and robustness, making them good templates for future extension.
|
[52]
|
Geoffrey Washburn and Stephanie Weirich.
Boxes Go Bananas: Encoding Higher-order Abstract Syntax with
Parametric Polymorphism.
Journal of Functional Programming, 18(1):87--140, January 2008.
[ PDF ]
Higher-order abstract syntax is a simple technique for implementing
languages with functional programming. Object variables and binders
are implemented by variables and binders in the host language. By
using this technique, one can avoid implementing common and tricky
routines dealing with variables, such as capture-avoiding
substitution. However, despite the advantages this technique provides,
it is not commonly used because it is difficult to write sound
elimination forms (such as folds or catamorphisms) for
higherorder abstract syntax. To fold over such a datatype, one must
either simultaneously define an inverse operation (which may not
exist) or show that all functions embedded in the datatype are
parametric.
In this paper, we show how first-class polymorphism can be used to
guarantee the parametricity of functions embedded in higher-order
abstract syntax. With this restriction, we implement a library of
iteration operators over data-structures containing functionals. From
this implementation, we derive fusion laws that functional
programmers may use to reason about the iteration operator. Finally,
we show how this use of parametric polymorphism corresponds to the
Schürmann, Despeyroux and Pfenning method of enforcing parametricity
through modal types. We do so by using this library to give a sound
and complete encoding of their calculus into System F-omega. This
encoding can serve as a starting point for reasoning about
higher-order structures in polymorphic languages.
|
[53]
|
Dimitrios Vytiniotis and Stephanie Weirich.
Free theorems and runtime type representations.
In Mathematical Foundations of Programming Semantics (MFPS
XXIII), pages 357--373, New Orleans, LA, USA, April 2007.
[ PDF
PS ]
Reynolds' abstraction theorem, often referred to
as the parametricity theorem, can be used to derive properties about
functional programs solely from their types. Unfortunately, in the
presence of runtime type analysis, the abstraction properties of
polymorphic programs are no longer valid. However, runtime type
analysis can be implemented with term-level representations of
types, as in the language of Crary et
al., where case analysis on
these runtime representations introduces type refinement. In this
paper, we show that representation-based analysis is consistent with
type abstraction by extending the abstraction theorem to such a
language. We also discuss the “free theorems” that result. This
work provides a foundation for the more general problem of extending
the abstraction theorem to languages with generalized algebraic
datatypes.
|
[54]
|
Dimitrios Vytiniotis and Stephanie Weirich.
Dependent types: Easy as PIE.
In Marco T. Morazán and Henrik Nilsson, editors, Draft
Proceedings of the 8th Symposium on Trends in Functional Programming, pages
XVII--1---XVII--15. Dept. of Math and Computer Science, Seton Hall
University, April 2007.
TR-SHU-CS-2007-04-1.
[ PDF ]
|
[55]
|
Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark
Shields.
Practical type inference for arbitrary-rank types.
Journal of Functional Programming, 17(1):1--82, January 2007.
[ Project
PDF ]
Haskell's popularity has driven the need for ever more expressive type
system features, most of which threaten the decidability and
practicality of Damas-Milner type inference. One such feature is the
ability to write functions with higher-rank types --- that is,
functions that take polymorphic functions as their arguments.
Complete type inference is known to be undecidable for higher-rank
(impredicative) type systems, but in practice programmers are more
than willing to add type annotations to guide the type inference
engine, and to document their code. However, the choice of just what
annotations are required, and what changes are required in the type
system and its inference algorithm, has been an ongoing topic of
research.
We take as our starting point a lambda-calculus proposed by Odersky
and Laufer. Their system supports arbitrary-rank polymorphism through
the exploitation of type annotations on lambda-bound arguments and
arbitrary sub-terms. Though elegant, and more convenient than some
other proposals, Odersky and Laufer's system requires many
annotations. We show how to use local type inference (invented by
Pierce and Turner) to greatly reduce the annotation burden, to the
point where higher-rank types become eminently usable.
Higher-rank types have a very modest impact on type inference. We
substantiate this claim in a very concrete way, by presenting a
complete type-inference engine, written in Haskell, for a traditional
Damas-Milner type system, and then showing how to extend it for
higher-rank types. We write the type-inference engine using a monadic
framework: it turns out to be a particularly compelling example of
monads in action.
The paper is long, but is strongly tutorial in style.
|
[56]
|
Stephanie Weirich.
Type-Safe Run-time Polytypic Programming.
Journal of Functional Programming, 16(10):681--710, November
2006.
[ PDF ]
Polytypic programming is a way of defining type-indexed
operations, such as map, fold and zip, based on type information.
Run-time polytypic programming allows that type information to
be dynamically computed---this support is essential in modern
programming languages that support separate compilation, first-class
type abstraction, or polymorphic recursion.
However, in previous work we defined run-time polytypic programming
with a type-passing semantics. Although it is natural to define
polytypic programs as operating over first-class types, such a
semantics suffers from a number of drawbacks. This paper describes
how to recast that work in a type-erasure semantics, where terms
represent type information in a safe manner. The resulting language
is simple and easy to implement---we present a prototype
implementation of the necessary machinery as a small Haskell
library.
|
[57]
|
Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey
Washburn.
Simple unification-based type inference for GADTs.
In International Conference on Functional Programming (ICFP),
pages 50--61, Portland, OR, USA, September 2006.
[ PDF ]
Generalized algebraic data types (GADTs), sometimes known as “guarded
recursive data types” or “first-class phantom
types”, are a simple but powerful generalization of
the data types of Haskell and ML. Recent works have
given compelling examples of the utility of GADTs,
although type inference is known to be difficult. Our
contribution is to show how to exploit
programmer-supplied type annotations to make the type
inference task almost embarrassingly easy. Our main
technical innovation is wobbly types, which express in
a declarative way the uncertainty caused by the
incremental nature of typical type-inference
algorithms.
|
[58]
|
Dimitrios Vytiniotis, Stephanie Weirich, and Simon L. Peyton Jones.
Boxy type inference for higher-rank types and impredicativity.
In International Conference on Functional Programming (ICFP),
pages 251--262, Portland, OR, USA, September 2006.
[ Project
PDF ]
Languages with rich type systems are beginning to
employ a blend of type inference and type
checking, so that the type inference engine is
guided by programmer-supplied type annotations. In
this paper we show, for the first time, how to combine
the virtues of two well-established ideas:
unification-based inference, and bidirectional
propagation of type annotations. The result is a type
system that conservatively extends Hindley-Milner, and
yet supports both higher-rank types and
impredicativity.
|
[59]
|
Geoffrey Washburn and Stephanie Weirich.
Good Advice for Type-directed Programming: Aspect-oriented
Programming and Extensible Generic Functions.
In Workshop on Generic Programming (WGP), pages 33--44,
Portland, OR, USA, September 2006.
[ Project
PDF ]
Type-directed programming is an important idiom for software design.
In type-directed programming the behavior of programs is guided by the
type structure of data. It makes it possible to implement many sorts
of operations, such as serialization, traversals, and queries, only
once and without needing to continually revise their implementation as
new data types are defined.
Type-directed programming is the basis for recent research into
"scrapping" tedious boilerplate code that arises in functional
programming with algebraic data types. This research has primarily
focused on writing type-directed functions that are closed to
extension. However, Lämmel and Peyton Jones recently developed a
technique for writing openly extensible type-directed functions in
Haskell by making clever use of type classes. Unfortunately, this
technique has a number of limitations.
We present an alternate approach to writing openly extensible
type-directed functions by using the aspect-oriented programming
features provided by the language AspectML. Our solution not only
avoids the limitations present in Lämmel and Peyton Jones technique,
but also allows type-directed functions to be extended at any time
with cases for types that were not even known at compile-time. This
capability is critical to writing programs that make use of dynamic
loading or runtime type generativity.
|
[60]
|
Stephanie Weirich.
RepLib: A library for derivable type classes.
In Haskell Workshop, pages 1--12, Portland, OR, USA, September
2006.
[ Project
PDF ]
Some type class instances can be automatically derived from the
structure of types. As a result, the Haskell language includes the
"deriving" mechanism to automatic generates such instances for a
small number of built-in type classes. In this paper, we present
RepLib, a GHC library that enables a similar mechanism for arbitrary
type classes. Users of RepLib can define the relationship between
the structure of a datatype and the associated instance declaration
by a normal Haskell functions that pattern-matches a representation
types. Furthermore, operations defined in this manner are
extensible---instances for specific types not defined by type
structure may also be incorporated. Finally, this library also
supports the definition of operations defined by parameterized
types.
|
[61]
|
Brian Aydemir, Aaron Bohannon, and Stephanie Weirich.
Nominal Reasoning Techniques in Coq.
In International Workshop on Logical Frameworks and
Meta-Languages:Theory and Practice (LFMTP), pages 60--69, Seattle, WA, USA,
August 2006.
[ Project
PDF ]
We explore an axiomatized nominal approach to variable binding in Coq,
using an untyped lambda-calculus as our test case. In our nominal
approach, alpha-equality of lambda terms coincides with Coq's built-in
equality. Our axiomatization includes a nominal induction principle and
functions for calculating free variables and substitution. These axioms
are collected in a module signature and proved sound
using locally nameless terms as the underlying
representation. Our experiences so far suggests that it is feasible to
work from such axiomatized theories in Coq and that the nominal style of
variable binding corresponds closely with paper proofs. We are currently
working on proving the soundness of a primitive recursion combinator
and developing a method of generating these axioms and their proof of
soundness from a grammar describing the syntax of terms and binding.
|
[62]
|
Benjamin C. Pierce, Peter Sewell, Stephanie Weirich, and Steve Zdancewic.
It is Time to Mechanize Programming Language Metatheory.
In Verified Software: Theories, Tools, Experiments (VS:TTE),
pages 26--30, Zürich, Switzerland, October 2005.
[ Project
PDF ]
How close are we to a world in which mechanically verified software is
commonplace? A world in which theorem proving technology is used
routinely by both software developers and programming
language researchers alike? One crucial step towards achieving these
goals is mechanized reasoning about language metatheory. The time has
come to bring together the theorem proving and programming language
communities to address this problem. We have proposed the POPLMark
challenge as a concrete set of benchmarks intended both for measuring
progress in this area and for stimulating discussion and
collaboration. Our goal is to push the boundaries of existing
technology to the point where we can achieve mechanized metatheory for
the masses.
|
[63]
|
Daniel S. Dantas, David Walker, Geoffrey Washburn, and Stephanie Weirich.
PolyAML: A polymorphic aspect-oriented functional programmming
language.
In ACM SIGPLAN International Conference on Functional
Programming (ICFP), pages 306--319, Tallinn, Estonia, September 2005.
[ Project
PDF
PS ]
This paper defines PolyAML, a typed functional and aspect-oriented
programming language. The main contribution of PolyAML is in the
seamless integration of polymorphism, run-time type analysis and
aspect-oriented programming language features. In particular, PolyAML
allows programmers to define type-safe polymorphic advice using pointcuts
constructed from a collection of polymorphic join points. PolyAML
also comes equipped with a type inference algorithm that conservatively
extends Hindley-Milner type inference. In order to support first-class
polymorphic point-cut designators, a crucial feature for developing
aspect-oriented profiling or logging libraries, the algorithm blends the
conventional Hindley-Milner type inference algorithm with a simple form
of local type inference.
We give our language operational meaning via a type-directed
translation into an expressive type-safe intermediate language. Many
complexities of the source language are eliminated in this
translation, leading to a modular specification of its semantics. One
of the novelties of the intermediate language is the definition of
polymorphic labels for marking control-flow points. These labels are
organized in a tree structure such that a parent in the tree serves as
a representative for the collection of all its children. Type safety
requires that the type of each child is a generic instance of the type
of the polymorphic parent. Similarly, when a set of labels is
assembled as a pointcut, the type of each label is an instance of the
type of the pointcut.
|
[64]
|
Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster,
Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn,
Stephanie Weirich, and Steve Zdancewic.
Mechanized Metatheory for the Masses: The POPLmark Challenge.
In The 18th International Conference on Theorem Proving in
Higher Order Logics (TPHOLs), pages 50--65, Oxford, UK, August 2005.
[ Project
PDF
PS ]
How close are we to a world where every paper on
programming languages is accompanied by an electronic appendix with
machine-checked proofs?
We propose a concrete set of benchmarks for measuring progress in this
area. Based on the metatheory of System F-sub, a typed
lambda-calculus with second-order polymorphism, subtyping, and
records, these benchmarks embody many aspects of programming languages
that are challenging to formalize: variable binding at both the term
and type levels, syntactic forms with variable numbers of components
(including binders), and proofs demanding complex induction
principles. We hope that these benchmarks will help clarify the
current state of the art, provide a basis for comparing competing
technologies, and motivate further research.
|
[65]
|
Geoffrey Washburn and Stephanie Weirich.
Generalizing Parametricity Using Information Flow.
In Twentieth Annual IEEE Symposium on. Logic in Computer Science
(LICS 2005), pages 62--71, Chicago, IL, USA, June 2005.
[ Project
PDF
PS ]
Run-time type analysis allows programmers to easily and
concisely define many operations based upon type structure, such as
serialization, iterators, and structural equality. However, when
types can be inspected at run time, nothing is secret. A module
writer cannot use type abstraction to hide implementation details from
clients: those clients can use type analysis to determine the
structure of these supposedly “abstract” data types. Furthermore,
access control mechanisms do not help in isolating the implementation
of abstract datatypes from their clients. Buggy or malicious
authorized modules may simply leak type information to unauthorized
clients, so module implementors cannot reliably tell which parts of a
program rely on their type definitions and which parts do not.
Currently, module implementors rely on parametric polymorphism to
provide guarantees about the use of their abstract datatypes.
Standard type parametricity does not hold for a language with run-time
type analysis, but in this paper we show how to generalize the
statement of parametricity so that it does hold in the presence of
type analysis and still encompasses the integrity and confidentiality
policies that are normally derived from parametricity. The key is to
augment the type system with annotations about information flow.
Because the type system tracks the flow of dynamic type information,
the implementor of an abstract data type can easily see what parts of
the program depend on the implementation of a given type.
|
[66]
|
Dimtrios Vytiniotis, Geoffrey Washburn, and Stephanie Weirich.
An Open and Shut Typecase.
In ACM SIGPLAN Workshop on Types in Language Design and
Implementation, pages 13--24, Long Beach, CA, USA, January 2005.
[ PS ]
Two different ways of defining ad-hoc polymorphic operations commonly
occur in programming languages. With the first form polymorphic
operations are defined inductively on the structure of types while
with the second form polymorphic operations are defined for specific
sets of types.
In intensional type analysis operations are defined by induction on
the structure of types. Therefore no new cases are necessary for
user-defined types, because these types are equivalent to their
underlying structure. However, intensional type analysis is
“closed” to extension, as the behavior of the operations cannot be
differentiated for the new types, thus destroying the distinctions
that these types are designed to express.
Haskell type classes on the other hand define polymorphic operations
for sets of types. Operations defined by class instances are
considered “open”---the programmer can add instances for new types
without modifying existing code. However, the operations must be
extended with specialized code for each new type, and it may be
tedious or even impossible to add extensions that apply to a large
universe of new types.
Both approaches have their benefits, so it is important to let
programmers decide which is most appropriate for their needs. In this
paper, we define a language that supports both forms of ad-hoc
polymorphism, using the same basic constructs.
|
[67]
|
Stephanie Weirich.
Type-Safe Cast.
Journal of Functional Programming, 14(6):681--695, November
2004.
[ PDF ]
Comparing two types for equality is an essential ingredient for an
implementation of dynamic types. Once equality has been established,
it is safe to cast a value from one type to another. In a language
with run-time type analysis, implementing such a procedure is fairly
straightforward. Unfortunately, this naive implementation destructs
and rebuilds the argument while iterating over its type structure.
However, by using higher-order polymorphism, a casting function can
treat its argument parametrically. We demonstrate this solution in
two frameworks for ad-hoc polymorphism: intensional type analysis
and Haskell type classes.
|
[68]
|
Stephanie Weirich and Liang Huang.
A Design for Type-Directed Java.
In Viviana Bono, editor, Workshop on Object-Oriented
Developments (WOOD), ENTCS, pages 117--136, August 2004.
[ Project
PDF
PS ]
Type-directed programming is an important and widely used
paradigm in the design of software. With this form of programming,
an application may analyze type information to determine its
behavior. By analyzing the structure of data, many operations, such
as serialization, cloning, adaptors and iterators may be defined
once, for all types of data. That way, as the program evolves, these
operations need not be updated---they will automatically adapt to
new data forms. Otherwise, each of these operations must be
individually redefined for each type of data, forcing programmers to
revisit the same program logic many times during a program's
lifetime.
The Java language supports type directed programming with the
instanceof operator and the Java Reflection API. These
mechanisms allow Java programs to depend on the name and structure
of the run-time classes of objects. However, the Java mechanisms
for type-directed programming are difficult to use. They also do not
integrate well with generics, an important new feature of the Java
language.
In this paper, we describe the design of several expressive new
mechanisms for type-directed programming in Java, and show that
these mechanisms are sound when included in a language similar to
Featherweight Java. Basically, these new mechanisms pattern-match
the name and structure of the type parameters of generic code,
instead of the run-time classes of objects. Therefore, they
naturally integrate with generics and provide strong guarantees
about program correctness. As these mechanisms are based on pattern
matching, they naturally and succinctly express many operations that
depend on type information. Finally, they provide programmers with
some degree of protection for their abstractions. Whereas
instanceof and reflection can determine the exact run-time type
of an object, our mechanisms allow any supertype to be supplied for
analysis, hiding its precise structure.
|
[69]
|
Geoffrey Washburn and Stephanie Weirich.
Boxes Go Bananas: Encoding Higher-order Abstract Syntax with
Parametric Polymorphism.
In ACM SIGPLAN International Conference on Functional
Programming (ICFP), pages 249--262, Uppsala, Sweden, August 2003.
[ PDF
PS ]
Higher-order abstract syntax is a simple technique for
implementing languages with functional programming. Object variables
and binders are implemented by variables and binders in the host
language. By using this technique, one can avoid implementing common
and tricky routines dealing with variables, such as capture-avoiding
substitution. However, despite the advantages this technique
provides, it is not commonly used because it is difficult to write
sound elimination forms (such as folds or catamorphisms) for
higher-order abstract syntax. To fold over such a datatype, one must
either simultaneously define an inverse operation (which may not
exist) or show that all functions embedded in the datatype are
parametric.
In this paper, we show how first-class polymorphism can be used to
guarantee the parametricity of functions embedded in higher-order
abstract syntax. With this restriction, we implement a library of
iteration operators over data-structures containing functionals. From
this implementation, we derive “fusion laws” that functional
programmers may use to reason about the iteration operator. Finally,
we show how this use of parametric polymorphism corresponds to the
Schuermann, Despeyroux and Pfenning method of enforcing
parametricity through modal types. We do so by using this library to
give a sound and complete encoding of their calculus into System F-omega.
This encoding can serve as a starting point for reasoning about
higher-order structures in polymorphic languages.
|
[70]
|
Karl Crary, Stephanie Weirich, and Greg Morrisett.
Intensional Polymorphism in Type Erasure Semantics.
Journal of Functional Programming, 12(6):567--600, November
2002.
[ PDF ]
Intensional polymorphism, the ability to dispatch to
different routines based on types at run time, enables a variety
of advanced implementation techniques for polymorphic languages,
including tag-free garbage collection, unboxed function
arguments, polymorphic marshalling, and flattened data
structures. To date, languages that support intensional
polymorphism have required a type-passing (as opposed to
type-erasure) interpretation where types are constructed and
passed to polymorphic functions at run time. Unfortunately,
type-passing suffers from a number of drawbacks; it requires
duplication of constructs at the term and type levels, it
prevents abstraction, and it severely complicates polymorphic
closure conversion. We present a type-theoretic framework that
supports intensional polymorphism, but avoids many of the
disadvantages of type passing. In our approach, run-time type
information is represented by ordinary terms. This avoids the
duplication problem, allows us to recover abstraction, and avoids
complications with closure conversion. In addition, our type
system provides another improvement in expressiveness; it allows
unknown types to be refined in place thereby avoiding certain
beta-expansions required by other frameworks.
|
[71]
|
Stephanie Weirich.
Higher-Order Intensional Type Analysis.
In Daniel Le Métayer, editor, 11th European Symposium on
Programming (ESOP), pages 98--114, Grenoble, France, April 2002.
[ PDF
PS ]
Intensional type analysis provides the ability to
analyze abstracted types at run time. In this paper, we extend
that ability to higher-order and kind-polymorphic type
constructors. The resulting language is elegant and expressive:
we show through examples how it extends the repertoire of
polytypic functions that may be defined.
|
[72]
|
Stephanie Weirich.
Encoding Intensional Type Analysis.
In D. Sands, editor, 10th European Symposium on Programming
(ESOP), pages 92--106, Genova, Italy, April 2001.
[ PDF
PS
http ]
Languages for intensional type analysis permit ad-hoc
polymorphism, or run-time analysis of types. However, such
languages require complex, specialized constructs to support this
operation, which hinder optimization and complicate the
meta-theory of these languages. In this paper, we observe that
such specialized operators need not be intrinsic to the language,
and in fact, their operation may be simulated through standard
encodings of iteration in the polymorphic lambda
calculus. Therefore, we may more easily add intensional analysis
operators to complicated languages via a translation semantics,
instead of through language extension.
|
[73]
|
Michael Hicks, Stephanie Weirich, and Karl Crary.
Safe and Flexible Dynamic Linking of Native Code.
In R. Harper, editor, Types in Compilation: Third International
Workshop, TIC 2000; Montreal, Canada, September 21, 2000; Revised Selected
Papers, volume 2071 of Lecture Notes in Computer Science, pages
147--176. Springer, 2001.
[ PDF
PS
http ]
We present the design and implementation of the first
complete framework for flexible and safe dynamic linking of
native code. Our approach extends Typed Assembly Language with a
primitive for loading and typechecking code, which is flexible
enough to support a variety of linking strategies, but simple
enough that it does not significantly expand the trusted
computing base. Using this primitive, along with the ability to
compute with types, we show that we can program many existing
dynamic linking approaches. As a concrete demonstration, we have
used our framework to implement dynamic linking for a type-safe
dialect of C, closely modeled after the standard linking facility
for Unix C programs. Aside from the unavoidable cost of
verification, our implementation performs comparably with the
standard, untyped approach.
|
[74]
|
Stephanie Weirich.
Type-Safe Cast: Functional Pearl.
In Proceedings of the fifth ACM SIGPLAN International
Conference on Functional Programming (ICFP), pages 58--67, Montreal, Canada,
September 2000.
[ PDF
PS ]
In a language with non-parametric or ad-hoc
polymorphism, it is possible to determine the identity of a type
variable at run time. With this facility, we can write a function
to convert a term from one abstract type to another, if the two
hidden types are identical. However, the naive implementation of
this function requires that the term be destructed and rebuilt. In
this paper, we show how to eliminate this overhead using
higher-order type abstraction. We demonstrate this solution in two
frameworks for ad-hoc polymorphism: intensional type analysis and
type classes.
|
[75]
|
Karl Crary and Stephanie Weirich.
Resource Bound Certification.
In The Twenty-Seventh ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages (POPL), pages 184--198, Boston, MA, USA,
January 2000.
[ PDF
PS ]
Various code certification systems allow the
certification and static verification of a variety of important
safety properties such as memory safety and control-flow
safety. These systems provide valuable tools for verifying that
untrusted and potentially malicious code is safe before execution.
However, one important safety property that is not usually
included is that programs adhere to specific bounds on resource
consumption, such as running time.
We present a decidable type system capable of specifying and
certifying bounds on resource consumption. Our system makes two
advances over previous resource bound certification systems, both
of which are necessary for a practical system: we allow the
execution time of programs and their subroutines to vary,
depending on their arguments, and we provide a fully automatic
compiler generating certified executables from source-level
programs. The principal device in our approach is a strategy for
simulating dependent types using sum and inductive kinds.
|
[76]
|
Karl Crary and Stephanie Weirich.
Flexible Type Analysis.
In Proceedings of the fourth ACM SIGPLAN International
Conference on Functional Programming (ICFP), pages 233--248, Paris, France,
September 1999.
[ PDF
PS ]
Run-time type dispatch enables a variety of advanced
optimization techniques for polymorphic languages, including
tag-free garbage collection, unboxed function arguments, and
flattened data structures. However, modern type-preserving
compilers transform types between stages of compilation, making
type dispatch prohibitively complex at low levels of typed
compilation. It is crucial therefore for type analysis at these
low levels to refer to the types of previous
stages. Unfortunately, no current intermediate language supports
this facility.
To fill this gap, we present the language LX, which provides a
rich language of type constructors supporting type analysis
(possibly of previous-stage types) as a programming idiom. This
language is quite flexible, supporting a variety of other
applications such as analysis of quantified types, analysis with
incomplete type information, and type classes. We also show that
LX is compatible with a type-erasure semantics.
|
[77]
|
Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick
Smith, David Walker, Stephanie Weirich, and Steve Zdancewic.
TALx86: A Realistic Typed Assembly Language.
In Second ACM SIGPLAN Workshop on Compiler Support for
System Software, pages 25--35, Atlanta, GA, USA, May 1999.
Published as INRIA research report number 0228, March 1999.
[ PDF
PS ]
The goal of typed assembly language (TAL) is to provide
a low-level, statically typed target language that is better
suited than Java bytecodes for supporting a wide variety of
source languages and a number of important optimizations. In
previous work, we formalized idealized versions of TAL and proved
important safety properties about them. In this paper, we present
our progress in defining and implementing a realistic typed
assembly language called TALx86. The TALx86 instructions comprise
a relatively complete fragment of the Intel IA32 (32-bit 80x86
flat model) assembly language and are thus executable on
processors such as the Intel Pentium. The type system for the
language incorporates a number of advanced features necessary for
safely compiling large programs to good code.
To motivate the design of the type system, we demonstrate how
various high-level language features are compiled to TALx86. For
this purpose, we present a type-safe C-like language called
Popcorn.
|
[78]
|
Karl Crary, Stephanie Weirich, and Greg Morrisett.
Intensional Polymorphism in Type Erasure Semantics.
In Proceedings of the third ACM SIGPLAN International
Conference on Functional Programming (ICFP), pages 301--313, Baltimore, MD,
USA, September 1998.
[ PDF
PS ]
Intensional polymorphism, the ability to dispatch to
different routines based on types at run time, enables a variety of
advanced implementation techniques for polymorphic languages,
including tag-free garbage collection, unboxed function arguments,
polymorphic marshalling, and flattened data structures. To date,
languages that support intensional polymorphism have required a
type-passing (as opposed to type-erasure) interpretation where types
are constructed and passed to polymorphic functions at run
time. Unfortunately, type-passing suffers from a number of
drawbacks; it requires duplication of constructs at the term and
type levels, it prevents abstraction, and it severely complicates
polymorphic closure conversion. We present a type-theoretic
framework that supports intensional polymorphism, but avoids many of
the disadvantages of type passing. In our approach, run-time type
information is represented by ordinary terms. This avoids the
duplication problem, allows us to recover abstraction, and avoids
complications with closure conversion. In addition, our type system
provides another improvement in expressiveness; it allows unknown
types to be refined in place thereby avoiding certain
beta-expansions required by other frameworks.
|
[79]
|
Cormac Flanagan, Matthew Flatt, Shriram Krishnamurthi, Stephanie Weirich, and
Matthias Felleisen.
Catching Bugs in the Web of Program Invariants.
In ACM SIGPLAN Conference on Programming Language Design and
Implementation (PLDI), pages 23--32, 1996.
[ PDF
PS ]
MrSpidey is a user-friendly, interactive static
debugger for Scheme. A static debugger supplements the standard
debugger by analyzing the program and pinpointing those program
operations tha may cause run-time errors suce as dereferencing
the null pointer or applying non-functions. The program analysis
of MrSpidey computes value set descriptions for each term in the
program and constructs a value flow graph connecting the set
descriptions. Using the set descriptions, MrSpidey can identify
and highlight potentially erroneous program operations, whose
cause the programmer can the explore by selectively exposing
portions of the value flow graph.
|
|
Artifacts, Extended Versions, and Technical Reports
[1]
|
Cassia Torczon, Emmanuel Suárez Acevedo, Shubh Agrawal, Joey
Velez-Ginorio, and Stephanie Weirich.
Artifact associated with "Effects and Coeffects in
Call-By-Push-Value".
Technical report, July 2024.
[ DOI
http ]
|
[2]
|
Li-yao Xia, Laura Israel, Maite Kramarz, Nicholas Coltharp, Koen Claessen,
Stephanie Weirich, and Yao Li.
Story of Your Lazy Function's Life: A Bidirectional Demand
Semantics for Mechanized Cost Analysis of Lazy Programs (Artifact).
Technical report, June 2024.
[ DOI
http ]
|
[3]
|
Yiyun Liu, Jonathan Chan, Jessica Shi, and Stephanie Weirich.
Artifact associated with Internalizing Indistinguishability
with Dependent Types.
Technical report, October 2023.
Awarded “Available” and “Evaluated & Reusable” badges by POPL
2024 Artifact Evaluation Committee.
[ DOI
http ]
|
[4]
|
Yiyun Liu and Stephanie Weirich.
Artifact Associated with Dependently-Typed Programming with
Logical Equality Reflection.
Technical report, 2023.
Awarded “Available” and “Evaluated & Reusable” badges by ICFP
2023 Artifact Evaluation Committee.
[ DOI
http ]
This artifact contains the complete mechanized Coq proofs
of the lemmas and theorems about System DE. The VM image is
preinstalled with the dependencies required to build and
verify the Coq development.
Keywords: Coq, Dependent types, Mechanized metatheory
|
[5]
|
Yao Li and Stephanie Weirich.
Program Adverbs and Tlön Embeddings (artifact).
Technical report, June 2022.
Awarded “Available” and “Evaluated & Reusable” badges by ICFP
2023 Artifact Evaluation Committee.
[ DOI ]
|
[6]
|
Pritam Choudhury, Harley Eades III, and Stephanie Weirich.
Artifact Associated with A Dependent Dependency Calculus.
Technical report, January 2022.
Awarded “Reusable” and “Available” badges by ESOP 2022 Artifact
Evaluation Committee.
[ DOI ]
|
[7]
|
Yao Li, Li yao Xia, and Stephanie Weirich.
Reasoning about the garden of forking paths (artifact).
Technical report, May 2021.
Awarded “Functional” and “Available” badges by ICFP 2021 Artifact
Evaluation Committee.
[ DOI ]
|
[8]
|
Yao Li, Li-yao Xia, and Stephanie Weirich.
Reasoning about the garden of forking paths.
Technical report, March 2021.
[ arXiv
http ]
|
[9]
|
Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie
Weirich.
Artifact for “A Graded Dependent Type System with a Usage-Aware
Semantics”.
Technical report, December 2020.
Awarded “Reusable”, “Functional” and “Available” badges by POPL
2021 Artifact Evaluation Committee.
[ DOI ]
|
[10]
|
Pritam Choudhury, Harley D. Eades III, Richard A. Eisenberg, and Stephanie
Weirich.
A Graded Dependent Type System with a Usage-Aware Semantics
(Extended Version).
Technical report, 2020.
[ http ]
|
[11]
|
Stephanie Weirich, Pritam Choudhury, Antoine Voizard, and Richard A. Eisenberg.
Replication Package for Article: A Role for Dependent Types in
Haskell.
Technical report, July 2019.
Awarded “Functional” and “Available” badges by ICFP 2019 Artifact
Evaluation Committee.
[ DOI ]
|
[12]
|
Stephanie Weirich, Pritam Choudhury, Antoine Voizard, and Richard Eisenberg.
A Role for Dependent Types in Haskell (Extended Version).
Technical report, 2019.
[ http ]
|
[13]
|
Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John
Wiegley, Joshua Cohen, and Stephanie Weirich.
The hs-to-coq tool with examples.
Technical report, July 2018.
Awarded “Artifacts Available” and “Artifacts Evaluated -
Functional” badges by ICFP 2018 Artifact Evaluation Committee.
[ DOI ]
|
[14]
|
Richard A. Eisenberg, Stephanie Weirich, and Hamidhasan G. Ahmed.
Visible Type Application (Extended version).
Technical report, January 2016.
[ PDF ]
|
[15]
|
Vilhelm Sjöberg and Stephanie Weirich.
Programming up to Congruence (Extended Version).
Technical Report MS-CIS-14-10, University of Pennsylvania, October
2014.
[ PDF ]
|
[16]
|
Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie
Weirich.
Safe Zero-cost Coercions for Haskell (Extended Version).
Technical Report MS-CIS-14-07, Univ. of Pennsylvania, April 2014.
[ PDF ]
|
[17]
|
Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, and Stephanie
Weirich.
Closed type families with overlapping equations (Extended
version).
Technical Report MS-CIS-13-10, University of Pennsylvania, November
2013.
[ PDF ]
|
[18]
|
Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich.
Combining Proofs and Programs in a Dependently Typed Language
(With Technical Appendix).
Technical Report MS-CIS-13-08, University of Pennsylvania, November
2013.
[ PDF ]
|
[19]
|
Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg.
System FC with explicit kind equality (Extended Version).
Technical report, September 2013.
[ PDF ]
|
[20]
|
Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, and Steve
Zdancewic.
Generative Type Abstraction and Type-level Computation (Extended
Version).
Technical report, November 2010.
[ PDF ]
Modular languages support generative type abstraction,
ensuring that an abstract type is distinct from its
representation, except inside the implementation where the
two are synonymous. We show that this well-established
feature is in tension with the non-parametric features
of newer type systems, such as indexed type families and GADTs.
In this paper we solve the problem by using kinds to
distinguish between parametric and non-parametric contexts.
The result is directly applicable to Haskell, which is rapidly
developing support for type-level computation, but the same
issues should arise whenever generativity and non-parametric features
are combined.
|
[21]
|
Aaron Stump, Vilhelm Sjöberg, and Stephanie Weirich.
Termination Casts: A Flexible Approach to Termination with
General Recursion (Technical Appendix).
Technical Report MS-CIS-10-21, University of Pennsylvania Department
of Computer and Information Science, 2010.
[ PDF ]
|
[22]
|
Dimitrios Vytiniotis, Stephanie Weirich, and Simon L. Peyton Jones.
Simple unification-based type inference for GADTs, Technical
Appendix.
Technical Report MS-CIS-05-22, University of Pennsylvania, April
2006.
[ PDF ]
|
[23]
|
Dimitrios Vytiniotis, Stephanie Weirich, and Simon L. Peyton Jones.
Boxy type inference for higher-rank types and impredicativity,
Technical Appendix.
Technical Report MS-CIS-05-23, University of Pennsylvania, April
2006.
[ PDF ]
|
[24]
|
Geoffrey Washburn and Stephanie Weirich.
Generalizing Parametricity Using Information Flow (Extended
version).
Technical Report MS-CIS-05-04, Computer and Information Science,
University of Pennsylvania, July 2005.
[ PDF ]
Run-time type analysis allows programmers to easily and
concisely define many operations based upon type structure, such as
serialization, iterators, and structural equality. However, when
types can be inspected at run time, nothing is secret. A module
writer cannot use type abstraction to hide implementation details from
clients: those clients can use type analysis to determine the
structure of these supposedly “abstract” data types. Furthermore,
access control mechanisms do not help in isolating the implementation
of abstract datatypes from their clients. Buggy or malicious
authorized modules may simply leak type information to unauthorized
clients, so module implementors cannot reliably tell which parts of a
program rely on their type definitions and which parts do not.
Currently, module implementors rely on parametric polymorphism to
provide guarantees about the use of their abstract datatypes.
Standard type parametricity does not hold for a language with run-time
type analysis, but in this paper we show how to generalize the
statement of parametricity so that it does hold in the presence of
type analysis and still encompasses the integrity and confidentiality
policies that are normally derived from parametricity. The key is to
augment the type system with annotations about information flow.
Because the type system tracks the flow of dynamic type information,
the implementor of an abstract data type can easily see what parts of
the program depend on the implementation of a given type.
|
[25]
|
Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark
Shields.
Practical type inference for arbitrary-rank types (Technical
appendix).
Technical Report MIS-CIS-05-14, University of Pennsylvania, July
2005.
[ Project
PDF ]
|
[26]
|
Daniel S. Dantas, David Walker, Geoffrey Washburn, and Stephanie Weirich.
PolyAML: A Polymorphic Aspect-Oriented Functional Programming
Language (Extended Version).
Technical Report MS-CIS-05-07, University of Pennsylvania, Department
of Computer and Information Science, 2005.
[ PDF ]
This paper defines PolyAML, a typed functional, aspect-oriented programming language. The main contribution of PolyAML is the seamless integration of polymorphism, run-time type analysis and aspect-oriented programming language features. In particular, PolyAML allows programmers to define type-safe polymorphic advice using pointcuts constructed from a collection of polymorphic join points. PolyAML also comes equipped with a type inference algorithm that conservatively extends Hindley-Milner type inference. To support first-class polymorphic point-cut designators, a crucial feature for developing aspect-oriented profiling or logging libraries, the algorithm blends the conventional Hindley-Milner type inference algorithm with a simple form of local type inference.
We give our language operational meaning via a type-directed translation into an expressive type-safe intermediate language. Many complexities of the source language are eliminated in this translation, leading to a modular specification of its semantics. One of the novelties of the intermediate language is the definition of polymorphic labels for marking control-flow points. These labels are organized in a tree structure such that a parent in the tree serves as a representative for all of its children. Type safety requires that the type of each child is less polymorphic than its parent type. Similarly, when a set of labels is assembled as a pointcut, the type of each label is an instance of the type of the pointcut.
|
[27]
|
Dan S. Dantas, David Walker, Geoffrey Washburn, and Stephanie Weirich.
Analyzing Polymorphic Advice.
Technical Report TR-717-04, Princeton University Computer Science,
December 2004.
[ Project
PDF ]
We take one of the first steps towards developing a
practical, statically-typed, functional, aspect-oriented
programming language by showing how to integrate polymorphism and
type analysis with aspect-oriented programming features. In
particular, we demonstrate how to define type-safe polymorphic
advice using pointcuts that unify a collection of polymorphic join
points. We also introduce a new mechanism for specifying
context-sensitive advice that involves pattern matching against the
current stack of activation records, and meshes well with
functional programming idioms. We give our language meaning via a
type-directed translation into an expressive, but fairly simple,
type-safe intermediate language. Many complexities of the source
language are eliminated in this translation, leading to a modular
specification of its semantics. One of the novelties of the
intermediate language is the definition of polymorphic labels for
marking control-flow points. These labels are organized in a tree
structure such that a parent in the tree serves as a representative
for the collection of all its children. Type safety requires that
the type of each child is a generic instance of the type of the
polymorphic parent. Similarly, when a set of labels is assembled
as a pointcut, the type of each label is an instance of the type of
the pointcut.
|
[28]
|
Dimtrios Vytiniotis, Geoffrey Washburn, and Stephanie Weirich.
An Open and Shut Typecase (Extended Version).
Technical Report MS-CIS-04-26, University of Pennsylvania, Computer
and Information Science, October 2004.
[ PDF ]
Ad-hoc polymorphism is a compelling addition to typed programming languages. There are two different forms of ad-hoc polymorphism. With the nominal form, the execution of an operation is determined solely by the name of the type argument, whereas with the structural form, operations are defined by case analysis on the structure of types. The two forms differ in the way that they treat user-defined types. Operations defined by the nominal approach are considered "open"--the programmer can add cases for new types without modifying existing code. The operations must be extended however with specialized code for the new types, and it may be tedious and even difficult to add extensions that apply to a potentially large universe of user-defined types. Structurally defined operations apply to new types by treating them as equal to their underlying definitions, so no new cases for new types are necessary. However this form is considered "closed" to extension, as the behaviour of the operations cannot be differentiated for the new types. This form destroys the distinctions that user-defined types are designed to express. Both approaches have their benefits, so it is important to provide both capabilities in a single language that is expressive enough to decouple the "openness" issue from the way that user-defined types are treated. We present such a language that supports both forms of ad-hoc polymorphism.
|
[29]
|
Liang Huang and Stephanie Weirich.
A Design for Type-Directed Programming in Java (Extended
Version).
Technical Report MS-CIS-04-11, University of Pennsylvania, Computer
and Information Science, October 2004.
[ PDF
PS ]
|
[30]
|
Simon L. Peyton Jones, Geoffrey Washburn, and Stephanie Weirich.
Wobbly types: Practical Type Inference for Generalised Algebraic
Dataypes.
Technical Report MS-CIS-05-26, University of Pennsylvania, Computer
and Information Science Department, Levine Hall, 3330 Walnut Street,
Philadelphia, Pennsylvania, 19104-6389, July 2004.
[ PDF ]
Generalised algebraic data types (GADTs), sometimes known as “guarded
recursive data types” or “first-class phantom types”, are a simple
but powerful generalisation of the data types of Haskell and ML.
Recent works have given compelling examples of the utility of GADTs,
although type inference is known to be difficult.
It is time to pluck the fruit. Can GADTs be added to Haskell, without
losing type inference, or requiring unacceptably heavy type annotations?
Can this be done without completely rewriting the already-complex Haskell
type-inference engine, and without complex interactions with (say)
type classes? We answer these questions in the affirmative, giving
a type system that explains just what type annotations are required,
and a prototype implementation that implements it. Our main technical
innovation is wobbly types, which express in a declarative way
the uncertainty caused by the incremental nature of typical type-inference
algorithms.
|
[31]
|
Geoffrey Washburn and Stephanie Weirich.
Unifying nominal and structural ad-hoc polymorphism (Extended
version).
Technical report, University of Pennsylvania, March 2004.
[ PDF ]
Ad-hoc polymorphism allows the execution of programs to
depend on type information. In modern systems, it is useful for
implementing generic operations over data structures, such as
equality, marshalling, or traversal. In the past, there have been
two different forms of ad-hoc polymorphism. The nominal form
dispatches on the name of the type argument, whereas the structural
form operates by decomposing the structure of types. In languages
with user-defined types, these two approaches are very
different. Operations defined by the nominal approach are
“open”---they must be extended with specialized branches for
user-defined types. In contrast, structurally defined operations are
closed to extension. They automatically apply to user-defined types
by treating them as their underlying definitions. Both approaches
have their benefits, so it important to provide both capabilities in
a language. Therefore we present an expressive language that
supports both forms of ad-hoc polymorphism in a single framework.
Among the language's features are the ability to define both
“open” and “closed” operations with a single mechanism, the
ability to naturally restrict the domain of type-analyzing
operations, and new mechanisms for defining higher-order polytypism
and manipulating generative type definitions.
|
[32]
|
Geoffrey Washburn and Stephanie Weirich.
Boxes Go Bananas: Encoding Higher-order Abstract Syntax with
Parametric Polymorphism (Extended version).
Technical Report MS-CIS-03-26, University of Pennsylvania, Computer
and Information Science, September 2003.
[ PDF
PS ]
Higher-order abstract syntax is a simple technique for implementing languages with functional programming. Object variables and binders are implemented by variables and binders in the host language. By using this technique, one can avoid implementing common and tricky routines dealing with variables, such as capture-avoiding substitution. However, despite the advantages this technique provides, it is not commonly used because it is difficult to write sound elimination forms (such as folds or catamorphisms) for higher-order abstract syntax. To fold over such a datatype, one must either simultaneously define an inverse operation (which may not exist) or show that all functions embedded in the datatype are parametric.
In this paper, we show how first-class polymorphism can be used to guarantee the parametricity of functions embedded in higher-order abstract syntax. With this restriction, we implement a library of iteration operators over data-structures containing functionals. From this implementation, we derive "fusion laws" that functional programmers may use to reason about the iteration operator. Finally, we show how this use of parametric polymorphism corresponds to the Schuermann, Despeyroux and Pfenning method of enforcing parametricity through modal types. We do so by using this library to give a sound and complete encoding of their calculus into System F-omega. This encoding can serve as a starting point for reasoning about higher-order structures in polymorphic languages.
|
[33]
|
Michael Hicks and Stephanie Weirich.
A Calculus for Dynamic Loading.
Technical Report MS-CIS-00-07, University of Pennsylvania, April
2000.
[ PDF ]
We present the load-calculus, used to model dynamic loading, and prove it sound. The calculus extends the polymorphic lambda-calculus with a load primitive that dynamically loads terms that are closed, with respect to values. The calculus is meant to approximate the process of dynamic loading in TAL/Load , a version of Typed Assembly Language extending with dynamic linking. To model the key aspects of TAL, the calculus contains references and facilities for named types. Loadable programs may refer to named types defined by the running program, and may export new types to code loaded later. Our approach follows the framework initially outlined by Glew et. al. This calculus has been implemented in the TALx86 version of Typed Assembly Language, and is used to implement a full-featured dynamic linking library, DLpop.
|
[34]
|
Karl Crary, Stephanie Weirich, and Greg Morrisett.
Intensional Polymorphism in Type Erasure Semantics (Extended
Version).
Technical Report TR98-1721, Cornell University, Computer Science,
November 1998.
[ PDF
PS ]
|
|