twanvl/ttie

Type Theory with Indexed Equality

TTIE - Type Theory with Indexed Equality

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.

Syntax

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.

Usage

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

Examples

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