haskell - 具有 `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 等函数的相似之处。 , 和 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 没有这样的函数，尽管您可以轻松定义它:

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 编码、作为 catamorphism 的 endcoding 等。有时使用米田引理来证明这种方法是正确的，但没有必要了解范畴论机制来理解该方法。

基本上，想法如下。所有的 ADT 都可以由

产品类型 (,) a b

和类型 Either a b

箭头类型 a -> b

单元类型 ()

空型 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 ，对等是非递归的。

请注意，通过对所有构造函数求和 ( Either ) 并将所有参数相乘，可以将每个 ADT，无论是否递归，都可以简化为具有单个参数的单个构造函数。例如， 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 的新型包装器，为了清楚起见，我省略了它。)

最后，一般的编码或 catamorphism 是:

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

注意“高中 albegra”步骤，其中 k^(1+k) = k^1 * k^k ，因此 Either () k -> k ~= (() -> k, k -> k) .

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

更非正式地， 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 中说明如何取“空列表”和“缺点” 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

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

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

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

(初始)范畴论中的 F 代数

类型论中的消除器/递归器/归纳原理(这些也可以应用于 GADT)