类型安全的差异列表

sha*_*haf 25 haskell types

Haskell中的一个常见习语(差异列表)是将列表表示xs为值(xs ++).然后(.)变成" (++)"并id变成" []"(实际上这适用于任何幺半群或类别).由于我们可以在恒定时间内组合函数,因此这为我们提供了一种通过追加来有效构建列表的好方法.

不幸的是,类型[a] -> [a]比表单的函数类型更大(xs ++)- 列表上的大多数函数除了在它们的参数之前做一些事情.

解决此问题的一种方法(如用于dlist)是DList使用智能构造函数创建一个特殊类型.另一种方法(如所使用的ShowS)是不在任何地方强制执行约束并希望最好.但是有一种很好的方法可以保持差异列表的所有所需属性,同时使用一个完全正确大小的类型吗?

Rom*_*aka 25

是!

我们可以将其[a]视为免费的monad实例Free ((,) a) ().

因此,我们可以将爱德华·凯梅特描述的方案应用于免费Monads for Less.

我们得到的类型是

newtype F a = F { runF :: forall r. (() -> r) -> ((a, r) -> r) -> r }
Run Code Online (Sandbox Code Playgroud)

或者干脆

newtype F a = F { runF :: forall r. r -> (a -> r -> r) -> r }
Run Code Online (Sandbox Code Playgroud)

所以runF只是foldr我们列表的功能!

这称为Boehm-Berarducci编码,它与原始数据类型(列表)同构 - 所以这个就像你可能得到的一样小.


尼斯会说:

所以这种类型仍然太"宽",它不仅仅允许前缀 - 不限制g函数参数.

如果我理解正确的话他的说法,他指出,你可以应用foldr(或runF)函数从不同的东西[](:).

但我从未声称你只能使用foldr-encoding进行连接.实际上,正如这个名字所暗示的那样,你可以用它来计算任何折叠 - 这就是Will Ness所展示的.

如果你忘记了一个真正的列表类型,可能会变得更加清晰[a].可能有很多列表类型 - 例如我可以定义一个

data List a = Nil | Cons a (List a)
Run Code Online (Sandbox Code Playgroud)

它与...不同,但同构[a].

foldr上述-encoding只是还没有列出,像另一种编码List a[a].它也是同形的[a],正如功能\l -> F (\a f -> foldr a f l)\x -> runF [] (:)它们的成分(以任何顺序)是同一性的事实所证明的那样.但是您没有义务转换为[a]- 您可以List直接转换为使用\x -> runF x Nil Cons.

重要的一点是,F a不包含不是foldr某个列表的函数的元素- 它也不包含一个元素,该元素是foldr多个列表的函数(显然).

因此,它不包含太少或太多的元素 - 它包含精确代表所有列表所需的精确元素.

差异列表编码不是这样 - 例如,该reverse函数不是任何列表的追加操作.