Тонкости точной семантики сопоставления с образцом

[deniok]

Хорошая хотя и простая задачка возникла в процессе проверки домашних заданий. Чем отличается поведение следующих двух функций, и в чем причина такого отличия:

diff xs = do
    p <- zip xs (tail xs)
    return $ abs (fst p - snd p)

diff' xs = do
    p <- zip (tail xs) xs
    return $ abs (fst p - snd p)

Comments

[thedeemon.livejournal.com]

Полагаю, разница в порядке попыток вычисления первого элемента списка и наличия второго. Если передать список из одной задницы, то в одном случае получится задница, во втором исключение. Мораль: нетотальные языки - пустая трата времени. :)

[zelych.livejournal.com]

Симпатичная загадка.

Разница в том, что diff' [] вычисляет сначала tail [] и отваливается с ошибкой.
Т.е. у zip только второй аргумент лениво вычисляется.

[deni-ok.livejournal.com]

Дело не конкретно в zip, zip-то можно сфэйлить и на втором аргументе

> (\xs -> zip xs (tail $ tail xs)) [42]
*** Exception: Prelude.tail: empty list

Дело в том, что сопоставление с образцом всегда делается сверху вниз (по уравнениям) и слева направо (по образцам-параметрам текущего уравнения). Поэтому, если первый в текущем уравнении образец представлен конструктором, то для сопоставления соответствующий параметр передаваемый в функцию должен быть приведен в WHNF. А у zip оказывается так, что если WHNF - это пустой список, то выбирается второе уравнение, которому пофиг на второй аргумент.

[zelych.livejournal.com]

Ага, спасибо за пояснения.

Т.е. (если я правильно пользуюсь терминами) zip всегда строгий по первому агрументу, и иногда не строгий по второму. А сопоставление с образцом -- это причина строгости/нестрогости.

[deni-ok.livejournal.com]

Мне не очень нравится термин "строгий" по отношению к функциям с богатой семантикой. Он слишком грубо описывает действительность. Ну вот сделаю я обычную take более определенной, чем в Prelude, переставив местами два первых уравнения:

take' _ []              =  []
take' n _      | n <= 0 =  []
take' n (x:xs)          =  x : take' (n-1) xs

Раньше take была строгая по первому аргументу, а стала "иногда нестрогая":

> take undefined []
*** Exception: Prelude.undefined
> take' undefined []
[]

Но понятно, что это же совершенно маргинальное улучшение!

[udpn.livejournal.com]

>> нетотальные языки - пустая трата времени

А нетотальные языки это вообще языки?

[thedeemon.livejournal.com]

Конечно. По Хомскому, даже Go - язык.

[helvegr.livejournal.com]

zip определён как

zip (a:as) (b:bs) = (a,b) : zip as bs
zip _      _      = []

Соответственно, zip [] (tail []) выдаёт пустой список, а zip (tail []) [] исключение.

[deni-ok.livejournal.com]

Да, механизм сопоставления с образцом вносит асимметрию в симметричную с вида конструкцию. Что приводит к неуниверсальности тождества

zipWith (curry swap) ≡ flip zip

хотя казалось бы...

[jakobz.livejournal.com]

А бывают языки где такой засады нету?

[thedeemon.livejournal.com]

tail : (l : List a) -> (isCons l = True) -> List a
tail (x::xs) p = xs

zip : (l : List a) -> (r : List b) -> (length l = length r) -> List (a, b)
zip = zipWith (\x => \y => (x, y))

(List.idr) ;)

[deni-ok.livejournal.com]

С таким зипом искомого диффа не сваришь.

Здравствуйте, извините что без стука

[unstablebear.livejournal.com]

Посмотрел пристально два раза, повертел код в ghci. Насколько я понимаю, diff корректно обработает [], а diff' нет.

Re: Здравствуйте, извините что без стука

[deni-ok.livejournal.com]

Да, правильно; полезно еще понять, почему это так.

Re: Здравствуйте, извините что без стука

[unstablebear.livejournal.com]

С пониманием сложнее, да. Ну да выше разъяснили что к чему.