haskell - このHaskellフィルターが終了するのはなぜですか？

Question

次のHaskellコードがGHCiで終了する理由がわかりません。

let thereExists f lst = (filter (==True) (map f lst)) /= []
thereExists (\x -> True) [1..]

2番目の引数が無限であることを考えると、フィルターの呼び出しが完了するとは思っていませんでした。また、lhsが完全に計算されるまで、比較が行われるとは思いませんでした。何が起こっていますか？

Answer 1

比較は、LHSが完全に計算される前に行うことができます。filter1つの要素を生成するとすぐ/=に、リストはおそらく等しいとは言えないと結論付けて、[]すぐにを返すことができTrueます。

/=リストには次のように実装されます。

(/=) :: Eq a => [a] -> [a] -> Bool
[] /= []         = False
[] /= (y:ys)     = True
(x:xs) /= []     = True
(x:xs) /= (y:ys) = (x /= y) || (xs /= ys)

Haskellは怠惰なので、どちらの右側を使用するかを選択するために必要なだけ引数を評価します。あなたの例の評価は次のようになります：

    filter (== True) (map (\x -> True) [1..]) /= []
==> (True : (filter (== True) (map (\x -> True) [2..]))) /= []
==> True

/=の最初の引数がであることがわかるとすぐに、上記のコード(1 : something)の3番目の方程式と一致するため、を返すことができます。/=True

ただし、試してみthereExists (\x -> False) [1..]ても実際には終了しません。その場合、filter一致するコンストラクターの作成に向けて進展が見られないためです。

     filter (== True) (map (\x -> False) [1..]) /= []
==>  filter (== True) (map (\x -> False) [2..]) /= []
==>  filter (== True) (map (\x -> False) [3..]) /= []
...

など、無限に。

結論としてthereExists、無限リストTrueでは有限時間で戻ることができますが、決して戻ることはありませんFalse。