如何推断 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接受一个常数、一个延续和 aList并产生任何值。

然而，数据构造函数的类型对我来说没有多大意义：

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

我看到它r有自己的范围，但这不是很有帮助。为什么是r和List a翻转相比uncons？为什么 LHS 上有额外的括号？

我可能在这里混淆了类型和术语级别。

Answer 1

什么是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而不是特定函数起作用的函数。这产生了以下类型：

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

Answer 2

^{（根据要求将我的评论移至此答案。）}

给定

newtype List a =
    List {
      uncons :: forall r. r -> (a -> List a -> r) -> r
    }

让我们写下一些清单。请注意，列表本质上是两个参数 ( \nil cons -> ...) 的函数。

-- []
empty = List (\nil _ -> nil)

-- [True]
-- True : []
-- (:)  True []
-- cons True nil
list1 = List (\_ cons -> cons True (List (\nil _ -> nil)))

-- [True, False]
-- True : False : []
-- (:)  True ((:)  False [])
-- cons True (cons False nil)
list2 = List (\_ cons -> 
           cons True (List (\_ cons' -> 
               cons' False (List (\nil _ -> nil)))))