How to write a self-compilation function in Haskell?

Question

I tried the following code, but it generates type errors.

sa f = ff 

 • Occurs check: cannot construct the infinite type: t ~ t -> t1 • In the first argument of 'f', namely 'f' In the expression: ff In an equation for 'sa': sa f = ff • 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

I do not think that there is one self-application function that will work for all terms in Haskell. Self-application is a peculiar thing in the typed calculus of lambda, which often avoids typing. This is due to the fact that with the help of self-application we can express a fixed-point combinator that introduces inconsistencies into the type system if we consider them as a logical system (see Curry-Howard Correspondence).

You asked to apply it to id function. In a native id id application, two id have different types. More explicitly, this is (id :: (A -> A) -> (A -> A)) (id :: A -> A) (for any type A ). We could do a self-application specifically designed for the id function:

 sa :: (forall a. a -> a) -> b -> b sa f = ff ghci> :t sa id sa id :: b -> b 

which works just fine, but pretty limited by its type.

Using RankNTypes , you can make families of self- RankNTypes functions like this, but you cannot make a general self-application function so that sa t well typed iff tt (at least not in System Fω ("F-omega"), on which GHC core calculus is based).

The reason, if you formally (possibly) work it out, is that then we could get sa sa , which does not have a normal shape, and Fω, as you know, normalizes (until we add fix , of course).

Answer 2

Use the new type to create an 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 3

This is because the untyped lambda calculus is somewhat larger than Haskell. Or, to put it another way, untyped lambda calculus does not have a type system. Thus, it does not have a sound type system. While Haskell has one.

This is manifested not only in self-service, but also in any cases when infinite types are involved. Try this for example:

 ix = x sfgx = fx (gx) sii 

It is amazing how the type system discovers that the seemingly harmless expression sii should not be allowed using the sound type system. Because, if it were allowed, the application itself could be possible.