Почему этот фильтр Haskell прекращает работу?

Я не понимаю, почему следующий код Haskell завершается в GHCi:

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

Я не ожидал, что вызов filter когда-либо завершится, учитывая, что его второй аргумент бесконечен, и я не думал, что сравнение может иметь место, пока не будет полностью вычислена левая сторона. Что творится?


person Ellen Spertus    schedule 29.10.2012    source источник
comment
Кстати, thereExists есть в стандартной библиотеке, за исключением того, что он называется any.   -  person hammar    schedule 30.10.2012
comment
У меня были студенты, которые написали свою версию thereExists в качестве контрольного вопроса. Я сказал одному студенту, что его версия (выше) не заканчивается, и он сказал мне, что это так. Он был прав, и теперь я понимаю, почему.   -  person Ellen Spertus    schedule 30.10.2012
comment
Также обратите внимание, что [1..] не должно быть бесконечным. С типом по умолчанию [Integer] это так, но это также может быть [Int], который обычно имеет 2 ^ 31-1 или 2 ^ 63-1 элементов.   -  person Tener    schedule 30.10.2012


Ответы (1)


Сравнение может выполняться до полного расчета LHS. Как только filter создал один элемент, /= может сделать вывод, что список не может быть равен [], и немедленно вернуть 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), он соответствует третьему уравнению для /= в приведенном выше коде, поэтому мы можем вернуть 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.

person hammar    schedule 29.10.2012
comment
Спасибо. Можете ли вы рассказать мне что-нибудь о том, как реализуется эта магия? Является ли /= встроенным в Haskell или его можно написать на Haskell? - person Ellen Spertus; 30.10.2012
comment
@espertus Это можно написать на Haskell - и это так. Он определяется как xs /= ys = not (xs == ys), а (==) задается как [] == [] = True; (x:xs) == (y:ys) = x == y && xs == ys; _ == _ = False. - person Daniel Fischer; 30.10.2012
comment
@espertus Это просто нестрогая оценка. В этом деле нет ничего особенного. Так работает Haskell в целом. - person Ben; 30.10.2012