Gradual Typing in Agda
About
Formalizations of Gradually Typed Languages in Agda.
The current release is v2.1
.
Agda Version
The release v2.1
of this project has been checked by Agda
version 2.6.2
with the Agda standard library version 1.7
.
Prerequisites/Dependencies
This project depends on the Abstract Binding Trees library,
specifically release v1.0
.
https://github.com/jsiek/abstract-binding-trees
After cloning that repository, make sure to add the path to abt.agda-lib
to the libraries
file in your .agda
directory and to add abt
to
the defaults
file.
Correspondence with article in Journal of Function Programming
The article "Parameterized Cast Calculi and Reusable Meta-theory for Gradually Typed Lambda Calculi" describes most of this Agda development. Here we provide a mapping from sections in that article to the files in this project.
- Introduction - no corresponding Agda files
- Gradually Typed Lambda Calculus: GTLC
- Parameterized Cast Calculus
- PreCastStructure
- ParamCastAux
- ParamCastAux
- CastStructure
- ParamCastCalculusOrig
- ParamCastReductionOrig
- ParamCastDeterministic
- ParamCastReductionOrig
- ParamCastCalculus, ParamCastReduction
- PreCastStructureWithBlameSafety CastStructureWithBlameSafety, Subtyping, ParamCastSubtyping, and ParamBlameSubtyping.
- PreCastStructureWithPrecision, CastStructureWithPrecision, ParamCCPrecision, ParamGradualGuaranteeAux, ParamGradualGuaranteeSim, and ParamGradualGuarantee.
- Compilation of GTLC to CC: GTLC2CCOrig
- A Half-Dozen Cast Calculi
- EDA: SimpleCast
- EDI: SimpleFunCast
- λB: GroundCast, GroundCastGG
- EDC: SimpleCoercions
- LDC: LazyCoercions
- λC: GroundCoercion
- Space-Efficient Parameterized Cast Caclulus
- EfficientParamCastAux
- CastStructure (
ComposableCasts
is namedEfficientCastStruct
) - EfficientParamCasts
- EfficientParamCasts
- PreserveHeight and SpaceEfficient
- Space-Efficient Cast Calculi
Inventory
-
Labels: Definition of blame labels.
-
PrimitiveTypes and Types: Definition of gradual types and operators on them, such as precision, consistency, etc.
-
Variables: Definition of variables as de Bruijn indices.
-
GTLC: Syntax and type system of the Gradually Typed Lambda Calculus with pairs and sums.
-
GTLC-materialize: A version of the GTLC that uses the materialize rule (subsumption with precision) instead of using the consistency relation.
-
PreCastStructure: A record definition
PreCastStruct
that abstracts the representation of a cast. It includes a type constructorCast
for casts, operations on casts (e.g.dom
andcod
) and categories of casts (Active
,Inert
,Cross
). This record definition does not depend on the definition of terms. Two records extendPreCastStruct
with their respective definitions and lemmas:- PreCastStructureWithBlameSafety: Contains the definition of a cast being blame safe and its related lemmas. Used in the blame theorem proof.
- PreCastStructureWithPrecision: Contains precision relations between (inert) casts and their related lemmas. Used in the gradual guarantee proof.
-
CastStructure: contains two record definitions: the
CastStruct
record and theEfficientCastStruct
. TheCastStruct
record extendsPreCastStruct
with anapplyCast
operation that applies an active cast to a value to produce a term. TheEfficientCastStruct
record also extendsPreCastStruct
with anapplyCast
operation, but also includes acompose
operation for compressing two casts into a single cast. Two records extendCastStruct
with their respective lemmas:- CastStructureWithBlameSafety:
Contains a preservation lemma about
CastsAllSafe
. - CastStructureWithPrecision: Contains various simulation lemmas between less precise and more precise terms.
- CastStructureWithBlameSafety:
Contains a preservation lemma about
-
We maintain two variants of the parameterized cast calculus (CC):
- ParamCastCalculusOrig: Syntax and type
system (it is intrinsically typed) for the Parameterized Cast
Calculus. It is parameterized over a type constructor
Cast
. This includes the definition of substitution. - ParamCastCalculus: This is mostly the same as the version above, except it has a separate term constructor for inert cast ("wrap"). This is used when defining the precision relation and proving the gradual guarantee.
- ParamCastCalculusOrig: Syntax and type
system (it is intrinsically typed) for the Parameterized Cast
Calculus. It is parameterized over a type constructor
-
ParamCastAux: defines
Value
,Frame
,plug
, the wrapper reductions based on the idea of eta expansion, and proves a canonical forms lemma for type dynamic. This module is parameterized over aPreCastStruct
. -
ParamCastReductionOrig: Reduction rules and proof of type safety for the first version of hte Parameterized Cast Calculus, parameterized over a
CastStruct
. -
ParamCastReduction: Reduction rules and proof of type safety for the second version of hte Parameterized Cast Calculus, parameterized over a
CastStruct
. -
ParamCastDeterministic: A proof that reduction is deterministic.
-
EfficientParamCastAux: defines
SimpleValue
,Value
, and proves a canonical forms lemma for type dynamic. This module is parameterized overPreCastStruct
. -
EfficientParamCasts: A space-efficient reduction relation for the parameterized cast calculus. This module requires a compose function for casts, so it is parameterized over
EfficientCastStruct
. This module includes a proof of progress. -
Compilation of the GTLC to the corresponding variant of the Parameterized Cast Calculus (CC). The compilation is type preserving.
- GTLC2CCOrig: From GTLC to
ParamCastCalculusOrig
. - GTLC2CC: From GTLC to
ParamCastCalculus
.
- GTLC2CCOrig: From GTLC to
-
Space-efficiency theorem:
-
PreserveHeight: Proves that the height of the casts in a program do not increase during reduction. Their size is bounded by their height, so this result contributes to the proof of space efficiency.
-
SpaceEfficient: A proof that the space-efficient reduction relation really is space efficient. That is, the casts that can accumulate during reduction only multiply the size of the program by a constant.
-
-
Blame-subtyping theorem:
- Subtyping: The module defines several subtyping relations used in the blame-subtyping theorem. They are the same relations as the ones in the Exploring the Design Space paper.
- ParamCastSubtyping: The module defines
what it means for a term
M
to contain only safe casts with the labelℓ
(CastsAllSafe
). We show that the data typeCastsAllSafe
is preserved during reduction. - ParamBlameSubtyping: A formalized
proof of the blame-subtyping theorem. The theorem statement says
that "if every cast labeled by
ℓ
is safe cast (respects subtyping, or a recursive safety definition if is coercion-based) in a termM
thenM
cannot reduce toblame ℓ
". It is slightly different, but equivalent to, the theorem statement in the Refined Criteria paper (Siek, Vitousek, Cimini, and Boyland 2015).
-
The gradual guarantee: We define this theorem as a simulation between less precise and more precise terms.
- ParamCCPrecision: The definition of precision for the Parameterized Cast Calculus.
- ParamGradualGuaranteeAux:
This module is parameterized by
PreCastStructWithPrecision
and contains inversion lemmas about less precise and more precise values, with inert casts wrapped around one or both sides. - ParamGradualGuaranteeSim:
This module is parameterized by
CastStructWithPrecision
. It contains multiple simulation lemmas and acatchup
lemma: the less precise side can catch up with a more precise value by reducing to a value that is less precise. - ParamGradualGuarantee:
This module is also parameterized by
CastStructWithPrecision
. It contains the main theorem statement and proof ofgradual-guarantee
.
-
GroundCast: Type safety of λB (Siek, Thiemann, Wadler 2015). ("lazy UD" of Siek, Garcia, and Taha 2009)
-
LazyGroundCast: λB but with active casts between function types.
-
GroundInertX: The cast representation in Refined Criteria (Siek, Vitousek, Cimini, and Boyland 2015). ("lazy UD" with inert cross cast)
-
GroundCoercion: Type safety of λC (Siek, Thiemann, Wadler 2015). ("lazy UD" of Siek, Garcia, and Taha 2009)
-
EfficientGroundCoercions: Type safety of λS (Siek, Thiemann, Wadler 2015). ("lazy UD" of Siek, Garcia, and Taha 2009)
-
HyperCoercions: A alternative to λS that optimizes the coercion representation by removing indirections. ("lazy UD")
-
SimpleCast: Type safety of the cast calculus of Siek and Taha (2006). (Called "partially-eager D" by Siek, Garcia, and Taha 2009).
-
SimpleFunCast: The same as above but casts between function types are values.
-
SimpleCoercions: Type safety for the cast calculus of Siek and Taha (2006) again, but the calculus is expressed with coercions.
-
LazyCast: Type safety for the "lazy D" calculus (Siek, Garcia, and Taha 2009).
-
LazyCoercions: Type safety for the "lazy D" calculus, with casts represented as coercions.
-
AGT: A space-efficient version of the GTLC inspired by Abstracting Gradual Typing (Garcia, Clark, and Tanter 2016). This is also closely related to the threesomes of Siek and Wadler (2011).
-
AbstractMachine: A space-efficient abstract machine. It's a variant of the SECD machine with optimized tail calls. It's parameterized with respect to casts.
-
GroundMachine: The abstract machine instantiated with the coercions from λS. ("lazy UD")
-
EquivCast: Proof of equivalence (simulation) between two instances of the Parameterized Cast Calculus.
-
EquivLamBLamC: Proof that λC simulates λB, by insantiating the above EquivCast module.
-
ForgetfulCast: Inspired by Greenberg's forgetful contracts. (
🚧 UNDER CONSTRUCTION🚧 )