A demo interpreter and type checker of a type theory with interval indexed equality types.
The indexed equality type looks like this (in Agda notation):
data Interval : Type where
0 : Interval
1 : Interval
01 : 0 == 1
data Eq (A : Interval -> Type) (A 0) (A 1) : Type where
refl : (x : (i : Interval) -> A i) -> Eq A (x 0) (x 1)
We write the binders for intervals as a subscript, so Eq_i (A i) x y.
The syntax is modeled after Agda and Haskell:
-- a comment
{- also a comment -}
variable
_ -- a hole, filled in by unification
Type : Type1 -- the type of types
tt : Unit -- built in unit type, with constructor tt
Unit -> Unit -- function type
Unit → Unit -- Unicode
(A : Type) -> A -> A -- dependent function type
{A : Type} -> A -> A -- implicit arguments
forall x -> B x -- the same as (x : _) -> B x
∀ x. B x -- the same
\x -> e -- lambdas / anonymous functions
\(x : A) -> e -- with type annotation
(x : A) => e -- same
f x -- function application
f {x} -- explicit application to an implicit argument
(x : A) * B x -- dependent sums (pairs)
{x : A} * B x -- with implicit arguments (to model existentials)
exists x -> B x -- the same as (x : _) * B x
∃ x. B x -- the same
x , y -- construct a pair
proj1 x -- first projection of a pair
proj2 x -- second projection
{proj1} x -- projection of an implicit pair/existential
{x} , y -- explicit construction of an implicit pair
0
1 : Interval -- The interval has values 0 and 1
01 : Eq _ 0 1 -- the path between 0 and 1
refl_i i -- the same
iflip i -- sends 0 to 1 and vice-versa
~i -- the same
iand i j -- 1 if i and j are both 1
i && j -- the same
i || j -- 1 if i or j is 1
Eq A x y -- type of equality proofs of x and y of type A
Eq_i (A i) x y -- indexed equality between x : A 0 and y : A 1
x == y -- sugar for equality type
refl x -- reflexivity at x
refl_i (x i) -- indexed version
xy^i -- end point of a path, if xy : Eq _ x y, xy^0 = x, xy^1 = y, refl_i xy^i = xy
iv x y xy i -- desugared version of xy^i
cast_i (A i) u v x -- substitution: if (x : A u), the result has type (A v)
fw_i (A i) x -- short hand notation for cast_i (A i) 0 1
bw_i (A i) x -- short hand notation for cast_i (A i) 1 0
data{left:A; right:B} -- A sum type, constructors have a single argument type
value left x -- A value of the above data type, you may need a type signature
case x of {left y -> ..; right y -> ..} -- case analysis of a sum type
data{} -- The type with no constructors (bottom)
Declarations and commands look like
name : Type
name arguments = expression
:help
:quit
:type e
:eval e
:nf e
:check e = e'
Remarks:
- Built in names like
Eq,proj1,cast, etc. must always be fully applied. - Spaces around operators like
->are usually required, because-can be part of a name. - There is no support for recursion yet.
- Implicit projections have not yet been implemented.
- Unification is often not very smart.
The implementation comes with a REPL and an interpreter:
$ cabal build
$ dist/ttie examples/Lemmas
The unit tests from Tests.hs are also instructive
$ cabal test
Here is a proof that fw ∘ bw = id
A : Type
B : Type
AB : Eq _ A B
lemma : forall x. fw_i (AB^i) (bw_i AB^i x) == x
lemma = \x -> refl_j (cast_i AB^i j 1 (cast_i AB^i 1 j x))
Proof of function extensionality:
ext : ∀ {A : Type} {B : A → Type} {f g : (x : A) → B x} → (∀ x. f x == g x) → f == g
ext = \fg → refl_i \x → (fg x)^i