如何推断Scott编码的List构造函数的类型?
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
List :: (forall r. r -> (a -> List a -> r) -> r) -> List a
我看到它r有自己的范围,但这不是很有帮助。为什么是r和List a翻转相比uncons?为什么 LHS 上有额外的括号?
我可能在这里混淆了类型和术语级别。
回答
什么是List?正如你所说,当提供一个常量(如果列表为空时做什么)和一个延续(如果列表非空时做什么)时,它会做这些事情之一。在类型中,它接受 anr和 aa -> List a -> r并产生一个r。
那么,我们如何制作清单呢?好吧,我们需要作为这种行为基础的函数。也就是说,我们需要一个函数,它本身需要的r和a -> List a -> r和做一些事情与他们(据推测,要么返回r直接或调用一些功能a和List a)。该类型的那看起来是这样的:
List :: (r -> (a -> List a -> r) -> r) -> List a
-- ^ the function that _takes_ the nil and continuation and does stuff with them
但是,这并不完全正确,如果我们使用显式,这会变得很清楚forall:
List :: forall a r. (r -> (a -> List a -> r) -> r) -> List a
请记住,List应该可以为任何 工作r,但是有了这个功能,r实际上是提前提供的。确实,有人将这种类型专门用于,例如Int,导致:
List :: forall a. (Int -> (a -> List a -> Int) -> Int) -> List a
但这不好!这List将只能产生Ints!相反,我们将 theforall 放在第一组括号内,表明 a 的创建者List必须提供一个可以对任何 函数r而不是特定函数起作用的函数。这产生了以下类型: