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

[deni_ok]

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

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]

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

[zelych]

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

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

[deni_ok]

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

> (\xs -> zip xs (tail $ tail xs)) [42]
*** Exception: Prelude.tail: empty list
Дело в том, что сопоставление с образцом всегда делается сверху вниз (по уравнениям) и слева направо (по образцам-параметрам текущего уравнения). Поэтому, если первый в текущем уравнении образец представлен конструктором, то для сопоставления соответствующий параметр передаваемый в функцию должен быть приведен в WHNF. А у zip оказывается так, что если WHNF - это пустой список, то выбирается второе уравнение, которому пофиг на второй аргумент.

[zelych]

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

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

[helvegr]

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

zip (a:as) (b:bs) = (a,b) : zip as bs
zip _ _ = []
Соответственно, zip [] (tail []) выдаёт пустой список, а zip (tail []) [] исключение.

[deni_ok]

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

zipWith (curry swap) ≡ flip zip
хотя казалось бы...

[jakobz]

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

[thedeemon]

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]

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

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

[deni_ok]

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