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.
_______________________________________________ Ur mailing list [email protected] http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
