Haskell: Почему сопоставление шаблонов работает для типов без экземпляров равенства?

Question

Мне было интересно, как работает шаблон в Haskell, я знаю об этой теме, но не мог понять ответы на них.

How does Haskell do pattern matching without us defining an Eq on our data types?

• ответы утверждают, что типы совпадают булевыми выражениями, но как это возможно.
• Другая вещь, которую я получил, это соответствие шаблону более общее, чем (==) и Eq реализовано с использованием сопоставления шаблонов.

Так что вы можете сказать мне, почему match и match3 работают, даже если я опускаю deriving (Eq) в следующем фрагменте кода (это понятно, почему match2 не удается).

data MyType = TypeA | TypeB 
      deriving (Eq) 

match :: MyType -> String 
match TypeA = "this is type A" 
match TypeB = "this is type B" 

match2 :: MyType -> String 
match2 a | a == TypeA = "this is type A matched by equality" 
     | a == TypeB = "this is type B matched by equality" 
     | otherwise = "this is neither type A nor type B" 

match3 :: MyType -> String 
match3 a = case a of TypeA -> "this is type A matched by case expression" 
        TypeB -> "this is type B matched by case expression" 

main :: IO() 
main = do 
    (print . match) TypeA 
    (print . match) TypeB 
    (print . match2) TypeA 
    (print . match2) TypeB 
    (print . match3) TypeA 
    (print . match3) TypeB 

Answer 1

Я просто хочу указать, что типы данных и сопоставление образцов (в первом приближении) являются просто полезными, но избыточными языковыми функциями, которые могут быть реализованы исключительно с использованием лямбда-исчисления. Если вы понимаете, как их реализовать в лямбда-исчислении, вы можете понять, почему они не нуждаются в Eq для реализации соответствия шаблону.

Внедрение типов данных в лямбда-исчислении называется «Церковное кодирование» их (после церкви Алонсо, которая продемонстрировала, как это сделать). Церковно-кодированные функции также известны как «Стиль продолжения прохождения».

Это называется «стиль продолжения прохождения», потому что вместо предоставления значения вы предоставляете функцию, которая будет обрабатывать значение. Так, например, вместо того, чтобы дать пользователю по электронной Int, я мог бы вместо того, чтобы дать им значение следующего вида:

type IndirectInt = forall x . (Int -> x) -> x 

выше типа является «изоморфными» к Int. «Изоморфная» это просто причудливый способ сказать, что мы можем преобразовать любой IndirectInt в Int:

fw :: IndirectInt -> Int 
fw indirect = indirect id 

... и мы можем преобразовать любой Int в IndirectInt:

bw :: Int -> IndirectInt 
bw int = \f -> f int 

... такие, что:

fw . bw = id -- Exercise: Prove this 
bw . fw = id -- Exercise: Prove this 

Использование продолжением мимолетную стиль, мы можем преобразовать любой тип данных в перспективе лямбда-исчисления.Давайте начнем с простым типом, например:

data Either a b = Left a | Right b 

В продолжении прохождения стиля, это стало бы:

type IndirectEither a b = forall x . (Either a b -> x) -> x 

Но Алонзо Чёрч был умным и заметил, что для любого типа с несколькими конструкторами, мы можем просто предоставляют отдельную функцию для каждого конструктора. Таким образом, в случае указанного выше типа, вместо обеспечения функции типа (Either a b-> x), мы можем вместо этого предоставить две отдельные функции, один для a, и один для b, и это было бы так же хорошо:

type IndirectEither a b = forall x . (a -> x) -> (b -> x) -> x 
-- Exercise: Prove that this definition is isomorphic to the previous one 

Как насчет типа Bool, где у конструкторов нет аргументов? Ну, Bool изоморфно Either()() (Упражнение: Докажите это), так что мы можем просто кодировать его, как:

type IndirectBool = forall x . (() -> x) -> (() -> x) -> x 

И () -> x просто изоморфно x (Упражнение: Докажите это), так что мы можем в дальнейшем записать его в виде :

type IndirectBool = forall x . x -> x -> x 

есть только две функции, которые могут быть выше типа:

true :: a -> a -> a 
true a _ = a 

false :: a -> a -> a 
false _ a = a 

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

Но как мы можем сопоставить матч на нашем IndirectBool? Например, с помощью обычного Bool, мы могли бы просто написать:

expression1 :: a 
expression2 :: a 

case someBool of 
    True -> expression1 
    False -> expression2 

Ну, с нашей IndirectBool он уже поставляется с инструментами для деконструкции себя. Мы бы просто написать:

myIndirectBool expression1 expression2 

Обратите внимание, что если myIndirectBool является true, он выберет первое выражение, и если это false он выберет второе выражение, так же, как если бы мы имели как-то картину подобранные по его стоимости ,

Давайте попробуем сделать то же самое с IndirectEither. Используя обычный Either, мы бы написать:

f :: a -> c 
g :: b -> c 

case someEither of 
    Left a -> f a 
    Right b -> g b 

С IndirectEither, мы бы просто написать:

someIndirectEither f g 

Короче говоря, когда мы пишем тип в продолжающем мимолетной стиле, являются продолжениями как и аргументы case для конструкции case, так что все, что мы делаем, - это передавать каждый аргумент case в качестве аргументов функции.

Именно по этой причине вам не нужен смысл Eq для сопоставления рисунка по типу. В исчислении лямбда тип решает, что он «равен», просто определяя, какой аргумент он выбирает из тех, которые ему предоставляются.Поэтому, если я true, я докажу, что я «равен» true, всегда выбирая свой первый аргумент. Если я false, я докажу, что я «равен» false, всегда выбирая мой второй аргумент. Короче говоря, конструктивное «равенство» сводится к «позиционному равенству», которое всегда определяется в лямбда-исчислении, и если мы можем отличить один параметр как «первый», а другой как «второй», это все, что нам нужно способность «сравнивать» конструкторы.

Answer 2

Вещь, которую вам не хватает, заключается в том, что конструкторы в Haskell могут иметь аргументы. Теги типа «сами» сопоставимы по принципу равенства (по крайней мере внутренне, за кулисами), но полные значения сопоставимы только в том случае, если составляющие аргументы также сопоставимы.

Так что, если у вас есть тип, как

data Maybe a = Nothing | Just a 

тогда, даже если вы можете проверить, если тип тега не «ничего» или «Просто» (т.е. .; шаблон матч на возможно стоимости) в целом вы не может сравниться полностью, возможно, если значение типа «а», которое удерживается Just, также оказывается сравнимым.

--note that your first and third examples are 
--just syntactic sugar for each other... 
matchMaybe mb = case mb of 
    Nothing -> "Got a Nothing" 
    Just _ -> "Got a Just but ignored its value" 

Теперь должно быть понятно, почему его невозможно написать вариант match2 для Maybes. Что бы вы использовали для проверки равенства в справедливом случае?

matchMaybe_2 mb | mb == Nothing = "Got a Nothing" 
       | mb == Just {- ??? -} = "This case is impossible to write like this" 

Answer 3

Прежде всего, match и match3 фактически точно так же (не обращая внимания на разные строки): сопоставление с образцом в функции Обессахаренные на саз.

Далее, сопоставление образцов работает с конструкторами, а не произвольными значениями. Согласование шаблонов встроено в язык и не зависит от булевых выражений - оно просто действует непосредственно на конструкторы. Это наиболее очевидно более сложных матчи, которые включают в себя некоторые Matchable терминов:

f :: MyType -> Int 
f (A a) = a + 1 
f (B a b) = a + b 

Как бы вы переписать эти образцы в логические выражения? Вы не можете (ничего не зная о MyType).

Вместо этого сопоставление шаблонов выполняется только конструктором. Каждый шаблон должен возглавляться конструктором - вы не можете писать шаблон, например, f (a b c) в Haskell. Затем, когда функция получает значение, он может посмотреть на конструктор значения и сразу перейти к соответствующим случаям. Так он должен работать для более сложных шаблонов (например, A a), а также так, как он работает для простых шаблонов, которые вы использовали.

Поскольку соответствие шаблонов работает только при переходе к соответствующему конструктору, это не зависит от Eqот всех.Вам не только не нужно иметь экземпляр Eq для сопоставления шаблонов, но также и тот, который не меняет поведение шаблона. Например, попробуйте следующее:

data MyType = TypeA | TypeB | TypeC 

instance Eq MyType where 
    TypeA == TypeA = True 
    TypeB == TypeC = True 
    TypeC == TypeB = True 
    _ == _   = False 

match :: MyType → String 
match TypeA = "this is type A" 
match TypeB = "this is type B" 
match TypeC = "this is type C" 

match2 :: MyType → String 
match2 a | a == TypeA = "this is type A matched by equality" 
     | a == TypeC = "this is type B matched by equality" 
     | a == TypeB = "this is type C matched by equality" 
     | otherwise = "this is neither type A nor type B" 

Теперь вы определили равенство таким образом, что TypeB равно TypeC, но не само по себе. (В реальной жизни вы должны убедиться, что равенство ведет себя разумно и соответствует рефлексивному свойству, но это пример игрушки.) Теперь, если вы используете сопоставление с образцом, TypeB по-прежнему соответствует TypeB и TypeC соответствует TypeC. Но если вы используете выражения для защиты, TypeB фактически соответствует TypeC и TypeC соответствует TypeB. TypeA не изменяется между ними.

Кроме того, обратите внимание, как был определен экземпляр Eq, используя образец сопоставив. Когда вы используете предложение deriving, оно определяется аналогичным образом с кодом, сгенерированным во время компиляции. Таким образом, сопоставление шаблонов более фундаментально, чем Eq - это часть языка, где Eq является частью стандартной библиотеки.

Таким образом: сопоставление образцов встроено в язык и работает путем сравнения конструктора, а затем рекурсивного соответствия остальной части значения. Равенство обычно реализуется с точки зрения сопоставления шаблонов и сравнивает целое значение, а не только конструктор.

Answer 4

Путь, который я думаю об этом, сопоставление шаблонов в основном побитовое равенство. Он основан на типах, а не на абстрактном понятии ценности.

Имейте в виду, однако, вы должны думать о сказать Int, как

data Int = ... | -2 :: Int | -1 :: Int | 0 :: Int | 1 :: Int | 2 :: Int | ... 

Таким образом, в некотором смысле, каждое целое число имеет другой тип.

Вот почему вы можете сравниться с Int сказать 2.

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

Например, у вас может быть двоичное дерево, в котором хранятся отсортированные элементы. Скажите следующее:

A  A 
/\ /\ 
B C B D 
    \ \ 
     D C 

можно считать равным по Eq, потому что они содержат одни и те же элементы, но вы не смогли бы проверить равенство здесь с помощью сопоставления с образцом.

Но в случае чисел побитовое равенство в основном такое же, как логическое равенство (за исключением, возможно, положительной и отрицательной с плавающей запятой 0.0), поэтому здесь Eq и сопоставление шаблонов в значительной степени эквивалентны.

---

Для аналогии с C++, думать о Eq, как operator== и сопоставления с образцом, как memcmp. Вы можете сравнивать множество типов для равенства, просто используя memcmp, но некоторые вы не можете, если они могут иметь разные представления для «равных» значений.