[TYPES] Y-combinator in Type:Type?

[Pierre Hyvernat]

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?
>
If I am not mistaken, this is still an open question.


Thierry Coquand and Hugo Herbelin showed how to get
"looping" combinators inside any inconsistent PTS. This
is enough for all "programming" purposes:

"A-translation and looping combinators in PTS",
Journal of Functional Programming , Volume 4, 1994.

The paper is available on Hugo Herbelin's web page...



The existence of a fixpoint combinator for *:* is said
to be open in the conclusion, and last time I asked
(about a year ago), it was still the case.



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.

(Available on Gilles Barthe's page.)



I guess more knowledgeable people will have other
suggestions (which I'd welcome)...



All the best


Pierre
--