foldl foldl が principal type を持てないわけ

foldl の型は:

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

これの第一引数を foldl で束縛しようとすると何が起きるかを考えてみる。

第一引数に束縛できるはずなので foldl を (a -> b -> a) にマッチさせなければならない。 foldl の型を三つの部分に分解すると (a -> b -> a)、 a、そして [b] -> a となる。マッチングの結果、 b は単純に a となる。一方 a は (a -> b -> a) であり、かつ [b] -> a を満たす型だということになる。

これは a -> (b -> a) が [b] -> a であるという主張だから、 a は [b] に一致し、 b -> a が a に一致しなければならない。後者の a を [b] で置き換えると b -> [b] と [b] とを一致させねばならない。 (でもそれはムリ)

これをもって GHCi 6.8.2 は

Couldn't match expected type `b -> [b]' against inferred type `[b]'
In the first argument of `foldl', namely `foldl'

というエラーメッセージを吐くわけだな、きっと。

SOE Errata によると Hugs はユニフィケーションの過程で infinite type が導かれるというエラーを出すらしい。

#10. Page 72, Exercise 5.2: "foldl foldl" does not have a principal type. Hugs, for example, will complain that "unification would give infinite type."

b -> [b] と [b] が一致するということは b -> [b] から b -> (b -> [b]) を生成でき、さらに b -> (b -> (b -> [b])) が生成でき…ということで、たしかにこれは infinite type だといえよう。

type inference というのは、こういうマッチングの過程のことを言っているのだろうな。