Typing the Y combinator

Question

http://muaddibspace.blogspot.com/2008/01/type-inference-for-simply-typed-lambda.html is a concise definition of the simply typed lambda calculus in Prolog.

It looks okay, but then he purports to assign a type to the Y combinator... whereas in a very real sense the entire purpose of adding types to lambda calculus is to refuse to assign a type to things like the Y combinator.

Can anyone see exactly where his error or -- more likely -- my misunderstanding is?

Answer 1

The Y combinator in its basic form

Y f = (\x -> f (x x)) (\x -> f (x x))

just cannot be typed using the simple type system proposed in the article.

There are other, much easier but meaningful examples that cannot be typed on that level:

Take e.g.

test f = (f 1, f "Hello")

This obviously works for test (\x -> x) but we cannot give the higher-ranked type that was required here, namely

test :: (∀a . a -> a) -> (Int, String)  

But even in more advanced type systems like the GHCI extensions of Haskell which allow the above, Y is still hard to type.

So, given the possibility of recursion, we can just define and work using the fix combinator

fix f = f (fix f) 

with fix :: (a -> a) -> a

Answer 2

Typing should disallow self application, it should not be possible to find a type for (t t). If it where possible then t would have a type A -> B, and we would have A = A -> B. Since self application is part of Y combinator, its also not possible to give a type to it.

Unfortunately many Prolog systems allow a solution for A = A -> B. This happens on many grounds, either the Prolog system allows circular terms, then the unification will succeed and the resulting bindings can even further be processed. Or the Prolog system does not allow circular terms, then it depends on whether it implements an occurs check. If the occurs check is on, then unification will not succeed. If the occurs check is off, then the unification might succeed but the resulting bindings can not further be processed, most likely leading to stack overflow in printing or further unifications.

So I guess a circular unification of this type happens in the given code by the used Prolog system and it gets unnoticed.

One way to solve the issue would be to either switch on the occurs check or to replace any of the occuring unifications in the code by an explicit call to unify_with_occurs_check/2.

Best Regards

P.S.: The following Prolog code works better:

/**
 * Simple type inference for lambda expression.
 *
 * Lambda expressions have the following syntax:
 *    apply(A,B): The application.
 *    [X]>>A: The abstraction.
 *    X: A variable.
 *
 * Type expressions have the following syntax:
 *    A>B: Function domain
 *
 * To be on the save side, we use some unify_with_occurs_check/2.
 */

find(X,[Y-S|_],S) :- X==Y, !.
find(X,[_|C],S) :- find(X,C,S).

typed(C,X,T) :- var(X), !, find(X,C,S), 
                unify_with_occurs_check(S,T).
typed(C,[X]>>A,S>T) :- typed([X-S|C],A,T).
typed(C,apply(A,B),R) :- typed(C,A,S>R), typed(C,B,T), 
                unify_with_occurs_check(S,T).

Here are some sample runs:

Jekejeke Prolog, Development Environment 0.8.7
(c) 1985-2011, XLOG Technologies GmbH, Switzerland
?- typed([F-A,G-B],apply(F,G),C).
A = B > C
?- typed([F-A],apply(F,F),B).
No
?- typed([],[X]>>([Y]>>apply(Y,X)),T).
T = _T > ((_T > _Q) > _Q)