[TYPES] Y-combinator in Type:Type?

Francois Pottier Francois.Pottier at inria.fr
Fri May 16 10:55:49 EDT 2008


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:


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

More information about the Types-list mailing list