Clarification on a Haskell function type argument

Question

On a recent worksheet I was asked to explain why the function f, in: f g x = g (g x) x has no type.

I'm quite new to Haskell and I'm quite confused by how could one work out the association orders of the left and right expressions without knowing any details about the functions. It seems like that g should be defined as:

g :: a -> b, supposing that the type of x was a - however that seems to lead to trouble immediately as on the RHS, g (g x) x seems to imply g takes 2 arguments, one of type b and one of type a. Moreover I'm also stuck as to how to read the LHS also, i.e. does f take in 2 arguments: a function g and a variable x or does it take in simply 1 argument, (g x)?

I'm wondering if anyone could enlighten me as to how these expressions should be read?

Answer 1

1. Function application is left associative: a b c parses as (a b) c
2. Function definitions are syntactic sugar for lambda expressions: f x y = ... means f = \x y -> ...
3. Lambdas with multiple arguments are curried automatically: \x y -> ... means \x -> (\y -> ...)

Thus

f g x = g (g x) x

means

f = \g -> (\x -> (g (g x)) x)

Now let's try to derive the type of f. Let's give it a name:

f :: ta

But what exactly is ta? f is defined as a lambda, so its type involves -> (it's a function):

\g -> (\x -> (g (g x)) x) :: tb -> tc
g :: tb
\x -> (g (g x)) x :: tc

I.e. the type of \g -> ... is tb -> tc for some types tb and tc, and the type of g (the argument) is tb, and the type of the result (the function body) is tc.

And since the whole thing is bound to f, we have

ta = tb -> tc

We're not done with tc, though:

\x -> (g (g x)) x :: td -> te
x :: td
(g (g x)) x :: te

with

tc = td -> te

The function body (whose type we've called te) consists of an application of (what must be) a function to the variable x. From this it follows that:

g (g x) :: td -> te

because

x :: td
(g (g x)) x :: te

Drilling down again, we have

g :: tf -> (td -> te)
g x :: tf

because applying g to g x must have type td -> te. Finally,

g :: td -> tf

because

x :: td
g x :: tf

Now we have two equations for g:

g :: tf -> (td -> te)
g :: td -> tf

Therefore

tf       = td
td -> te = tf

tf -> te = tf

Here we run into a problem: tf is defined in terms of itself, giving something like

tf = (((((... -> te) -> te) -> te) -> te) -> te) -> te

i.e. an infinitely large type. This is not allowed, and that's why f has no valid type.

Answer 2

To be able to answer questions like this, you need to think like the Haskell compiler. We have a function.

f g x = g (g x) x

In order for this to be well-typed, we need to find the types for f, g, and x. Now, f takes two arguments, so

f :: a -> b -> c
g :: a
x :: b

We also know that g x must make sense as an expression (we would say that g x is "well formed"), so g must be a function to which x can be applied. So it is also the case that

g :: b -> t0

Where t0 is a type variable, for now. We don't know the result of g x; we just know that it "makes sense". Now, the outer g (g x) x must also make sense. So g has to be a type which we can apply g x (which has type t0, as we said before) and x (which has type b) to be able to get a result of type c (the return type of the function). So

g :: t0 -> b -> c

Now, here's where the problem happens. We see that g has three declarations: a, b -> t0, and t0 -> b -> c. In order for g to have all three of these types, they must unify. That is, they have to be able to become the same, by plugging in values for certain variables. The a poses no problems, seeing as it's a free variable and doesn't depend on anything else, so we can "set" it to whatever we want. So b -> t0 and t0 -> b -> c have to be the same. In Haskell, we write that as

(b -> t0) ~ (t0 -> b -> c)

Parentheses (in types) are right-associative, so this is equivalent to

(b -> t0) ~ (t0 -> (b -> c))

In order for two function types to be the same, their arguments must be the same, so

b ~ t0
t0 ~ (b -> c)

By the transitive property, this implies that

b ~ (b -> c)

So b is a type which takes itself as an argument. This is what Haskell calls an infinite type and is inadmissible by the current standard. So in order for that function you've written to be acceptable, b must be a type which does not exist in Haskell. Therefore, f is not a valid Haskell function.

Answer 3

The relevant rules are:

1. Application is written as juxtaposition, i.e., f x applies f to x.

2. Parentheses are used to delimit expressions, not for function application, i.e., f (g x) applies f to g x. (Where g x is itself the application of g to x.)

3. Application associates to the left, i.e., f x y = (f x) y.

Putting these together, we can see that g (g x) x = (g (g x)) x, i.e., the application of g (g x) to x, where g (g x) is itself the application of g to g x.

I should also mention that all functions in Haskell take exactly one argument. Where it appears that a function takes multiple arguments, there is really currying:

f x y z = ((f x) y) z

In other words, f is a function that takes an argument and returns a function that takes an argument and returns a function that takes an argument and returns a value. You can probably see why we sometimes prefer to lie a bit and say that a function takes multiple arguments, but it is not technically true. A function that "takes multiple arguments" is really a function that returns a function, which may return a function, and so on.