How do I find a general type of a haskell definition?

Question

How do I determine the types for q2, and q3? The module gave me the types when I enter it in, but what's a reliable method in doing this by hand? Please help. Thank you.

q2 x y z w = w (x y) (z y)

Type is: q2 :: (a -> b) -> a -> (a -> c) -> (b -> c -> d) -> d

q3 f g x y = (f.g) x == y

Type is: q3 :: Eq a => (b -> a) -> (c -> b) -> c -> a -> Bool

Answer 1

Type information flows from existing constructs to new ones. Let's look at your example:

q2 x y z w = w (x y) (z y)

It might not be obvious, but this function already invokes some typed Haskell primitives. In particular, it uses function application which has a type

($) :: (a -> b) -> a -> b

and in fact we can use ($) syntax just like that to make our use of function application more explicit.

q2 x y z w = (w $ x $ y) $ z $ y

Or, we could reformulate it in, say, Javascript-esque syntax to see application more clearly again

q2(x)(y)(z)(w) = w(x(y))(z(y))

In any case, it should be clear that there are 4 function applications occurring. From these we'll produce the information that gives us the principal type of q2.

---

The primary method of extending type inference is "unification" which is to say that if we know a single thing has types A and B then we must be able to transform A and B into C, a third type which agrees with both A and B. It might just be either A or B even.

 | A      | B      | C      |
 |--------|--------|--------|
 | String | a      | String |
 | Int    | String | <fail> |
 | a      | b      | c      | (where we suppose a == b == c)
 | a -> b | c -> d | e -> f | (where we suppose a == c == e
 |        |        |        |               and b == d == f)

As you can see, two further features of unification: (1) it can fail if and (2) it sometimes results in us supposing equalities between type variables.

In general, that's how inference proceeds: we assign a fresh type variable to everything we don't know and then try to unify all of the pieces. Along the way we might fail (and thus we say that typechecking has failed) or we'll collect a whole bunch of equalities which tell us that we've introduced a lot of redundant type variables. We then just summarize the information by eliminating all of the redundant variables until we don't need to state our equalities anymore.

 id     :: a -> a
    3   :: Num a => a
    3   :: Num b => b       -- make the variable fresh / not conflict with `a`
 id 3   :: Num c => c   (supposing a == b == c)
 id 3   :: Num a => a   (supposing nothing, we've forgotten about b and c)

---

So we can apply this process to q2. It's a bit long-winded to do algorithmically, but easy to do by hand. We're looking for a type for the value q2. We know q2 takes 4 arguments and returns something, so we can build that type immediately

q2 :: a -> b -> c -> d -> e

We know by unifying the types of x, z, and w with the type for application ($) that the types a and c must be compatible with functions

q2 :: (f -> g) -> b -> (h -> i) -> d -> e

and that their input argument must have type compatible with their argument value y :: b

q2 :: (b -> g) -> b -> (b -> i) -> d -> e

Finally we can examine w to see that its a function which takes one argument of the type of x y and returns another function which takes an argument of the type of z y and returns something

q2 :: (b -> g) -> b -> (b -> i) -> (g -> (i -> j)) -> e

which by the right-associativity of (->) we usually write as

q2 :: (b -> g) -> b -> (b -> i) -> (g -> i -> j) -> e

Finally, we know that the return type of w is the return type of the whole function

q2 :: (b -> g) -> b -> (b -> i) -> (g -> i -> j) -> j

Which, up to renaming, is the final, most general type of q2.

---

For more information, investigate Hindley-Milner and Algorithm W. I've loosely covered most of the details, but there are a few remaining ideas and they all can be examined much more carefully.

Answer 2

Well is just about analysing what makes sense:

First we have

q2 x y z w = w (x y) (z y)

Let's break it down, from just looking at q2 x y z w we have that it takes 4 arguments, and a return type too:

q2 :: a -> b -> c -> d -> e

now we look at each of these, we have w (x y) (z y), let's split it in smaller pieces:

• (x y) : We are using x as a function and y as the argument of said function, so x has a type x :: b -> f. So q2 now looks like this:

  q2 :: (b -> f) -> b -> c -> d -> e
  

• (z y): has the same style so we can say the same we said about x, but we don't know if x and z return the same type, so z would look like this z :: b -> g. Making q2 look like this:

  q2 :: (b -> f) -> b -> (b -> g) -> d -> e
  

  Note: (b -> f) and (b -> g) return different types, because there's no indication (at least until now) that they return the same type.

• w (x y) (z y): here we use w as a function, taking as arguments (x y) and (z y), so now w has a type w :: f -> g -> h. Making q2:

  q2 :: (b -> f) -> b -> (b -> g) -> (f -> g -> h) -> e
  

  Note: w takes arguments of the return types of x and z.

• q2 x y z w = w (x y) (z y): we can see that the last thing this function does is use w as a function, so what w returns is what q2 should return, so finally q2 looks like this:

  q2 :: (b -> f) -> b -> (b -> g) -> (f -> g -> h) -> h
  

---

Hope it helps, you should do q3 on your own to practice. Let me know if you have difficulties.

Answer 3

A good paper to gain insights into Haskell's type system is also "Typing Haskell in Haskell", where you can actually see how the Hindley-Milner type inference can be done by a program. http://web.cecs.pdx.edu/~mpj/thih/

Since Haskell is strongly typed, you can always infer all types of all functions, starting from the assumption of an unrestricted type variable, which may become restricted to a more concrete type or type class by the context (other functions that require a specific type).

J. Abrahamson explained it very well. :)