Calculating types of Haskell Functions

Question

Having troubles with manually calculating types of given functions in Haskell for an exam at the weekend.

I understand the basics such as:

• i x = x :: t -> t
• k x y = x :: t -> t1 -> t

But having trouble on more complicated questions such as:

• two f x = f (f x)
• s x y z = x z (y z)

Any explanations would be much appreciated!

Answer 1

Let's look at

two f x = f (f x)

We will proceed by writing down what we know, using variables for anything we don't. Some of the things we know will be equations, and like in math, we will substitute around in the equations until we get something that we can't do anything else with.

Starting with the expression f x. f is a function, and its argument type is whatever x's type is, so:

x :: a      -- a is a new variable
f :: a -> b -- b is a new variable

These two equations say exactly what I just said in the previous sentence. Also, we created the variable b which is the type of the result of the application:

f x :: b

Now let's move on to f (f x). So the argument type of f has to be the type of f x, which we know is b, so:

f :: b -> c   -- c is a new variable
f (f x) :: c

But, of course, a function can only have one type, and we already have a type for f:

f :: a -> b   -- from above

That means that

a = b
b = c

We've reached the top level expression now. So now let's look at the types of the input variables we've found together with the expression:

f :: a -> b
x :: a
f (f x) :: c

Now we go substituting around as much as we can, expressing it with as few variables as possible (but only using equalities that we have deduced). We'll try to do it all in terms of a.

f :: a -> b
   = a -> a  -- because b = a
x :: a 
f (f x) :: c
         = b  -- because c = b
         = a  -- because b = a

And there we have it:

two :: (a -> a)    ->    a      ->       a
       ^^^^^^^^^      ^^^^^^^^^    ^^^^^^^^^^^^^^
       type of f      type of x    type of result

This is more verbose than necessary, because I repeated myself a lot, so that you could see the reasoning involved. There is a methodical way to do this, but I prefer to do it more like math, going along and discovering what I can. The methodical way usually gets me lost in a sea of variables (which is easy enough for a computer, but hard for my mortal human brain).

I hope this helped.

Answer 2

Your two and s are what as known as higher level functions, because they take functions as arguments. You already have the tools to discern their types, you just have to be willing to be a bit more abstract about it.

If you're given the expression

f x

You know the type of f is a -> b with x :: a and f x :: b. If you see

f (f x)

Then you can deduce that the output type of (f x) is the same as the input type for f. This means that a ~ b, so f :: a -> a and x :: a. If we look at the type of two, we can deduce that it follows the pattern

two :: s -> t -> u

but the first argument to two is f, which has the type a -> a, so we can plug that in as

two :: (a -> a) -> t -> u

And x is the second argument with type a, so we can plug that in

two :: (a -> a) -> a -> u

And the return type is the same as the return type of f (f x), which has the return type of f, which has the return type of a, so if we plug that in we get the final type

two :: (a -> a) -> a -> a

---

For s, we can do similarly. We start off by saying s follows the form

s :: s -> t -> u -> v

since it has 3 arguments. The expression (y z) is function application, so y must have the type y :: a -> b, with z :: a. Plugging that in to s:

s :: s -> (a -> b) -> a -> v

Then we look at x z (y z). Since y z :: b and z :: a, x is a function of two arguments, the first of type a and the second of type b, with some unknown return type c, so we can plug that in as

s :: (a -> b -> c) -> (a -> b) -> a -> c

Answer 3

In those two examples the only hints you have as to the types of the functions come from observing the application going on. In Haskell application hardly has any syntax, so I'll rewrite them a bit more obviously.

two f x = f(f(x))
s x y z = x(z)(y(z))

---

We'll now discover the types of these functions through gradual refinement. For instance, beginning with two we know that it takes in two arguments and thus must have a type which agrees with the (more general) type

two :: a -> b -> c

We also know that the a type variable above actually corresponds to a function because f is being applied to both x and f(x).

two :: (a -> b) -> c -> d

Since f is applied to x we know that here a and c must be the same.

two :: (a -> b) -> a -> d

and since we apply f again to its result f(x) we know that the result type must be the same as the input type

two :: (a -> a) -> a -> b

And finally, the result of calling f is the total result of two so d must also equal a

two :: (a -> a) -> a -> a

This uses all of the information we have in the definition and is the most general type that is compatible with the definition of two.

---

We can do basically the same process for s. We know it has 3 arguments

s :: a -> b -> c -> d

We know that the first and second arguments are functions of some kind. We see the second argument applied to a single value and the first applied to two values.

s :: (a -> b -> c) -> (d -> e) -> f -> g

We also know that the first input to both functions are the same (namely, it's z each time). This lets us infer that a, d, and f are the same type

s :: (a -> b -> c) -> (a -> d) -> a -> e

We also know that the result of calling the second function is the second argument to the first function, so b and d must be the same.

s :: (a -> b -> c) -> (a -> b) -> a -> e

Finally, the result of fully applying the first function is the final result of s so c and e are the same

s :: (a -> b -> c) -> (a -> b) -> a -> c

---

While that might be a lot to digest and kind of a blur, the thing to emphasize is that the tools I've used to solve this problem are all primitive. Effectively, I introduce arrows (->) when I see that the type got applied to some values and thus must be a function of a certain number of arguments and I unify type variables by following the values through their expression. These are sufficient tools for inferring the types of simple functions like two and s.