6
$\begingroup$

I am trying to learn haskell and could not configure it out, why following code snippet can not get compiled:

*Uncurry> applyTwice f x = f f x

<interactive>:14:20: error:
    • Occurs check: cannot construct the infinite type:
        t ~ t -> t2 -> t1
    • In the first argument of ‘f’, namely ‘f’
      In the expression: f f x
      In an equation for ‘applyTwice’: applyTwice f x = f f x
    • Relevant bindings include
        x :: t2 (bound at <interactive>:14:14)
        f :: t -> t2 -> t1 (bound at <interactive>:14:12)
        applyTwice :: (t -> t2 -> t1) -> t2 -> t1
          (bound at <interactive>:14:1)

This would be fine:

applyTwice f x = f (f x)

In haskell function application is left associative, the first code snippet would be apply like:

(f f) x

why (f f) x it is wrong?

$\endgroup$
  • 1
    $\begingroup$ This seems like it would be a good fit to migrate to StackOverflow. $\endgroup$ – jmite Mar 17 '17 at 21:20
  • $\begingroup$ Application is left associative simply means that we write f x y for ((f x) y). It is only a notational convention. It does not mean that application is associative, i.e. that ((f x) y) must be equal to (f (x y)). $\endgroup$ – chi Mar 23 '17 at 18:19
2
$\begingroup$

Okay, let's look at what we know about the type of applyTwice, $\alpha$:

  • It is given two arguments, so $\alpha = \beta_1 \to \beta_2 \to \gamma$, and $f$ has type $\beta\_1$ and $x$ has type $\beta_2$
  • $f$ is applied to $f$, so $\beta_1 = \beta_1 \to \gamma_2$
  • $(f\ f)$ is applied to $x$, so $\gamma_2 = \beta_2 \to \gamma$

The kicker here is the second equation, $\beta_1 = \beta_1 \to \gamma_2$. This equation has no finite solution, because $S \to T$ is structurally larger (uses at least one more type constructor) than either $S$ or $T$.

So the only type that satisfies this equation is infinite recursive type $\mu T\ldotp T \to \gamma_2 = ((\ldots \to \gamma\_2) \to \gamma\_2) \to \gamma\_2) \to \gamma\_2) \to \gamma\_2) \to \gamma\_2)$. But this type doesn't really have any meaning in Haskell or related type systems, and it's pretty hard represent an infinite type in finite memory in a concrete form.

Remember that $f\ f$ is giving $f$ as an argument to $f$. If you want to apply $f$ twice, you could use function composition (f . f) x, or $(f \circ f)\ x$ in math notation.

$\endgroup$
  • $\begingroup$ Yes I know, I could make a function composition. But the point that I do not understand is, why f apply to f is infinite? Can I imagine, it is a function recursion? What does so symbols mean? Can you please in a very easy way? $\endgroup$ – zero_coding Mar 18 '17 at 7:42
  • $\begingroup$ The application isn't infinite, but the type is. If you don't believe me, here's a challenge: try to think of a type for it. Without higher rank polymorphism, it's not possible. $\endgroup$ – jmite Mar 24 '17 at 9:12

Not the answer you're looking for? Browse other questions tagged or ask your own question.