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.

1. Introduction - no corresponding Agda files
2. Gradually Typed Lambda Calculus: GTLC
3. Parameterized Cast Calculus
   1. PreCastStructure
   2. ParamCastAux
   3. ParamCastAux
   4. CastStructure
   5. ParamCastCalculusOrig
   6. ParamCastReductionOrig
   7. ParamCastDeterministic
   8. ParamCastReductionOrig
   9. ParamCastCalculus, ParamCastReduction
   10. PreCastStructureWithBlameSafety CastStructureWithBlameSafety, Subtyping, ParamCastSubtyping, and ParamBlameSubtyping.
   11. PreCastStructureWithPrecision, CastStructureWithPrecision, ParamCCPrecision, ParamGradualGuaranteeAux, ParamGradualGuaranteeSim, and ParamGradualGuarantee.
4. Compilation of GTLC to CC: GTLC2CCOrig
5. A Half-Dozen Cast Calculi
   1. EDA: SimpleCast
   2. EDI: SimpleFunCast
   3. λB: GroundCast, GroundCastGG
   4. EDC: SimpleCoercions
   5. LDC: LazyCoercions
   6. λC: GroundCoercion
6. Space-Efficient Parameterized Cast Caclulus
   1. EfficientParamCastAux
   2. CastStructure (ComposableCasts is named EfficientCastStruct)
   3. EfficientParamCasts
   4. EfficientParamCasts
   5. PreserveHeight and SpaceEfficient
7. Space-Efficient Cast Calculi
   1. EfficientGroundCoercions
   2. HyperCoercions

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 constructor Cast for casts, operations on casts (e.g. dom and cod) and categories of casts (Active, Inert, Cross). This record definition does not depend on the definition of terms. Two records extend PreCastStruct 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 the EfficientCastStruct. The CastStruct record extends PreCastStruct with an applyCast operation that applies an active cast to a value to produce a term. The EfficientCastStruct record also extends PreCastStruct with an applyCast operation, but also includes a compose operation for compressing two casts into a single cast. Two records extend CastStruct with their respective lemmas:

  • CastStructureWithBlameSafety: Contains a preservation lemma about CastsAllSafe .
  • CastStructureWithPrecision: Contains various simulation lemmas between less precise and more precise terms.

• 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.

• 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 a PreCastStruct.

• 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 over PreCastStruct.

• 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.

• 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 type CastsAllSafe 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 term M then M cannot reduce to blame ℓ". 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 a catchup 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 of gradual-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 🚧 )