[TYPES] Y-combinator in Type:Type?

[Andreas Abel]

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

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/