[Ur] Ur and full dependent types system

[Adam Chlipala]

Alexander Gryzlov wrote:
> Can anyone tell where in the lambda cube falls Ur's type system? I
> understand that it is not a fully dependently typed system, but what's
> missing? Type-level unions maybe?
>    

Many people have very different definitions of "dependent types" than 
the one I like to use.  My definition is that a type system is dependent 
when types can contain values that aren't determined until runtime.  
This is a bit imprecise; a heavier definition works in terms of the idea 
of a directed graph of the different syntactic classes in a programming 
language, with "describes" edges between them.  For instance, in ML, 
types "describe" expressions, but expressions do not "describe" types.  
In contrast, the Calculus of Constructions has just one syntactic class 
which is used to describe itself.  A type system is dependent when the 
"describes" graph has a cycle.

According to this definition, Ur just doesn't have dependent types.  No 
qualifications about "full" or whatever else.

Ur is a superset of System F_omega.  I'm not so familiar with the 
details of the lambda cube, but I believe F_omega falls on it.  Ur 
should fall in the same corner.