或者具体来说,为什么我们使用 foldr 来编码列表和迭代来编码数字?
很抱歉介绍冗长,但我真的不知道如何命名我想问的事情,所以我需要先做一些说明。这主要来自 this C.A.McCann post这并不能完全满足我的好奇心,而且我也会用 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”函数是微不足道的,但如果您需要使用折叠来代替,则变得很棘手。
所以我的真正问题是:
data
定义的数据类型中使用递归类型? ?模式匹配是直接使用递归代数数据类型的唯一方法吗?它与类型推断算法有关吗? 最佳答案
给定一些归纳数据类型
data Nat = Succ Nat | Zero
我们可以考虑如何对这些数据进行模式匹配
case n of
Succ n' -> f n'
Zero -> g
很明显,
Nat -> a
类型的每个函数可以通过给出适当的 f
来定义和 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 优化器有时会扼杀那些 :(。
关于haskell - 为什么我们使用折叠将数据类型编码为函数?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/13575894/