The Coq mailing list

[Dan Doel <dan.doel AT gmail.com>]

On Thu, Jun 16, 2011 at 5:55 PM, Vladimir Voevodsky 
<vladimir AT ias.edu>
 wrote:
> I have been looking at Barendregt's "Lambda calculi with Types" and I have 
> the following question. It seems that he is considering systems with 
> different universe arrangements but he never assumes one universe to be a 
> sub-universe of another. Is it so or am I missing something? And if this is 
> so is there a careful analysis of the analog of PST's where universes are 
> not only members but also subtypes of each other?

At least as far as universes go, there is sort of a way around needing
subtyping in pure type systems, although I must admit I completely
overlooked it myself for quite some time.

The crux is that the 'axioms' and the 'rules' (assuming I'm using the
standard terms) needn't be functional relations. So, you can get
cumulativity via axiom/rule sets like:

    (Type0, Type1)
    (Type0, Type2)
    ...

    (Type0, Type0, Type0)
    (Type0, Type0, Type1)
    ...

Essentially, you add a rule for every possible way cumulativity could be used.

The problem with 'non-functional' pure type systems like these is that
checking tends to become semi-decidable. You may eventually find a
correct choice of axioms/rules for a particular term, but you can
never get through all of them to definitively say that certain terms
are ill-typed. By contrast, 'functional' pure type systems admit
decidable checking/inference of sufficiently annotated terms.

The boon of the cumulativity/subtyping approach, like Luo's, is that
terms admit principal types, and there is an algorithm for deciding
them. Essentially, it is a slightly different treatment of a special
case of the general class of non-functional pure type systems that
admits decidable checking.

As for reading about systems with cumulativity, I recommend Luo, as others 
have.

-- Dan