-- Intro --
pts is a type checker and normalizer for pure type systems. At its core it's
a library, but it comes with a read-eval-print loop allowing one to fiddle
with many type systems. This is an overview of how to interact.
The prompt will inform you of the type system in which you are currently
working. Regardless, pi types will be available to work with. The syntax
is:
(x : k) -> t
where t may mention x. As a special case, where x is not mentioned in t, one
can write
k -> t
Other type systems will likely have other sorts.
-- Commands --
Typing a term by itself at the prompt is the same as the :echo command.
:type
infers the type of the given term
:let =
checks that the term is well typed, and adds it to the environment under
the given name.
:tlet : =
infers the type of the term on the right of the equals sign, and ensures
that it's beta-equal to the given type, then adds it to the environment
under the given name. This is useful if the inferred type would be less
readable, such as specifying that a term has type Nat, instead of the
Church encoding thereof.
:env
displays the names in the environment
:tenv
displays the names and types thereof in the environment
:assume :
assumes a postulate into existence with the given name and type
:normal/:nf
computes the normal form of a term, assuming it's well-typed
:whnf
computes the weak head normal form of a term, assuming it's well-typed
:echo
parses a term, and then pretty prints it
:dump
parses a term, and dumps the abstract syntax tree (useful for debugging)
:load
loads a file, which should contain a list of commands as above. The commands
are executed.
:{:}
enables multi-line input. Normally any above command would have to fit on a
single line, but when :{ is encountered, input will be consumed as a single
command until a matching :} is seen. This is also necessary for multi-line
definitions/etc. in :loaded files.
:
All type systems have an associated command to switch to them. Switching will
clear the environment.
-- Type Systems --
* Lambda Cube -- all lambda cube systems have * as an additional constant (* has
a type ◻, but it is the only sort at that level, and so is not
even in the parser)
:simp : The simply typed lambda calculus
No quantification is possible in this system, but one can :assume types of
kind * in order to write functions.
:f2 : System F, the second-order lambda calculus
This extends the simply typed calculus with universal quantification, and
many datatypes can be encoded by their eliminator. For instance:
Nat = (r : *) -> r -> (r -> r) -> r
There is a predicative version :pf2, but it is severely limited, as Church
encoded types like above then have kind ◻, and even multiple universal
quantifiers are disallowed.
:fw : System F_omega
This extends System F with higher-order types, and quantification thereover.
It is a type system quite close to Haskell's, except with arbitrary rank
polymorphism. Similar to :f2, there is a predicative :pfw, which has similar
problems encoding inductive data, but is somewhat less crippled than :pf2.
:lf : The logical framework
This type system doesn't have the above universal quantifier over types, but
instead has type dependency upon values. This turns out to make it the
Curry-Howard analogue of first-order logic, and one can use it in a similar
way, :assuming types and predicates to make a sort of first-order theory.
:lf2 : the second order dependently-typed lambda calculus
This is a combination of :f2 and :lf, and corresponds to second-order
predicate logic.
:coc : the calculus of constructions
This system contains every rule of the lambda cube, and has the full spectrum
of what one would expect in a dependent pure type system. :coc has predicative
rules, but there is a similar :icoc that has an impredicative rule, allowing
one to usefully encode datatypes as in :f2 and :fw.
* Other
:tower : an infinite hierarchy of universes
This system extends the calculus of constructions by having more than just *
and ◻. Instead, it has a hierarchy Set : Set1 : Set2 : .... All universes
are closed under pi types in conjunction with themselves and lower universes,
for instance:
T : Set2
U : T -> Set1
(x : T) -> U x : Set2
There is a variant, :itower, in which the lowest level, Set, is impredicative,
meaning that regardless of what sort T is:
U : T -> Set
(x : T) -> U x : Set
This allows datatypes to be encoded similarly to :icoc, :f2 and :fw. All other
levels follow the normal max(i,j) rules, because impredicativity on levels
other than the lowest can be used to construct paradoxes that lead to
non-termination.
:hm : a Hindley-Milner alike
This is a system that attempts to type only valid Hindley-Milner style terms.
The syntax is that of the lambda cube systems above. However, the * that one
is allowed to refer to ranges only over monotypes, and when terms are printed,
monotype kinds and polytype kinds will be distinguished by appending an m or p.
So:
T : *m
T -> T : *m
(a : *) -> a -> T : *p
etc. :hm only allows types that can be written in prenex normal form, while
the type system :hhm has additional rules that allow rank-n types. Although
both these systems are predicative, in that variables in quantifiers don't
range over types with quantifiers (and therefore themselves), they lack the
oddness of the predicative cube systems (for instance, T -> ((a : *) -> a)
is not a valid :pfw type, because the rule to allow it would enable
dependent types). However, these systems do not have a suitable encoding of
data, because Church encodings will be forced into *p, and thus not
quantified over with *m.
To rectify this, one can also add something like newtype in Haskell.
This has been done in the type systems :ihm and :ihhm. To allow Church encoding,
a constant Ty : *p -> *m is built in, to inject encodings into monotypes. To
construct elements, given T : *p, and t : T, and t' : Ty T
Con T t : Ty T
unCon T t' : T
and normalization eliminates adjacent Con-unCon pairs. This technically makes the
system impredicative (although impredicativity is tagged by Ty), hence the names.
:sysu : System U
This is a type system rather like the calculus of constructions, but with three
universe levels: * : □ : △. □ is the only inhabitant of △, and there are likewise
no function spaces quantifying over △ itself. However, both * and □ admit
impredicative quantification, so given T : * and K : □ :
((U : *) -> T) : *
((L : □) -> T) : *
((L : □) -> K) : □
and so on. Girard showed that this additional impredicativity allows one to write
a paradox, and that proof was subsequently simplified by Hurkens. A PTS translation
can be seen in the accompanying hurkens.pts.
Note that it is the impredicativity of □ that allows the (known) paradox, not that
* allows impredicative quantification over members of △. The above impredicative
tower system allows quantification over arbitrarily high universes in *, but does
not allow Girard's paradox.