Scott编码列表可以定义如下:
newtype List a =
List {
uncons :: forall r. r -> (a -> List a -> r) -> r
}
与 ADT 版本相反的List
是类型和数据构造函数。Scott 编码通过模式匹配来确定 ADT,这实质上意味着移除了一层构造函数。这是uncons
没有隐式参数的完整操作:
uncons :: r -> (a -> List a -> r) -> List a -> r
-- Nil ^ ^^^^^^^^^^^^^^^^^^ Cons
uncons nil cons (List f) = f nil cons
这很有意义。uncons
接受一个常数、一个延续和 aList
并产生任何值。
然而,数据构造函数的类型对我来说没有多大意义:
List :: (forall r. r -> (a -> List a -> r) -> r) -> List a
我看到它r
有自己的范围,但这不是很有帮助。为什么都r
和List a
翻转相比uncons
?为什么 LHS 上有额外的括号?
我可能在这里混淆了类型和术语级别..