How to determine type of Haskell functions?

Question

I have stumbled upon lots of exercises that give you a function and ask for you to deduce the type of each one.

I have the following example. Please note this is not homework that I need to get done. I have the answer to this specific example and provide it below. Maybe someone can help me out in learning how to reason this kind of exercises.

The function:

h1 f g x y = f (g x y) x

The supposed type:

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

Thanks!

---

I added 27 exercises here without solutions.

Some of them have solutions included here. However, it is possible to know the type by using the GHCi command :t

Answer 1

h1 f g x y = f (g x y) x

So, taking the argument list from left-to-right:

• f is a function applied to two arguments: the first is the result of (g x y) and the second is x
  • we don't know what type the first argument is yet, so let's call it a
  • we don't know the second type either, so let's call that b
  • we also don't know the result type (so we'll call that c), but we do know this must be the type returned by h1
    • now f is a function mapping a -> b -> c
• g is a function applied to two arguments: the first is x and the second y
  • we know the first argument to g is the same as the second argument to f, so it must be the same type: we already labelled that b
  • the second argument to g is y, which we haven't assigned a placeholder type yet, so that gets the next in sequence, d
  • g's result is the first argument to f, and we already labelled that a
    • so now g is a function mapping b -> d -> a
• third argument is x, and as that's the second argument to f, we've already labelled its type b
• fourth argument is y, which is the second argument to g, so we've already labelled its type d
• the result of h1 is the result of applying f to (g x y) x, as we said before, so it has the same type, already labelled c

---

Although we worked through the argument list in order, the actual process of labeling, inferring and unifying types for each of those arguments was done by looking at the body of h1.

So, my first bullet could be elaborated as:

• f is the first argument to consider, so let's look at the body of h1 (everything after the =) to see how it's used
  • f (g x y) x means that f is applied to (g x y) x, so f must be a function
  • (g x y) is in parenthesis, which means whatever is inside those parentheses is being evaluated, and the result of that evaluation is an argument to f
  • x is just a simple argument to f, passed straight from h1's own argument list
  • so, f is a function taking two arguments

If it helps read f (g x y) x, you can consider the equivalent expression in C-like notation would be f(g(x,y), x). Here, you can see right away that f and g are functions taking two arguments, that f's first argument is whatever g returns, etc.

---

Note that the left-hand side of the expression, h1 f g x y, only gives one piece of type information by itself: h1 is a function on four arguments. The argument names themselves are just placeholders used in the right-hand side of the expression (the body of h1). The relative ordering of the arguments here just tells us how to call h1, but nothing about how h1 uses the arguments internally.

Again, here's a procedural-style equivalent (I'll use Python so I don't have to fill in any types):

def h1(f, g, x, y):
    return f(g(x,y),x)

this means exactly the same as

h1 f g x y = f (g x y) x

(with one caveat - partial application - that I suspect will only confuse matters further here).

In both cases, the declaration (left of the = in Haskell, and before the : in Python) only tells us the function name and how many arguments it takes.

In both cases, we can infer from the definition (right hand side in Haskell, the indented block after : in Python) that f and g are both functions on two arguments, that g's first argument is the same as f's second, etc. In Haskell, the compiler does this for us; Python will just complain at runtime if we call g with the wrong number of arguments, or it returns something f can't use as a first argument.

Answer 2

Determining a type of a function depends on the type system used. Most of functional programming languages are based on Hindley-Milner type system for which there is a type inference algorithm (called also Hindley-Milner). For a given expression the algorithm derives so-called principial type, which is basically the most general type the function can have, or fails, if the expression is untypable. This is what GHCi uses when you type in :t expression.

Hindley-Milner type system allows polymorphic functions, but all universal quantifiers have to be outside of the type. (Normally you don't see the quantifiers when working with types; the quantifiers are omitted and they are only assumed.) For example, const has type a -> (b -> a), which could be written with quantifiers as (∀a)(∀b)(a -> (b -> a)). However, H-M doesn't allow types like (∀a)(a -> (((∀b)b) -> a))

There are more expressive type system, such as System F, which allows universal quantifiers for type variables anywhere, but its type inference is undecidable, and there is no proper notion of a principial type. There are various language extensions in GHC that allow you to use such types, but then you lose the type inference, you have to explicitly annotate your functions with types.

For example: In H-M the function xx = \f -> f f is untypable (try it in GHCi). But in a type system that allows universal type quantifiers everywhere, it has a type. In Haskell with a proper GHC extension, you can write:

{-# LANGUAGE RankNTypes #-}

xx :: (forall a. a -> a) -> (forall b. b -> b)
xx = \f -> f f

(Note that RankNTypes allow you to write such quantified types, but cannot give you type inference for such functions - you have to state the type yourself.)

Hindley-Milner type system is a good trade-off: it allows polymorphic functions together with type inference.

If you're interested, you can read the original paper. However, it contains some typos so you have to be alert when reading it.

Answer 3

If you want to do it the formal way, you can follow the inference rules of the type system. If all you have are applications, the rules of the simply typed lambda calculus will do (see section 2.3 of these lecture notes on lambda calculus).

The algorithm consists of building a deduction tree using the typing rules of the type system and then calculating the final type of the term by unification.

Answer 4

If you have nothing to go by, you go step by step deducing types from the way things are used, unifying the parts deduced. We have the definition

h f g x y = f (g x y) x

So we see that h takes four arguments of so far completely unknown types, let's call them a, b, c, d and the result type shall be called r. So the type of h must be unifiable with

a -> b -> c -> d -> r

Now we have to see what we can say about the argument types. For that, we look at the right hand side of the definition.

f (g x y) x

so f is applied to two arguments, the second of them is the third argument to h, hence we know its type is c. We know nothing yet about the type of f's first argument. The result of the application of f is the result of the application of h, so f's result type is r.

f :: u -> c -> r
a = u -> c -> r

The first argument of f on the right hand side is g x y. Thus we can deduce

g :: c -> d -> u
b = c -> d -> u

since g's arguments are the third and fourth argument of h, hence their types are known, and the result is the first argument of f.

Wrapping up,

f :: u -> c -> r
g :: c -> d -> u
x :: c
y :: d
h :: (u -> c -> r) -> (c -> d -> u) -> c -> d -> r

rename the type variables as you like.