Inferred type appears to detect an infinite loop, but what's really happening?

haskell, hindley-milner, ml, type-inference, type-systems

Solution

This is indeed a remarkable example; an infinite loop being detected, essentially, at compile time! There is nothing special about the Hindley–Milner inference in this example; it just proceeds as usual.

Note that ghc gets the types of `split` and `merge` correctly:

*Main> :t split
split :: [a] -> ([a], [a])
*Main> :t merge
merge :: (Ord t) => [t] -> [t] -> [t]

Now when it comes to `mergesort`, it is, in general, a function t1→t2 for some types t1 and t2. Then it sees the first line:

mergesort [] = []

and realizes that t1 and t2 must be list types, say t1=[t3] and t2=[t4]. So mergesort must be a function [t3]→[t4]. The next line

mergesort xs = merge (mergesort p) (mergesort q) 
  where (p,q) = split xs

tells it that:

- xs must be an input to split, i.e., of type [a] for some a (which it already is, for a=t3).

- So `p` and `q` are also of type [t3], since `split` is [a]→([a],[a])

- `mergesort p`, therefore, (recall that mergesort is believed to be of type [t3]→[t4]) is of type [t4].

- `mergesort q` is of type [t4] for exactly the same reason.

- As `merge` has type `(Ord t) => [t] -> [t] -> [t]`, and the inputs in the expression `merge (mergesort p) (mergesort q)` are both of type [t4], the type t4 must be in `Ord`.

- Finally, the type of `merge (mergesort p) (mergesort q)` is the same as both its inputs, namely [t4]. This fits with the previously known type [t3]→[t4] for `mergesort`, so there are no more inferences to be done and the "unification" part of the Hindley–Milner algorithm is complete. `mergesort` is of type [t3]→[t4] with t4 in `Ord`.

That's why you get:

*Main> :t mergesort 
mergesort :: (Ord a) => [t] -> [a]

(The description above in terms of logical inference is equivalent to what the algorithm does, but the specific sequence of steps the algorithm follows is simply that given on the Wikipedia page, for example.)

Problem

In Andrew Koenig’s An anecdote about ML type inference, the author uses implementation of merge sort as a learning exercise for ML and is pleased to find an “incorrect” type inference. Much to my surprise, the compiler reported a type of ``` 'a list -> int list ``` In other words, this sort function accepts a list of any type at all and returns a list of integers. That is impossible. The output must be a permutation of the input; how can it possibly have a different type? The reader will surely find my first impulse familiar: I wondered if I had uncovered a bug in the compiler! After thinking about it some more, I realized that there was another way in which the function could ignore its argument: perhaps it sometimes didn't return at all. Indeed, when I tried it, that is exactly what happened: `sort(nil)` did return `nil`, but sorting any non-empty list would go into an infinite recursion loop. When translated to Haskell ``` split [] = ([], []) split [x] = ([x], []) split (x:y:xs) = (x:s1, y:s2) where (s1,s2) = split xs merge xs [] = xs merge [] ys = ys merge xx@(x:xs) yy@(y:ys) | x < y = x : merge xs yy | otherwise = y : merge xx ys mergesort [] = [] mergesort xs = merge (mergesort p) (mergesort q) where (p,q) = split xs ``` GHC infers a similar type: ``` *Main> :t mergesort mergesort :: (Ord a) => [t] -> [a] ``` How does the Damas–Hindley–Milner algorithm infer this type?

Original source