具有“bool”、“either”等功能的模式

Question

我最近了解了 GADTs 及其表示法：

例如

data Maybe a where
  Nothing :: Maybe a
  Just    :: a -> Maybe a

data Either a b where
  Left  :: a -> Either a b
  Right :: b -> Either a b

data Bool where
  False :: Bool
  True  :: Bool

现在我注意到 bool, and either 等函数的相似性，基本上就像 GADT 定义：

以每一行作为参数
用字母表中的下一个字母替换实际类型
最后返回一个函数Type -> (the letter of step 2)

例如

maybe  :: b -> (a -> b) -> Maybe a -> b
either :: (a -> c) -> (b -> c) -> Either a b -> c
bool   :: a -> a -> Bool -> a

这也包括 foldr，但我注意到，例如元组没有这样的功能，但你可以很容易地定义它：

tuple :: (a -> b -> c) -> (a,b) -> c
tuple f (x,y) = f x y

这是什么图案？在我看来，这些函数减轻了模式匹配的需要（因为它们为每种情况提供了通用方法），因此 every 操作该类型的函数可以根据此函数定义。

Answer 1

首先，您提到的类型并不是真正的 GADT，它们是普通的 ADT，因为每个构造函数的 return 类型总是 T a。一个合适的 GADT 应该是

data T a where
   K1 :: T Bool  -- not T a

无论如何，您提到的技术是一种将代数数据类型编码为（多态）函数的众所周知的方法。它有很多名称，如 Church 编码、Boehm-Berarducci 编码、作为变形的编码等。有时米田引理用于证明这种方法的合理性，但无需了解范畴论机制即可理解该方法。

基本上，思路如下。所有的ADT都可以通过

生成

产品类型(,) a b
求和类型Either a b
箭头类型a -> b
单位类型()
void类型Void（在Haskell中很少使用，但理论上不错）
变量（如果定义的类型bing有参数）
可能是基本类型 (Integer, ...)
类型递归

当某些值构造函数采用被定义为参数的类型时，使用类型级递归。典型的例子是 Peano 风格的自然色：

data Nat where
   O :: Nat
   S :: Nat -> Nat
     -- ^^^ recursive!

列表也很常见：

data List a where
   Nil :: List a
   Cons :: a -> List a -> List a
             -- ^^^^^^ recursive!

Maybe a、对等类型是非递归的。

请注意，每个 ADT，无论是否递归，都可以通过对所有构造函数求和 (Either) 并将所有参数相乘，简化为具有单个参数的单个构造函数。例如，Nat 同构于

data Nat1 where
  O1 :: () -> Nat
  S1 :: Nat -> Nat

同构于

data Nat2 where K2 :: (Either () Nat) -> Nat

列表变为

data List1 a where K1 :: (Either () (a, List a)) -> List a

上面的步骤使用了类型代数，这使得类型的和和乘积遵循与高中代数相同的规则，而a -> b表现得像指数b^a。

因此，我们可以将任何 ADT 写成

-- pseudo code
data T where
   K :: F T -> T
type F k = .....

例如

type F_Nat k = Either () k      -- for T = Nat
type F_List_a k = Either () (a, k) -- for T = List a

（注意后面的类型函数F依赖于a，但现在不重要。）

非递归类型不会使用k:

type F_Maybe_a k = Either () a     -- for T = Maybe a

请注意，上面的构造函数 K 使类型 T 与 F T 同构（让我们忽略它引入的提升/额外底部）。本质上，我们有

Nat ~= F Nat = Either () Nat
List a ~= F (List a) = Either () (a, List a)
Maybe a ~= F (Maybe a) = Either () a

我们甚至可以通过从 F

中抽象出来进一步形式化

newtype Fix f = Fix { unFix :: f (Fix f) }

根据定义 Fix F 现在将同构于 F (Fix F)。我们可以让

type Nat = Fix F_Nat

（在 Haskell 中，我们需要围绕 F_Nat 的新类型包装器，为清楚起见，我将其省略。）

最后，通用编码，或变形，是：

cata :: (F k -> k) -> Fix F -> k

这里假定 F 是一个函子。

对于Nat，我们得到

cata :: (Either () k -> k) -> Nat -> k
-- isomorphic to
cata :: (() -> k, k -> k) -> Nat -> k
-- isomorphic to
cata :: (k, k -> k) -> Nat -> k
-- isomorphic to
cata :: k -> (k -> k) -> Nat -> k

注意 "high school albegra" 个步骤，其中 k^(1+k) = k^1 * k^k，因此 Either () k -> k ~= (() -> k, k -> k)。

请注意，我们得到两个参数，k 和 k->k，它们对应于 O 和 S。这不是巧合——我们对所有构造函数求和。这意味着 cata 期望传递类型 k 的值，其中 "plays the role of O" 在那里，然后类型 k -> k 的值扮演 S 的角色.

更通俗地说，cata 告诉我们，如果我们想在 k 中映射一个自然数，我们只需要说明 [=40= 中的 "zero" 是什么] 以及如何在 k 中取 "successor"，然后每个 Nat 都可以因此被映射。

对于列表，我们得到：

cata :: (Either () (a, k) -> k) -> List a -> k
-- isomorphic to
cata :: (() -> k, (a, k) -> k) -> List a -> k
-- isomorphic to
cata :: (k, a -> k -> k) -> List a -> k
-- isomorphic to
cata :: k -> (a -> k -> k) -> List a -> k

即foldr.

同样，这是 cata 告诉我们，如果我们说明如何在 k 中获取 "empty list" 和 "cons" a 和 k 在 k 中，我们可以映射 k.

中的任何列表

Maybe a 同理：

cata :: (Either () a -> k) -> Maybe a -> k
-- isomorphic to
cata :: (() -> k, a -> k) -> Maybe a -> k
-- isomorphic to
cata :: (k, a -> k) -> Maybe a -> k
-- isomorphic to
cata :: k -> (a -> k) -> Maybe a -> k

如果我们可以在k中映射Nothing，并在k中执行Just映射a，那么我们可以映射任何Maybe a 在 k.

如果我们尝试对 Bool 和 (a,b) 应用相同的方法，我们将获得问题中发布的功能。

要查找的更高级理论主题：

(初)范畴论中的F-代数
类型论中的消除器/递归器/归纳原理（这些也可以应用于 GADT）

具有“bool”、“either”等功能的模式

The pattern with functions like `bool`, `either`, etc

haskell

pattern-matching

gadt