Соответствие шаблону Haskell "расходятся" и ⊥

Я пытаюсь понять раздел Haskell 2010 Report 3.17.2 "Неофициальная семантика соответствия шаблонов". Большая часть из них, относящаяся к совпадению шаблонов, преуспевающая или неудачная, кажется простой, однако мне трудно понять случай, который описывается как совпадение шаблона "расходящийся".

Я полууверен, это означает, что алгоритм соответствия не "сходится" к ответу (следовательно, функция совпадения никогда не возвращается). Но если не вернется, то как он может вернуть значение, как это предлагается в скобках "i.e. return ⊥"? И что значит "возвращать ⊥" в любом случае? Как обрабатывать этот результат?

Пункт 5 имеет особенно запутанную (мне) точку "Если значение ⊥, совпадение расходится". Это просто говорит о том, что значение ⊥ дает результат соответствия ⊥? (Отметив, что я не знаю, что означает этот результат!)

Любое освещение, возможно, с примером, будет оценено!

Добавление после нескольких длительных ответов: Спасибо Тихону и всем за ваши усилия.

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

Очевидно, что "bottom" ⊥ находится в семантическом домене и не существует как значение внутри Haskell (т.е. вы не можете ввести его, вы никогда не получите результат, который выводится как "⊥" ).

Итак, когда объяснение говорит, что функция "возвращает ⊥", это относится к функции, которая выполняет любое из нескольких неудобных вещей, например, не завершает, генерирует исключение или возвращает "undefined". Правильно ли это?

Кроме того, те, кто прокомментировал, что ⊥ на самом деле является значением, которое может быть передано, действительно думают о привязках к обычным функциям, которые еще не были призваны оценивать ( "так называемые" неразорвавшиеся бомбы ") и может никогда, из-за лень, правильно?

Ответ 1

Значение ⊥, обычно произносится как "снизу". Это значение в семантическом смысле - это не обычное значение Хаскелла как таковое. Он представляет собой вычисления, которые не приводят к нормальному значению Haskell: например, исключения и бесконечные петли.

Семантика - это определение "значения" программы. В Haskell мы обычно говорим о денотационной семантике, где значение является каким-то математическим объектом. Самый тривиальный пример: выражение 10 (но также выражение 9 + 1) имеет обозначения числа 10 (а не значение Haskell 10). Обычно мы пишем, что ⟦9 + 1⟧ = 10 означает, что обозначение выражения Хаскелла 9 + 1 - это число 10.

Однако, что мы делаем с выражением типа let x = x in x? Для этого выражения нет значения Haskell. Если вы попытаетесь оценить его, это просто не закончится. Более того, неясно, какой математический объект ему соответствует. Однако для того, чтобы рассуждать о программах, нам нужно дать некоторое обозначение. Итак, по сути, мы просто составляем значение для всех этих вычислений, и мы называем значение ⊥ (внизу).

Итак, ⊥ - это просто способ определить, что вычисление, которое не возвращает "означает".

Мы также определяем другие вычисления, такие как undefined и error "some message" как ⊥, потому что они также не имеют очевидных нормальных значений. Таким образом, выбрасывание исключения соответствует ⊥. Это именно то, что происходит с неудачным совпадением шаблонов.

Обычный способ думать об этом заключается в том, что каждый тип Haskell "снят" - он содержит ⊥. То есть Bool соответствует {⊥, True, False}, а не только {True, False}. Это свидетельствует о том, что программы Haskell не гарантируют прекращения и могут иметь исключения. Это также верно, если вы определяете свой собственный тип - тип содержит каждое значение, определенное для него, а также ⊥.

Интересно, что, поскольку Haskell не является строгим, ⊥ может существовать в нормальном коде. Таким образом, у вас может быть значение типа Just ⊥, и если вы его никогда не оцените, все будет работать нормально. Хорошим примером этого является const: const 1 ⊥ оценивается до 1. Это также работает для неудачных совпадений шаблонов:

const 1 (let Just x = Nothing in x) -- 1

В Haskell WikiBook вы должны прочитать раздел денотационная семантика. Это очень доступное введение в тему, которую я лично считаю очень увлекательным.

Ответ 2

Денотационная семантика

Итак, кратко денотационная семантика, где находится ⊥, является отображением значений Haskell в другое пространство значений. Вы делаете это, чтобы придавать смысл программам более формальным образом, чем просто говорить о том, какие программы должны делать - вы говорите, что они должны уважать их денотационную семантику.

Итак, для Haskell вы часто думаете о том, как выражения Haskell обозначают математические значения. Вы часто видите скобки Strachey ⟦·⟧, чтобы обозначить "семантическое отображение" от Haskell до Math. Наконец, мы хотим, чтобы наши семантические скобки были совместимы с семантическими операциями. Например,

⟦x + y⟧ = ⟦x⟧ + ⟦y⟧

где на левой стороне + есть функция Haskell (+) :: Num a => a -> a -> a, а справа - бинарная операция в коммутативной группе. Хотя это здорово, потому что тогда мы знаем, что мы можем использовать свойства из семантической карты, чтобы знать, как работают наши функции Haskell. Для этого напишем коммутативное свойство "в Math"

  ⟦x⟧ + ⟦y⟧ == ⟦y⟧ + ⟦x⟧ 
= ⟦x + y⟧ == ⟦y + x⟧ 
= ⟦x + y == y + x⟧

где третий шаг также указывает, что Haskell (==) :: Eq a => a -> a -> a должен обладать свойствами отношения математической эквивалентности.

Ну, кроме...

В любом случае, все хорошо и хорошо, пока мы не вспомним, что компьютеры - это конечные вещи, а математика не очень заботится об этом (если вы не используете интуиционистскую логику, а затем получаете Coq). Итак, мы должны обратить внимание на места, где наша семантика не соответствует математике совершенно правильно. Вот три примера

⟦undefined⟧         = ??
⟦error "undefined"⟧ = ??
⟦let x = x in x⟧    = ??

Здесь ⊥ входит в игру. Мы просто утверждаем, что, поскольку денотационная семантика Haskell касается каждого из этих примеров, это может означать (недавно введенное математическое/семантическое понятие) ⊥. Каковы математические свойства ⊥? Ну, вот где мы начинаем действительно погружаться в то, что представляет собой семантическая область, и начать говорить о монотонности функций и CPO и т.п. По существу, однако, ⊥ - это математический объект, который играет примерно ту же игру, что и без прерывания. С точки зрения семантической модели, ⊥ токсичен и заражает выражения с его токсическим недетерминизмом.

Но это не концепция Haskell-language, а только вещь с семантическим доменом на языке Haskell. В Haskell имеем undefined, error и бесконечный цикл. Это важно.

Экстра-семантическое поведение (боковое примечание)

Итак, семантика ⟦undefined⟧ = ⟦error "undefined"⟧ = ⟦let x = x in x⟧ = ⊥ понятна, когда мы понимаем математические значения ⊥, но также ясно, что каждый из них имеет разные эффекты "на самом деле". Это похоже на "поведение undefined" поведения C..., которое undefined в том, что касается семантической области. Вы можете назвать это семантически ненаблюдаемым.

Итак, как соответствие шаблонов возвращает `⊥`?

Итак, что значит "семантически" возвращать ⊥? Ну, ⊥ - это совершенно правильное семантическое значение, обладающее свойством заражения, которое моделирует недетерминированность (или асинхронное бросание ошибок). С семантической точки зрения это вполне допустимое значение, которое может быть возвращено как есть.

С точки зрения реализации у вас есть несколько вариантов, каждая из которых соответствует одному и тому же семантическому значению. undefined не совсем прав, и он не вводит бесконечный цикл, поэтому, если вы собираетесь выбрать семантически поведение undefined, вы можете выбрать тот, который полезен, и выбросить ошибку

*** Exception: <interactive>:2:5-14: Non-exhaustive patterns in function cheers