hub.darcs.net :: dolio -> pts -> files

-- 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 <term>
  infers the type of the given term

:let <name> = <term>
  checks that the term is well typed, and adds it to the environment under
  the given name.

:tlet <name> : <term> = <term>
  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 <name> : <term>
  assumes a postulate into existence with the given name and type

:normal/:nf <term>
  computes the normal form of a term, assuming it's well-typed

:whnf <term>
  computes the weak head normal form of a term, assuming it's well-typed

:echo <term>
  parses a term, and then pretty prints it

:dump <term>
  parses a term, and dumps the abstract syntax tree (useful for debugging)

:load <file>
  loads a file, which should contain a list of commands as above. The commands
  are executed.

:{<cmd>:}
  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.

:<type system>
  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.