This is a simple prototype implementation of a pure type system with dependent intersections, a heterogeneous equality, and implicit products. This allows one to have a pure-type-system capable of expressing dependent elimination principals.
Right now, the language only supports adding declarations and type checking them. All files must begin with a module declaration;
module Nat where
After that, a declaration of the form <NAME> : <TYPE> = <TERM>
can be declared;
cNat : U[0] = (a : U[0]) -> (a -> a) -> a -> a
cZ : cNat = \ a s z . z
U[0] is a universe. For each natural number i, there is a corresponding
type universe U[i], with U[i] : U[i+1], etc.
Implicit products are denoted with curly braces;
{<NAME> : <TYPE>} -> <TYPE>
And implicit lambda binders are denoted with a forward slash
/ <NAME> . <TERM>
To issue an implicit argument, use <TERM> - <TERM>
Lambda terms are denoted with a back-slash. Type annotations are optional, but are sometimes necessary for type inference.
Dependent intersections are denoted
i (<NAME> : <TYPE>) . <TYPE>
Square braces are used for constructing dependent intersections;
[ <TERM> | <TERM> ]
Any term c of a dependent intersection i (x : A) . B x can
then be typed as A via c.1, and typed as B c.1 with
c.2.
Heterogeneous identity is denoted a ~ b.
Elimination is denoted r(<NAME> . <TYPE>) <EQUATION> . <TERM>.
This is one of the main differences between this implementation and
the Stump paper. Here, r binds a variable, and one must provide a type
which acts as any possible intermediate substitution. For example, say
we had a proof that e : t1 ~ t2, and we knew that p : P t1, and we
want to obtain P t2. We have, as an intermediate form, x . P x.
We use this in the full elimination
r(x . P x) e . p
Which will be of type P t2. Note that x is only bound in the intermediate
type-form, not in anything else. Additionally, reflexive proofs are denoted
B.
- Navigate to directory and run
cabal install - The
iotatt.exewill appear in.\dist\build\iotatt\ - Load a program with
iotatt.exe Nat.itt
-
From Realizability to Induction via Dependent Intersection, Aaron Stump. This paper describes the type theory that this language is based on, as well as a different implementation.
-
Simply Easy!, Andres Loh, Conor McBride, Wouter Swierstra. I used the lambda-Pi system described on page 6 as a reference when unifying types and kinds.
Anthony Hart