4

I'm kind of stuck with an assignement concerning my exams. I want to find out the types of those two functions by applying the unifying algorithm by hand:

map map
(\x -> x >>= (\y -> y))

Could someone point me to the right direction? The only ressource I could find until now was the wikipedia entry which is not really aiding me because of the high level of abstraction.

Greetings and thank you.

s_qw23
  • 354
  • 2
  • 11
  • This is the most beginner friendly source I've found: http://cs.brown.edu/courses/cs173/2012/book/types.html#(part._.Type_.Inference) and there is also this, which is a more in-depth explanation http://web.cecs.pdx.edu/~antoy/Courses/TPFLP/lectures/TYPE/BasicTypechecking.pdf – Wes Jun 17 '13 at 14:51

2 Answers2

5

Let's just do the first.

map :: (a -> b) -> [a] -> [b]

Now we can write it again with two different names, for clarity:

map :: (c -> d) -> [c] -> [d]

Now we substitute the second as the first parameter of the first, getting:

(a -> b) === (c -> d) -> ([c] -> [d]) (recall the associativity of (->))
a === (c -> d)
b === ([c] -> [d])

Now we substitute those type assignments into the remaining portion of the first signature, getting

map map :: [c -> d] -> [[c] -> [d]]

Clear?

sclv
  • 38,665
  • 7
  • 99
  • 204
  • I think they were asking for an explanation of type unification in general as well. – Wes Jun 17 '13 at 14:49
  • 1
    Thank you very much. This explenation was exactly what I was searching for. It was the right-associtivity I missed all the time. Great post. – s_qw23 Jun 17 '13 at 15:00
1

The type of map is map :: (a -> b) -> [a] -> [b]. Hence the type of map foo is obtained from [a] -> [b] by substituting a and b with what can be derived from foo's type. If, for example, foo :: t -> t, you substitute a = t, b = t and obtain [t] -> [t]. If foo :: [t] -> Int, you obtain [[t]] -> [Int].

In your case, the type of foo (which is map) is (x -> y) -> [x] -> [y]. You have to unify that type with a -> b to find out what a and b have to be substituted with. [Note that the function arrow is right-associative, x -> y -> z = x -> (y -> z).]

To find the type of

\x -> x >>= (\y -> y)

use the known type of (>>=) :: Monad m => m a -> (a -> m b) -> m b. Ignore the constraint (Monad m =>) for now.

As the first argument of (>>=), x must have a type m a for as yet unknown m and a. The second argument of (>>=) is here the identity,

(\y -> y) :: t -> t

so you must unify t -> t with a -> m b. That gives you some information about a, namely a = m b.

That gives x :: m (m b), and (\x -> x >>= (\y -> y)) :: type_of_x -> type_of_rhs.

Finally remember the temporarily forgotten constraint Monad m =>.

Daniel Fischer
  • 181,706
  • 17
  • 308
  • 431