推論型は無限ループを検出しているように見えますが、実際には何が起こっているのでしょうか?

StackOverflow https://stackoverflow.com/questions/1830005

質問

アンドリュー・ケーニッヒ氏の作品では ML 型推論に関する逸話, 、著者はの実装を使用します マージソート ML の学習演習として使用しており、「間違った」型推論を見つけて喜んでいます。

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

'a list -> int list

つまり、このソート関数は任意の型のリストを受け入れ、整数のリストを返します。

それは不可能。出力は入力の順列である必要があります。どうして違うタイプがあり得るのでしょうか？読者は私の最初の衝動にきっと馴染みがあるでしょう。コンパイラのバグを発見したのではないかと思いました。

もう少し考えた後、関数がその引数を無視できる別の方法があることに気付きました。おそらくまったく戻らないこともありました。実際、試してみると、まさにそのとおりでした。 sort(nil) 戻ってきました 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]

どうやって ダマス・ヒンドリー・ミルナーアルゴリズム このタイプだと推測しますか？

役に立ちましたか？

解決

これは確かに注目に値する例です。無限ループは基本的に次の時点で検出されます。 コンパイル時間！この例のヒンドリー・ミルナー推論には特別なことは何もありません。いつも通りに進むだけです。

ghc は次のタイプを取得することに注意してください。 split そして merge 正しく:

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

さて、ということになると、 mergesort, 、一般に、それは関数 t です。1→t2 一部のタイプでは1 そして、2. 。次に、最初の行が表示されます。

mergesort [] = []

そして、それが1 そして、2 リスト型である必要があります。たとえば、1=[t3]とt2=[t4]。したがって、マージソートは関数 [t3]→[t4]。次の行 

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

それは次のように伝えます。

  • xs は分割する入力でなければなりません。つまり、ある a に対してタイプ [a] である必要があります (a=t の場合はすでにそうなっています)。3).
  • それで p そして q タイプも [t3]、 以来 split [a]→([a],[a])です
  • mergesort p, したがって、(マージソートのタイプは [t3]→[t4]) のタイプは [t4].
  • mergesort q タイプは [t4] 全く同じ理由です。
  • として merge タイプがあります (Ord t) => [t] -> [t] -> [t], 、および式の入力 merge (mergesort p) (mergesort q) どちらもタイプ [t4』、タイプt4 入っている必要があります Ord.
  • 最後に種類は、 merge (mergesort p) (mergesort q) は両方の入力と同じです。つまり [t4]。これは、以前から知られているタイプ [t3]→[t4] のために mergesort, したがって、これ以上行うべき推論はなくなり、ヒンドリー・ミルナーアルゴリズムの「統合」部分が完了します。 mergesort タイプは [t3]→[t4]とt4 で Ord.

そのため、次のことが得られます。

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

(論理推論に関する上記の説明は、アルゴリズムの動作と同等ですが、アルゴリズムが従う具体的なステップのシーケンスは、たとえば、Wikipedia ページに記載されているものにすぎません。)

他のヒント

それはあなたが順番にオードの型クラスの一部であるmergesort、とリストの頭部を比較する、mergeする<の結果を渡すことを見ているので、

その型を推論することができます。だから、型推論は、それがオードのインスタンスのリストを返す必要があることを理由することができます。それは実際に無限に再帰するのでもちろん、我々はそれが実際には戻らないタイプについて何かを推測することはできません。

ライセンス： CC-BY-SA と 帰属
所属していません StackOverflow
scroll top