How can I write self-application function in Haskell?

Question

I tried following code, but it generates type errors.

sa f = f f

• Occurs check: cannot construct the infinite type: t ~ t -> t1
• In the first argument of ‘f’, namely ‘f’
  In the expression: f f
  In an equation for ‘sa’: sa f = f f
• Relevant bindings include
    f :: t -> t1
      (bound at fp-through-lambda-calculus-michaelson.hs:9:4)
    sa :: (t -> t1) -> t1
      (bound at fp-through-lambda-calculus-michaelson.hs:9:1)

Answer 1

Use a newtype to construct the infinite type.

newtype Eventually a = NotYet (Eventually a -> a)

sa :: Eventually a -> a
sa eventually@(NotYet f) = f eventually

In GHC, eventually and f will be the same object in memory.

Answer 2

I don't think there is a single self-application function that will work for all terms in Haskell. Self-application is a peculiar thing in typed lambda calculus, which will often evade typing. This is related to the fact that with self-application we can express the fixed-point combinator, which introduces inconsistencies into the type system when viewed as a logical system (see Curry-Howard correspondence).

You asked about applying it to the id function. In the self application id id, the two ids have different types. More explicitly it's (id :: (A -> A) -> (A -> A)) (id :: A -> A) (for any type A). We could make a self-application specifically designed for the id function:

sa :: (forall a. a -> a) -> b -> b
sa f = f f

ghci> :t sa id
sa id :: b -> b

which works just fine, but is rather limited by its type.

Using RankNTypes you can make families of self-application functions like this, but you're not going to be able to make a general self-application function such that sa t will be well-typed iff t t is well-typed (at least not in System Fω ("F-omega"), which GHC's core calculus is based on).

The reason, if you work it out formally (probably), is that then we could get sa sa, which has no normal form, and Fω is known to be normalizing (until we add fix of course).

Answer 3

This is because the untyped lambda calculus is in some way more powerful than Haskell. Or, to put it differently, the untyped lambda calculus has no type system. Thus, it has no sound type system. Whereas Haskell does have one.

This shows up not only with self application, but in any cases where infinite types are involved. Try this, for example:

i x = x
s f g x = f x (g x)
s i i

It is astonishing how the type system finds out that the seemingly harmless expresion s i i should not be allowed with a sound type system. Because, if it were allowed, self application would be possible.