haskell - 如何推断 Scott 编码的 List 构造函数的类型？

Question

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接受一个常数、一个延续和一个 List并产生任何值(value)。
然而，数据构造函数的类型对我来说没有多大意义:

List :: (forall r. r -> (a -> List a -> r) -> r) -> List a

我看到 r有自己的范围，但这不是很有帮助。为什么是 r和 List a与 uncons 相比翻转?为什么 LHS 上有额外的括号？
我可能在这里混淆了类型和术语级别..

Answer 1

什么是List ?正如您所说，当提供一个常量(如果列表为空时该怎么办)和延续(如果列表非空该怎么办)时，它会做其中的一件事情。在类型中，它需要 r和 a -> List a -> r并产生 r .
那么，我们如何制作 list 呢？好吧，我们需要支持这种行为的函数。也就是说，我们需要一个本身采用 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只能生产Int !相反，我们把 forall在第一组括号内，表示 List 的创建者必须提供可以在任何 r 上工作的函数而不是一个特定的。这会产生类型:

List :: (forall r. r -> (a -> List a -> r) -> r) -> List a