-- 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.