# cannot construct the infinite type [closed]

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?

• This seems like it would be a good fit to migrate to StackOverflow. – jmite Mar 17 '17 at 21:20
• 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)). – chi Mar 23 '17 at 18:19

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.

• 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? – zero_coding Mar 18 '17 at 7:42
• 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. – jmite Mar 24 '17 at 9:12