为什么我们使用folds将数据类型编码为函数？

Question

具体而言，为什么我们使用foldr来编码列表，使用迭代来编码数字？

抱歉我的介绍有些冗长，但我不知道如何命名我想要询问的东西，所以我需要先进行一些阐述。这主要参考了C.A.McCann的这篇文章，但它并没有完全满足我的好奇心，同时我也会略显地讲解rank-n-types和无限懒加载的问题。

---

将数据类型编码为函数的一种方法是创建一个“模式匹配”函数，该函数接收每个情况的一个参数，每个参数都是一个接收与该构造函数相应的值的函数，并且所有参数都返回相同的结果类型。

对于非递归类型，这一切都按预期进行。

--encoding data Bool = true | False
type Bool r = r -> r -> r

true :: Bool r
true = \ct cf -> ct

false :: Bool r
false = \ct cf -> cf

--encoding data Either a b = Left a | Right b
type Either a b r = (a -> r) -> (b -> r) -> r

left :: a -> Either a b r
left x = \cl cr -> cl x

right :: b -> Either a b r
right y = \cl cr -> cr y

然而，当涉及到递归类型时，与模式匹配的好比并不适用。我们可能会想要做一些类似于以下的事情：

然而，当涉及到递归类型时，与模式匹配的美好类比就不再适用了。我们可能会尝试像下面这样做：

--encoding data Nat = Z | S Nat
type RecNat r = r -> (RecNat -> r) -> r
zero = \cz cs -> cz
succ n = \cz cs -> cs n

-- encoding data List a = Nil | Cons a (List a)
type RecListType a r = r -> (a -> RecListType -> r) -> r
nil = \cnil ccons -> cnil
cons x xs = \cnil ccons -> ccons x xs

但是在Haskell中，我们无法编写这些递归类型定义！通常的解决方案是强制将cons/succ情况的回调应用于所有层次的递归而不仅仅是第一层（即编写一个fold/iterator）。 在此版本中，我们使用返回类型r来代替递归类型:

--encoding data Nat = Z | S Nat
type Nat r = r -> (r -> r) -> r
zero = \cz cf -> cz
succ n = \cz cf -> cf (n cz cf)

-- encoding data List a = Nil | Cons a (List a)
type recListType a r = r -> (a -> r -> r) -> r
nil = \z f -> z
cons x xs = \z f -> f x (xs z f)

尽管这个版本可以工作，但是它使得一些函数的定义变得更加困难。例如，如果你使用了模式匹配，那么编写列表的"tail"函数或数字的"predecessor"函数就很容易，但如果您需要使用folds，则会变得棘手。

接下来是我的真正问题：

1. 我们如何确保使用folds进行编码与假设的“模式匹配编码”一样强大？是否有一种方法可以通过模式匹配来机械地将任意函数定义转换为仅使用folds的函数定义？（如果有的话，这也将有助于使像tail或foldl这样的棘手定义不再那么神奇）

2. 为什么Haskell类型系统不允许“模式匹配”编码中所需的递归类型？为什么只允许通过"data"定义递归类型的数据类型？模式匹配是否是直接消耗递归代数数据类型的唯一方式？这是否与类型推断算法有关？

- hugomg

---

我只是把这个留在这里：http://www.haskell.org/pipermail/haskell-cafe/2010-November/085897.html - melpomene

@melpomene：嗯，看起来那回答了问题#2 - 你可以在Haskell中做到这一点，但你需要使用newtypes才能获得对递归的访问。现在我只需要看看你提供的那些论文是否也回答了问题#1 :) （顺便说一句，你的链接复制粘贴得有点奇怪） - hugomg

虽然 Nat 的前任很难，但添加是 O(1)（我认为这甚至比计算机通常使用的二进制版本更有效率）。 - PyRulez

Answer 1

假设有一个归纳数据类型

data Nat = Succ Nat | Zero

我们可以考虑如何在这些数据上进行模式匹配。

case n of
  Succ n' -> f n'
  Zero    -> g

显然，每个类型为 Nat -> a 的函数都可以通过给定适当的 f 和 g 来定义，并且除了使用两个构造函数之一以外，没有其他方法可以创建一个 Nat（除了底部）。

---

编辑：仔细考虑一下 f。如果我们通过给出适当的 f 和 g 定义一个函数 foo :: Nat -> a，使得 f 递归调用 foo，那么我们可以将 f 重新定义为 f' n' (foo n')，使得 f' 不再是递归的。如果类型 a = (a',Nat)，那么我们可以改为写成 f' (foo n)。因此，不失一般性。

foo n = h $ case n
                 Succ n' -> f (foo n)
                 Zero    -> g

这是使我的帖子其余部分有意义的表述：

---

因此，我们可以将case语句视为应用“解构字典”

data NatDict a = NatDict {
   onSucc :: a -> a,
   onZero :: a
}

现在我们之前的Case语句可以变成：

h $ case n of
      Succ n' -> onSucc (NatDict f g) n'
      Zero    -> onZero (NatDict f g)

鉴于此，我们可以推导出：

newtype NatBB = NatBB {cataNat :: forall a. NatDict a -> a}

我们可以定义两个函数。

fromBB :: NatBB -> Nat
fromBB n = cataNat n (NatDict Succ Zero)

并且

toBB :: Nat -> NatBB
toBB Zero = Nat $ \dict -> onZero dict
toBB (Succ n) = Nat $ \dict -> onSucc dict (cataNat (toBB n) dict)

我们可以证明这两个函数是同构的证人（使用快速且不精确的推理），从而表明

newtype NatAsFold = NatByFold (forall a. (a -> a) -> a -> a)

(这与 NatBB 相同) 同构于 Nat

我们可以使用相同的构造方法来处理其他类型，并通过代数推理（和归纳）证明所得到的函数类型是我们想要的。

至于您的第二个问题，Haskell 的类型系统基于等递归而不是等价递归类型。这可能是因为使用等递归类型更容易处理理论和类型推断，并且它们具有所有功能，只需在程序员的部分施加一些额外的工作。我喜欢声称您可以在没有任何开销的情况下获得您的等递归类型。

newtype RecListType a r = RecListType (r -> (a -> RecListType -> r) -> r)

但显然 GHC 的优化器有时会卡住这些内容 :(。

- Philip JF

---

等一下，为什么在NatDict的onSucc情况下是(a -> a)？难道它不应该接收一个natdict作为第一个参数，而不是一个a以使模式匹配并行保持吗？（我还不明白的部分是，为什么我们可以确定在这种情况下fold和模式匹配是一样强大的） - hugomg

onSucc是正确的，但我的后续解释还不够...请给我一点时间。 - Philip JF

Answer 2

维基百科关于斯科特编码的页面提供了一些有用的见解。简而言之，你所指的是教堂编码，而你的“假设模式匹配编码”是斯科特编码。两种方法都是合理的，但教堂编码需要更轻量级的类型机制来使用（特别是它不需要递归类型）。

证明这两者等价的方法使用以下思想：

churchfold :: (a -> b -> b) -> b -> [a] -> b
churchfold _ z [] = z
churchfold f z (x:xs) = f x (churchfold f z xs)

scottfold :: (a -> [a] -> b) -> b -> [a] -> b
scottfold _ z [] = z
scottfold f _ (x:xs) = f x xs

scottFromChurch :: (a -> [a] -> b) -> b -> [a] -> b
scottFromChurch f z xs = fst (churchfold g (z, []) xs)
 where
  g x ~(_, xs) = (f x xs, x : xs)

这个想法是，由于 churchfold (:) [] 对列表的作用就是恒等，我们可以使用一个 Church fold 来生成它所接收到的列表参数以及它应该生成的结果。然后在链式表达式 x1 `f` (x2 `f` (... `f` xn) ... ) 中，最外层的 f 接收到一对 (y, x2 : ... : xn : [])（其中 y 是我们不关心的值），因此返回 f x1 (x2 : ... : xn : [])。当然，它还必须返回 x1 : ... : xn : []，以便更多的 f 应用也能正常工作。

（这实际上有点类似于从“弱”或通常的归纳原理证明数学原理 strong（或完全）归纳 的证明方法。）

顺便提一下，你的Bool r类型对于真正的Church布尔值来说有点太大了——例如(+) :: Bool Integer，但(+)并不真正是一个Church布尔值。如果启用RankNTypes，则可以使用更精确的类型：type Bool = forall r. r -> r -> r。现在它被强制为多态，因此仅包含两个（忽略seq和底部）成员——\t _ -> t和\_ f -> f。类似的想法也适用于其他的Church类型。

- Ben Millwood