Haskell:为什么模式匹配适用于类型而不是相等的实例？

Question

我想知道 Haskell 中的模式匹配是如何工作的。我知道 this thread ，但不能完全理解其中的答案。

答案表明类型由 bool 表达式匹配，但这怎么可能呢？

我得到的另一件事是模式匹配比 (==) 更通用。和 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

我只想指出，数据类型和模式匹配(初步近似)只是有用但冗余的语言特性，可以纯粹使用 lambda 演算来实现。如果您了解如何在 lambda 演算中实现它们，您就可以理解为什么它们不需要 Eq实现模式匹配。

在 lambda 演算中实现数据类型被称为“教堂编码”(在 Alonzo Church 之后，他演示了如何做到这一点)。 Church-encoded 函数也被称为“Continuation-passing style”。

它被称为“连续传递样式”，因为您提供了一个处理该值的函数，而不是提供值。例如，不要给用户一个 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

使用延续传递风格，我们可以将任何数据类型转换为 lambda 演算项。让我们从一个简单的类型开始，例如:

data Either a b = Left a | Right b

在延续传递风格中，这将变为:

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

但是 Alonzo Church 很聪明，他注意到对于任何具有多个构造函数的类型，我们可以只为每个构造函数提供一个单独的函数。所以在上述类型的情况下，而不是提供类型为(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

由于同构，我们可以保证所有 Church 编码将具有与原始数据类型的可能值一样多的实现。因此，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对类型进行模式匹配。在 lambda 演算中，类型决定它“等于”什么，只需定义它从提供给它的参数中选择哪个参数。

所以如果我是 true , 我证明我“等于” true总是选择我的第一个论点。如果我是 false , 我证明我“等于” false总是选择我的第二个论点。简而言之，构造函数“相等”归结为“位置相等”，它总是在 lambda 演算中定义，如果我们可以将一个参数区分为“第一个”，另一个作为“第二个”，这就是我们所需要的“比较”构造函数的能力。