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?
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