[TYPES] Y-combinator in Type:Type?

[Francois Pottier]

Hello,

On Fri, May 16, 2008 at 09:36:56AM +0100, Edsko de Vries wrote:
> 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? 

There is an interesting 1987 paper by Howe about this question:

  http://ecommons.library.cornell.edu/handle/1813/6660

Howe did not settle the question. I don't know if it has been settled since?

Best regards,

-- 
François Pottier
Francois.Pottier at inria.fr
http://cristal.inria.fr/~fpottier/