I am trying to translate this JS fixed-point operator into Haskell.

JS:

const fix = F => {
    const D = X => F(
        t => X(X)(t)
    )
    return D(D)
};

My attempt is (Haskell):

fix' f = d d
  where
    d x = f (\t -> x x t)

However, I get the following error:

Couldn't match expected type ‘(t2 -> t3) -> t4’
              with actual type ‘p’
because type variables ‘t2’, ‘t3’, ‘t4’ would escape their scope
These (rigid, skolem) type variables are bound by the inferred type of d :: (t1 -> t2 -> t3) -> t4

Does someone know what's happening here ?

CodePudding user response：

In the self-application d d, d is both a function, of some type a -> r, and its argument, of type a. Thus the two types must be one and the same, a ~ (a -> r).

Haskell wants to know its types in full upfront so it keeps substituting one for another ending up with an infinite type.

Infinite types aren't allowed in Haskell, but recursive types are allowed.

All we need to do here is to name that recursive type:

newtype T r = D { app :: T r -> r }

Now T r is both a type of a function and its argument, for some result type r.

Here T is a type constructor, and D its data constructor, D :: (T r -> r) -> T r.

The above record syntax defines a new data type (here though with the keyword newtype, not data) and names its single field as app. It also defines app as an accessor function, app :: T r -> (T r -> r). _{(It's kind of an inverse of D, and oftentimes one sees such functions named with the prefix of "un", like app could have been named unD. But here app makes sense, as we will see later.)}

For a value x of type T r, x :: T r, this means that x is / matches up with / some value D g where (g = app x) :: T r -> r, i.e. app simply unwraps the data constructor D to get to the underlying value (a function) g: x = D g ; app x = app (D g) = g. That's how the record syntax works in Haskell.

Now we can write

{- fix' f = d d
     where
       d x = f (\t -> x x t)   -- applying x to x can't be typed!
-}

fix1 :: ((t1 -> t) -> t1 -> t) -> t1 -> t
fix1 f = d (D d)
  where
    d x = f (\t -> app x x t)   -- `app`ing x to x is well-typed!

fix2 :: ((t1 -> t) -> t1 -> t) -> t1 -> t
fix2 f = d (D d)
  where
    d (D y) = f (\t -> y (D y) t)

fix3 :: ((t1 -> t) -> t1 -> t) -> t1 -> t
fix3 f = f (\t -> d (D d) t)
  where
    d (D y) = f (\t -> y (D y) t)

fix4 :: (t -> t) -> t
fix4 f = f (d (D d))
  where
    d (D y) = f (y (D y))

all work. The last one even has the same type as the built-in fix.

But Haskell doesn't only have recursive types. It also has recursion itself. An entity is allowed to refer to itself in its own definition.

Thus as the comments say we don't really need to emulate recursion by self-application of a value passed as an argument. We can just use recursively the function being defined, itself:

fix0 :: (t -> t) -> t
fix0 f  =  f (fix0 f)

Or we can use a recursively defined value:

y :: (t -> t) -> t
y f  =  x  where  { x = f x }

Regarding the error, the second type error you get,

prog.hs:3:22: error:
    • Occurs check: cannot construct the infinite type:
        t1 ~ t1 -> t2 -> t3
    • In the first argument of ‘x’, namely ‘x’
      In the expression: x x t
      In the first argument of ‘f’, namely ‘(\ t -> x x t)’
    • Relevant bindings include
        t :: t2 (bound at prog.hs:3:15)
        x :: t1 -> t2 -> t3 (bound at prog.hs:3:7)
        d :: (t1 -> t2 -> t3) -> t4 (bound at prog.hs:3:5)
  |
3 |     d x = f (\t -> x x t)
  |                      ^

seems more to-the-point / helpful / than the one you included.