16

或者具体来说，为什么我们使用 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)

虽然此版本有效，但它使定义某些功能变得更加困难。例如，如果您可以使用模式匹配，则为列表编写“tail”函数或为数字编写“predecessor”函数是微不足道的，但如果您需要使用折叠来代替，则变得很棘手。

所以我的真正问题是：

  1. 我们如何确定使用折叠的编码与假设的“模式匹配编码”一样强大？有没有办法通过模式匹配来获取任意函数定义，然后机械地将其转换为仅使用折叠的函数？（如果是这样，这也将有助于在 foldr 方面使诸如 tail 或 foldl 之类的棘手定义变得不那么神奇）

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

4

2 回答 2

6

给定一些归纳数据类型

data Nat = Succ Nat | Zero

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

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

很明显，每个类型的函数Nat -> a都可以通过给出适当的fand来定义，g并且唯一的方法Nat是使用两个构造函数之一。

编辑：想一想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 类型解决，并且它们具有所有功能，它们只是将更多的工作强加给程序员部分。我喜欢声称你可以在没有任何开销的情况下获得你的 iso-recursive 类型

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

但显然 GHCs 优化器有时会扼杀那些 :(。

于 2012-11-27T05:51:30.097 回答
3

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

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

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 折叠来产生它给出的列表参数以及它应该产生的结果。然后在链x1 `f` (x2 `f` (... `f` xn) ... )中最外层f接收一对(y, x2 : ... : xn : [])（对于y我们不关心的一些），所以返回f x1 (x2 : ... : xn : [])。当然，它也必须返回x1 : ... : xn : []，以便更多的应用程序f也可以工作。

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

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

于 2012-12-06T16:33:22.460 回答