This project is created to encourage the internal cat of a particular donut to implement some full-scale type checker/dependently typed language.
- Observational Equality
- Universe Polymorphism a là Conor McBride
- Holes and first class implicit functions
Extensional equality principles are very useful for both math formalization and proving program properties, but has long been a second-class citizen in proof assistants due to technical difficulties. OTT [1] [2] [3] is an approach to integrate extensional principles into intensional type theory, while retaining good metatheory properties like canonicity and strong normalization.
AFAIK, OTT is currently the most promising approach to extensional equality principles:
| type theory | funext | UIP | canonicity | normalization | regularity1 |
|---|---|---|---|---|---|
| ITT | no | no | yes | yes | yes |
| ITT + axiom | yes | yes | no | yes | yes |
| ITT + irr. | no | yes | yes | yes2 | yes |
| ETT | yes | yes | yes | no3 | yes |
| HoTT | yes | no | no | yes | yes |
| Cubical TT | yes | no | yes | yes (no NBE yet) | no/difficult |
| OTT | yes | yes | yes | yes | possible (see [2]) |
1: whether eliminating refl computes to the identity.
2: there are sound NBE implementations that lack universe hierarchy [4]. However, adding too much irrelevance and impredicativity breaks normalization [5]
3: type checking ETT itself is very difficult, due to the need to automatically "guess"
propositional equalities.
This difficulty can be avoided by requiring user annotations [6].
But even so, ETT fails to normalize (e.g. see [6]) in the presence of universe/large elimination.
Also, ETT allows ill-typed open terms such as 0 1 or fst (\x. x),
making type-directed normalization very difficult. See [7] for some discussions.
Despite its good properties, there seems to be many different ways to implement/formalize OTT. [1] [2] [3] and an existing implementation [8] all use different approaches:
-
In [1], observational equalities are built using builtin constructors. This requires a set of primitive constructors for every type former.
-
In [2], the equality type computes to the type of its proof/witness. But I am afraid that this will make type checking difficult: the endpoints of an equality type is hard to retrieve after it computes to something else.
The type system in [2] uses a separate (definitionally) proof-irrelevant proposition fragment to support (definitional) UIP.
[2] also stresses the issue of regularity. Without regularity, elimination of inductive types may have undesirable computational behavior. The authors propose adding a regularity rule to overcome this problem, implementation may be similar to [4]
-
[3] also adapts the "equality type computes to proof" approach and definitional irrelevance in [2]. However, while both [1] and [2] uses an heterogenous equality, [3] features homogeneous equality. It also supports propositional regularity. But I am worried that this may cause some kind of coercion hell.
-
[8] is the only implementation I found for OTT online. It features quotient type, normalization-by-evaluation and regularity. The NBE algorithm erases all equality proofs, which is good computationally, but probably not so desirable from a formalization point of view.
In this project, my approach to implement OTT is:
- equality types are heterogeneous, don't compute to something else, and are definitionally proof irrelevant
- no primitive equality constructors, all necessary operations on equalities are supported via axioms
- so long as all axioms are irrelevant, canonicity would be safe
- support definitional regularity, following the approach in [4]
- equality proofs are not erased, but perhaps wrapped in lazy thunks to avoid unnecessary computation
Universe hierarchy and polymorphism here follows the proposal of Conor McBride [9] [10]. In this style of universe hierarchy:
-
viewing a small type from a larger universe is done implicitly via bidirectional type checking and subtyping
-
the universe level of a global definition is the smallest possible value ("build on the ground"), no level variables needed
-
enlarging a small type (i.e. "shift to higher", universe polymorphism) is done via a explicit operator
~. The operator accumulates on global variables and is structural on all other term formers. In the surface syntax, you can only shift a globally defined variable. To shift more than one level, you can add the number of levels to shift after the "~", e.g.~3 id
The implementation strategy comes from [11]
This project is distributed under the zero clause BSD license. See LICENSE.
[1] Towards Observational Equality
[2] Observational Equality, Now!
[3] Observational Equality: Now For Good!
[4] Extensional Normalization in the Logical Framework with Proof Irrelevant Equality
[5] Failure of Normalization in Impredicative Type Theory with Proof-irrelevant Propositional Equality
[6] Equality, Quasi-Implicit Products, and Large Eliminations
[7] https://proofassistants.stackexchange.com/questions/1301/tutorial-implementations-of-extensional-type-theories
[8] https://github.com/bobatkey/sott
[9] https://personal.cis.strath.ac.uk/conor.mcbride/Crude.pdf
[10] https://pigworker.wordpress.com/2015/01/09/universe-hierarchies/
[11] Dependently typed lambda calculus with a lifting operator