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