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

Question

In Andrew Koenig's An anecdote about ML type inference, the author uses 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 Hindley-Milner algorithm infer this type?

Answer 1

That type can be inferred because it sees that you pass the result of mergesort to merge, which in turn compares the heads of the lists with <, which is part of the Ord typeclass. So the type inference can reason that it must return a list of an instance of Ord. Of course, since it actually recurses infinitely, we can't infer anything else about the type it doesn't actually return.

Answer 2

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 t₁→t₂ for some types t₁ and t₂. Then it sees the first line:

mergesort [] = []

and realizes that t₁ and t₂ must be list types, say t₁=[t₃] and t₂=[t₄]. So mergesort must be a function [t₃]→[t₄]. 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=t₃).
• So p and q are also of type [t₃], since split is [a]→([a],[a])
• mergesort p, therefore, (recall that mergesort is believed to be of type [t₃]→[t₄]) is of type [t₄].
• mergesort q is of type [t₄] 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 [t₄], the type t₄ must be in Ord.
• Finally, the type of merge (mergesort p) (mergesort q) is the same as both its inputs, namely [t₄]. This fits with the previously known type [t₃]→[t₄] 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 [t₃]→[t₄] with t₄ 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.)

Answer 3

I wonder if the "theorems for free" approach could detect that a function with that type necessarily had to diverge.