[TYPES] Y-combinator in Type:Type?

Pierre Hyvernat pierre.hyvernat at univ-savoie.fr
Fri May 16 10:38:29 EDT 2008


> 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


More information about the Types-list mailing list