Есть ли какая-либо гарантия относительно порядка оценки в соответствии с шаблоном?

Question

Следующие

(&&) :: Bool -> Bool -> Bool
False && _ = False
True && False = False
True && True = True

имеет желаемое свойство короткого замыкания False && undefined ≡ False, Первый пункт, который не является строгим в правильном аргументе, гарантированно будет проверен, прежде чем что-либо еще будет проверено.

Судя по всему, это все еще работает, если я изменяю порядок и даже не выполняю функцию

both :: (Bool,Bool) -> Bool
both (True,False) = False
both (True, True) = True
both (False, _) = False

Prelude> both (False, undefined)
False

но действительно ли это гарантировано стандартом? В отличие от порядка предложений, порядок оценки шаблонов здесь не так ясен. Могу ли я быть уверен, что соответствие (True,False) будет прерван, как только (False,_) определяется, прежде чем элемент snd будет оценен вообще?

Answer 1

Да, гарантируется, что при оценке выражения both (False, undefined) не будет расходиться, так как сопоставление конструкторов данных гарантированно сопоставит компоненты слева направо с компонентом конструктора, и шаблон завершится неудачно, как только произойдет сбой некоторого под-шаблона. Поскольку первый элемент кортежа False, шаблон не удастся для обоих (True, ...) ветви, как только первый элемент не соответствует.

Согласно докладу Haskell 2010, раздел 3.17.2, который дает неформальную семантику сопоставления с образцом:

5. Сопоставление шаблона con pat1 … patn со значением, где con - это конструктор, определенный данными, зависит от значения:
   • Если значение имеет форму con v1… vn, подшаблоны сопоставляются слева направо с компонентами значения данных; если все совпадения успешны, общее совпадение успешно; первый отказ или расхождение приводит к сбою или расхождению общего совпадения соответственно.
   • Если значение имеет вид con ′ v1… vm, где con - это другой конструктор, отличный от con ′, совпадение не выполняется.
   • Если значение равно ⊥, совпадение расходится.

Поскольку синтаксис кортежа является просто синтаксическим сахаром особого случая для конструктора данных, применимо вышеизложенное.

Более подробное описание сопоставления с образцом см. В разделе 3.17.3 отчета Haskell 2010, в котором приведена формальная семантика сопоставления с образцом (в частности, рисунок 3.2 относится к этому вопросу).

Другим интересным ресурсом является статья " Управляемое шаблоном сокращение в Haskell", в которой семантика задается как интерпретатор (написанный на Haskell) представления абстрактного синтаксиса конкретного синтаксиса Haskell (функция mP на рисунке 3 страница 7 относится к вопросу).