具有`bool`,`both`等功能的模式

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

现在,我注意到一个similiarity像功能bool,并且either,这基本上是一样的GADT定义:

1. 把每一行作为一个论据
2. 用字母表的下一个字母替换实际类型
3. 最后返回一个函数 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没有这样的功能,虽然你可以很容易地定义它:

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

这种模式是什么？在我看来,这些函数减轻了模式匹配的需要(因为它们为每种情况提供了一般方法),因此可以根据此函数定义在该类型上操作的每个函数.

Answer 1

首先，您提到的类型并不是真正的 GADT，它们是普通的 ADT，因为每个构造函数的返回类型始终是T a。正确的 GADT 应该是这样的

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

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

基本上，想法如下。所有 ADT 都可以通过以下方式生成

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

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

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

列表也很常见：

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

、pairs 等类型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

注意“高中阿尔贝格拉”步骤，其中k^(1+k) = k^1 * k^k，因此Either () k -> k ~= (() -> k, k -> k)。

请注意，我们得到两个参数，k和k->k对应于O和S。这不是巧合——我们对所有构造函数进行了总结。这意味着cata期望传递k“扮演”角色的类型值，然后传递扮演“角色”O的类型值。k -> kS

更通俗地说，cata就是告诉我们，如果我们想要映射 中的一个自然数k，我们只需说明其中的“零”是什么k以及如何取 中的“后继” k，然后每个都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和 中的“空列表”放入“cons”a和kinside 中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

如果我们可以映射Nothing并k在中执行Just映射，那么我们就可以映射 中的任何内容。akMaybe ak

如果我们尝试应用相同的方法Bool，(a,b)我们就会达到问题中发布的功能。

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

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