Какова роль "нижней" (⊥) в определениях функций Haskell?

Ответ 1

Внизу, по сути, есть фантастический алгебраический способ сказать undefined.

Если вы попробуете это, вы можете понять, почему zip ленив за свой правый аргумент:

λ> zip [] undefined
[]
λ> zip undefined []
*** Exception: Prelude.undefined

Это связано с тем, что undefined работает только при попытке оценить его.

Возможно, вы сбиваете с толку _|_ с помощью _ из-за того, как он был представлен. Я проясню: строка zip [] _|_ = [] не действует как совпадение с шаблоном, а уравнение, указывающее равенство zip [] _|_ и []. То есть это недопустимый код Хаскелла, но нотационный, абстрактно-алгебраический способ сказать: "Меня не волнует второй аргумент".

В определении zip вы можете, конечно, использовать _, но это не имеет значения. Вы могли бы использовать любое имя, до тех пор, пока оно не соответствует шаблону соответствия конструктора, например (Just x) или (a,b). Значения останутся неизменными до тех пор, пока они не будут соответствовать образцу в чистом коде.

Подробнее о ленивой оценке здесь.

Подробнее о нижнем здесь и здесь.

Ответ 2

Я думаю, что ОП уже осознает это, но на благо других, которые приходят сюда с такой же путаницей: zip [] _|_ = [] не является фактическим кодом!

Символ _|_ (который представляет собой только рендеринг математического символа ⊥ ascii-art) означает bottom ¹ но только когда мы говорим о Haskell. В коде Haskell это значение не имеет значения ².

Строка zip [] _|_ = [] представляет собой описание свойства фактического кода для zip; что если вы вызываете его с первым аргументом [] и передаете любое нижнее значение в качестве второго аргумента, результат равен []. Причина, по которой они хотели бы сказать именно это, состоит в том, что техническое определение того, что означает для функции f быть нестрогим, - это когда f ⊥ не ⊥.

Но при определении функций Haskell (в коде) нет роли _|_ (или ⊥, или undefined, или вообще концепции дна). Невозможно сопоставить шаблон по аргументу, чтобы определить, является ли он ⊥ по ряду причин, и поэтому в коде Haskell ³ нет фактического символа для ⊥. zip [] _|_ = [] представляет собой документацию о свойстве, которое является следствием определения zip, а не части его определения.

Как описание этого свойства zip [] _ = [] является менее конкретным требованием; он сказал бы, что чем бы вы не назовете zip [] on, он возвращает []. Это то же самое, так как единственный способ zip [] ⊥ может вернуть что-то не дно, если он вообще не проверяет свой второй аргумент. Но это говорит не сразу о определении нестрогости.

Поскольку код, составляющий часть определения функции zip [] _ = [], нельзя сравнивать и противопоставлять zip [] _|_ = []. Они не альтернативы, первый - действительный код, а второй - нет.

¹ Который является "значением" выражения, которое выполняется навсегда, выдает исключение или иным образом падает, чтобы оценить нормальное значение.

² Это даже не действительный идентификатор Haskell, так как он содержит символы "namey" (_) и "operator" (|). Таким образом, это не может быть символом, означающим что-либо вообще в коде Haskell!

³undefined часто используется для ⊥, но это скорее переменная, относящаяся к значению ⊥, чем сама фактическая вещь. Как и в случае с let xs = [1, 2, 3], вы можете использовать xs для ссылки на список [1, 2, 3], но вы не можете использовать его в качестве шаблона для сопоставления некоторого другого списка; совпадение с запрограммированным шаблоном просто рассматривалось бы как введение новой переменной с именем undefined или xs затенением старой.

Ответ 3

⊥ вытекает из теории математического порядка. Частично упорядоченная коллекция имеет нижний элемент, обозначаемый ⊥, если этот элемент предшествует каждому другому элементу. Как это попадает в документацию Haskell? В какой-то момент компьютерные ученые поняли, что было бы полезно подумать о том, что означает компьютерная программа на любом языке. Один подход к этому называется денотационной семантикой. В денотационной семантике каждому термину на языке программирования присваивается "обозначение" или значение в некоторой вселенной математических значений. Было бы замечательно, если бы можно было сказать, что

• meaningInteger :: Integer -> mathematical integer
• meaningList :: [a] -> possibly-infinite sequence of elements of type a

К сожалению, это не совсем работает в Haskell, потому что, например, я могу написать

oops :: Integer
oops = oops

Это дает мне термин типа Integer, но нет разумного способа присвоить ему значение как математическое целое. Более интересно, я мог писать такие вещи, как

undefined
undefined : undefined
3 : undefined
[undefined]
let foo = undefined : 3 : undefined : foo

Эти все (могут) имеют один и тот же тип, но имеют разные уровни неопределенности. Поэтому нам нужно добавить в нашу коллекцию значений различные виды undefined вещей. Однако возможно наложить на них частичный порядок в зависимости от того, как они определены! Например, 3 : 4 : [] более определен, чем 3 : 4 : undefined, а также более определен, чем 3 : undefined : 4, но последние два не сопоставимы. Нижний элемент каждого типа, его наименее определенный элемент, называется ⊥.

Ответ 4

Riffing на AJFarmar ответе, я думаю, что эта критическая точка не была сделана явной:

• _|_ не является допустимым литералом или идентификатором в коде Haskell!
• И поэтому zip [] _|_ = [] также не является допустимым кодом!

Это подразумевается в том, что AJFarmar означает по этой цитате:

[T] he line zip [] _|_ = [] не действует как совпадение шаблона, а уравнение, указывающее равенство zip [] _|_ и [].

Чтобы сделать его очень четким, zip [] _|_ = [] отображается в комментариях документации для определения zip. Это не код Haskell - это комментарий на английском языке, написанный в неофициальной технической нотации, которая немного похожа на код Haskell. Или, другими словами, псевдокод.