[TYPES] Y-combinator in Type:Type?

Herman Geuvers herman at cs.ru.nl
Fri May 16 10:50:33 EDT 2008

```Edsko de Vries wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Hi,
>
> 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?
>
>

No but you can define a family of looping combinators:
Y_0, Y_1, Y_2 ...
satisfying the property
Y_i F = F(Y_{i+1} F)

This is proven in* A-translation and Looping Combinators in Pure Type
Systems by Thierry Coquand, Hugo Herbelin, Journal of Functional
Programming (1994)***

This is enough to type all partial recursive functions.
(For the know proof of representation of recursive functions in lambda
calculus, a looping combinator suffices.)

Using the short proof of inconsistency by Hurkens, one can actually
exhibit such a looping combinator, and if you look at the underlying
"Curry variant" of it (which you can exhibit in the system lambda-U),
then it is a fixed point combinator indeed. So the looping occurs just
because the type information in the term gets bigger and bigger; the
underlying untyped term is a fixed-point combinator. See also an old
note of mine, where the latter result is just mentioned without proof.

Best Regards

Herman Geuvers

Reference:
||A. J. Hurkens, "A simplification of Girard's paradox", Proceedings of
the 2nd international conference Typed Lambda-Calculi and Applications
(TLCA'95), 1995.

H. Geuvers,
Inconsistency of classical logic in type theory,
<http://www.cs.ru.nl/%7Eherman/PUBS/newnote.ps.gz> Short Note (Version
of November 27, 2001) http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz
```

More information about the Types-list mailing list