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

Question

或者具体来说,为什么我们使用foldr来编码列表和迭代来编码数字？

对于长篇介绍很抱歉,但我真的不知道如何命名我想问的事情,所以我需要先给一些说明.这很大程度上吸引了这个CAMcCann的帖子,这个帖子只是不太满足我的好奇心,而且我也会用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案例的回调应用于所有级别的递归而不仅仅是第一个递归(即,编写折叠/迭代器).在这个版本中,我们使用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)

虽然这个版本有效,但它使得定义一些函数变得更加困难.例如,如果您可以使用模式匹配,则为列表编写"尾部"函数或为数字编写"前任"函数是微不足道的,但如果您需要使用折叠,则会变得棘手.

所以我真正的问题:

1. 我们如何确保使用折叠的编码与假设的"模式匹配编码"一样强大？有没有办法通过模式匹配采取任意函数定义,并使用折叠机械转换为一个？(如果是这样,这也有助于制作棘手的定义,例如在折叠器中使用tail或foldl,因为它不那么神奇)

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

Answer 1

给出一些归纳数据类型

data Nat = Succ Nat | Zero

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

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

显而易见的是,类型的每个函数Nat -> a都可以通过给出一个适当的来定义f,g并且制作一个Nat(baring bottom)的唯一方法是使用两个构造函数中的一个.

编辑:想f一下.如果我们定义一个函数foo :: Nat -> a给予适当的f,并g使得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
}

现在我们的案例陈述可以成为

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的类型系统是基于iso-recursive而不是equi-recursive类型.这可能是因为理论和类型推断更易于使用iso-recursive类型,并且它们具有所有的功能,它们只是对程序员部分施加了更多的工作.我想声称你可以在没有任何开销的情况下获得iso-recursive类型

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

但显然GHC优化器有时会对这些产生扼要:(.

Answer 2

关于斯科特编码的维基百科页面有一些有用的见解。简而言之，您所指的是 Church 编码，而您的“假设模式匹配编码”是 Scott 编码。两者都是明智的做事方式，但 Church 编码需要使用更轻的类型机制（特别是，它不需要递归类型）。

\n\n

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

\n\n

churchfold :: (a -> b -> b) -> b -> [a] -> b\nchurchfold _ z [] = z\nchurchfold f z (x:xs) = f x (churchfold f z xs)\n\nscottfold :: (a -> [a] -> b) -> b -> [a] -> b\nscottfold _ z [] = z\nscottfold f _ (x:xs) = f x xs\n\nscottFromChurch :: (a -> [a] -> b) -> b -> [a] -> b\nscottFromChurch f z xs = fst (churchfold g (z, []) xs)\n where\n  g x ~(_, xs) = (f x xs, x : xs)\n

\n\n

这个想法是，由于churchfold (:) []是列表上的恒等式，我们可以使用 Church 折叠来生成给定的列表参数以及它应该生成的结果。然后在链中x1 `f` (x2 `f` (... `f` xn) ... )最外层f接收一对(y, x2 : ... : xn : [])（对于一些y我们不关心的），因此返回f x1 (x2 : ... : xn : [])。当然，它也必须返回，x1 : ... : xn : []以便任何更多的应用程序f也可以工作。

\n\n

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

\n\n

顺便说一句，您的Bool r类型对于真正的 Church 布尔值 \xe2\x80\x93 例如 来说有点太大(+) :: Bool Integer，但(+)并不是真正的 Church 布尔值。如果启用RankNTypes，则可以使用更精确的类型：type Bool = forall r. r -> r -> r。现在它被迫是多态的，因此实际上只包含两个（忽略seq和底部）居民 \xe2\x80\x93\\t _ -> t和\\_ f -> f。类似的想法也适用于其他教会类型。

\n