[TYPES] Y-combinator in Type:Type?

[Karl Crary]

No.  You can define a looping combinator, but not a true fixed point 
combinator.  Doug Howe's paper "The Computational Behaviour of Girard's 
Paradox" is a good reference.

Karl Crary


Edsko de Vries wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Hi,
>
> Assuming that Type:Type (or *:*) in dependently typed languages is said
> to be inconsistent (Girard's paradox?). Does that mean that it is
> possible to define a Y combinator in such a language? 
>
> Thanks,
>
> Edsko
>
>