25

Andrew Koenig のAn anecdote about ML type inferenceで、著者はマージ ソートの実装を ML の学習演習として使用し、「正しくない」型推論を発見して喜んでいます。

驚いたことに、コンパイラは次のタイプを報告しました。

'a list -> int list

つまり、このソート関数は、あらゆるタイプのリストを受け入れ、整数のリストを返します。

それは不可能です。出力は入力の順列でなければなりません。どのように異なるタイプを持つことができますか? 読者はきっと、私の最初の衝動に親しみを覚えるでしょう。コンパイラのバグを発見したのではないかと思ったのです!

もう少し考えてみたところ、関数が引数を無視する別の方法があることに気付きました。確かに、私が試してみたところ、まさにそれが起こったのです: sort(nil)return でしたnilが、空でないリストを並べ替えると、無限再帰ループに入ります。

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 は同様の型を推論します:

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

Damas-Hindley-Milner アルゴリズムはどのようにこの型を推測しますか?

4

2 に答える 2

30

これは確かに顕著な例です。基本的に、コンパイル時に無限ループが検出されます。この例の Hindley-Milner 推論について特別なことは何もありません。いつも通りに進むだけです。

ghc は と の型を正しく取得することに注意してsplitくださいmerge:

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

さて、 に関して言えばmergesort、それは、一般に、いくつかの型 t 1および t 2に対する関数 t 1 →t 2です。次に、最初の行が表示されます。

mergesort [] = []

そして、t 1と t 2がリスト型でなければならないことを認識します。t 1 =[t 3 ] と t 2 =[t 4 ] とします。したがって、mergesort は関数 [t 3 ]→[t 4 ] でなければなりません。次の行

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

次のように伝えます。

  • xs は、split への入力、つまり、いくつかの a の [a] 型でなければなりません (これは既に a=t 3の場合です)。
  • [ a]→([a],[a]) であるため、pとqも [t 3 ]型です。split
  • mergesort pしたがって、(mergesort は [t 3 ]→[t 4 ]型であると考えられていることを思い出してください) は [t 4 ] 型です。
  • mergesort qまったく同じ理由で[t 4 ] 型です。
  • mergeが type(Ord t) => [t] -> [t] -> [t]を持ち、式の入力merge (mergesort p) (mergesort q)が両方とも [t 4 ] 型であるため、型 t 4はin でなければなりませんOrd。
  • 最後に、 の型はmerge (mergesort p) (mergesort q)両方の入力、つまり [t 4 ] と同じです。これは、以前に知られていた型 [t 3 ]→[t 4 ] formergesortに適合するため、これ以上推論を行う必要はなく、Hindley-Milner アルゴリズムの「統一」部分が完了します。mergesortは [t 3 ]→[t 4 ] 型で、t 4は inOrdです。

それがあなたが得る理由です：

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

(論理的推論に関する上記の説明は、アルゴリズムが行うことと同じですが、アルゴリズムがたどる具体的な一連のステップは、たとえばウィキペディアのページに記載されているものにすぎません。)

于 2009-12-02T02:13:28.690 に答える
2

mergesortその型は、の結果をに渡すことがわかるため、推測できますmerge。これにより、リストの先頭が<Ord型クラスの一部であると比較されます。したがって、型推論は、Ordのインスタンスのリストを返さなければならないことを推論できます。もちろん、実際には無限に繰り返されるため、実際に返されないタイプについては他に何も推測できません。

于 2009-12-02T01:40:26.363 に答える