A PTS Supporting Induction
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
withc.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 denotedB
.
cabal install
iotatt.exe
will appear in .\dist\build\iotatt\
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