[TYPES] Y-combinator in Type:Type?

Andreas Abel andreas.abel at ifi.lmu.de
Fri May 16 13:35:24 EDT 2008

Pierre Hyvernat wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> Hello,
>> 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?
> Concerning this, you should also have a look at
> "Remarks on the Equational Theory of non-Normalizing
> PTS" by Thierry Coquand and Gilles Barthe,  Journal of
> Functional Programming, 14(2), 2004.

In that very paper a fixed-point combinator is given for domain-free 
*:*.  I.e., there is a fixed-point combinator if you ignore the 
type-labels in lambda-abstraction.


Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich

More information about the Types-list mailing list