Miranda Type error

Question

Can anyone tell me where goes wrong?

b f x = f x (f x)

My understanding is: because f at the left takes one argument but on the right side it has two arguments?

Any more detail explanations?

Answer 1

Let's try to construct that type:

b :: ... ?

We have at least two arguments, so lets change b accordingly:

b :: a -> c -> d

The right hand side of b suggests that f is a function. Lets first concern only the first argument:

f :: c -> e

Up till now, everything fits quite nice: the first argument of list has the same type as the second argument of b. Lets continue on the right hand side.

f x (f x)

If we take f x _, we have to assume that e is e :: k -> l, that is, we take another argument. We now have

f :: c -> k -> l

Now have a look at the type of f's second argument. It's type should be the one of f x:

f x :: k -> l

So k = k -> l. That's an infinite type, which we can also see by looking at ghci's error message:

Prelude> let b f x = f x (f x)

<interactive>:2:18:
    Occurs check: cannot construct the infinite type: t1 = t1 -> t0
    In the return type of a call of `f'
    Probable cause: `f' is applied to too few arguments
    In the second argument of `f', namely `(f x)'
    In the expression: f x (f x)

The type checker gives up, as infinite type cannot be constructed by it. At the end, this happens since you apply f on a different number of arguments.

Answer 2

The compiler tries to infer the type of f. First it sees that f takes an argument x and another argument (f x), which for now we'll substitute as y. So when the compiler sees something like f x y, it infers that f has the type a -> b -> c, with x :: a, y :: b, and f x y :: c. Then it inspects y closer, seeing that its type is more specifically b -> c, since it already knows f must have a second argument. So it can now determine that b ~ b -> c. And this is where it has to stop, how can b also be b -> c? If it kept substituting b ~ b -> c, it would have an infinite recursion trying to figure out what type b is! This obviously can't work, so it throws a compile error saying that it can't construct the infinite type b = b -> c (note: the error message may use different names than b or c). The error message I get is actually pretty helpful:

Occurs check: cannot construct the infinite type: t1 = t1 -> t0
In the return type of a call of `f'
Probable cause: `f' is applied to too few arguments
In the second argument of `f', namely `(f x)'
In the expression: f x (f x)

This tells you exactly where the problem is, "namely (f x)", and gives you the probable cause "f is applied to too few arguments", saying that it "cannot construct the infinite type t1 = t1 -> t0".