[TYPES] Y-combinator in Type:Type?
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 ]
>> 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