[TYPES] Universe Polymorphism

[Xavier Leroy]

> What are the practical implications of having "type:type"? I read
> that it destroys the consistency of the type system as a logic, but
> this is not relevant for my purposes.

There is an old technical report by Luca Cardelli that discusses
Type:Type from a programming language viewpoint:

http://lucacardelli.name/Papers/TypeType.A4.pdf

I don't think Cardelli implemented these ideas -- the Quest language
that he designed and implemented shortly after was stratified into
terms, types and kinds, probably because it was an imperative language
(see below).

> On one hand, I have read that type-checking in systems with
> "type:type" is not decidable

Here is my (limited) understanding of the problem, from a programming
language viewpoint.  Apologies for the inaccuracies.

- Even for a restricted language of terms (no fixed-point operator),
various paradoxes can be encoded with Type:Type, establishing
undecidability of type-checking.  However, the programmer has to go
to a long way to run into undecidability.  In this respect, this is
no worse than other programming languages where type-checking is
also undecidable "in corner cases", such as full F_sub, the C++
template language, or OCaml's higher-order functors.

- If the term language contains general recursive functions, as seems
necessary for a fully-fledged programming language, it is much
easier to run into undecidability, since arbitrary computations can
be performed at compile-time at the type level.  Stratification could
then become desirable, e.g. have general recursion at the bottom
level but only structural recursion at higher levels.

- If the term language contains imperative features such as ML's
references, I'd be worried that the type system could become
unsound.  Stratification appears necessary to confine imperative
features to a bottom level of computations.  For an example of such
stratification, see e.g. the work by Zhong Shao and his group:

http://flint.cs.yale.edu/flint/publications/tscb-toplas.html


Hope this helps,

- Xavier Leroy