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

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

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

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

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

解决方法

什么是List？正如您所说，当提供一个常量（如果列表为空时做什么）和一个延续（如果列表非空时做什么）时，它会做其中一件事情。在类型中，它需要一个 r 和一个 a -> List a -> r 并产生一个 r。

那么，我们如何制作清单？好吧，我们需要作为这种行为基础的函数。也就是说，我们需要一个函数，它本身接受 r 和 a -> List a -> r 并用它们做一些事情（大概，要么直接返回 r，要么在某个 {{1} } 和 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 应该可以为any List 工作，但是有了这个函数，r 实际上是提前提供的。确实，有人将这种类型专门用于 r 并没有错，导致：

Int

但这不好！这个 List :: forall a. (Int -> (a -> List a -> Int) -> Int) -> List a 只能产生 List！相反，我们将 Int 放在第一组括号中，表明 forall 的创建者必须提供一个可以对任何起作用的函数> List 而不是特定的。这产生了类型：

r

,

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

给定

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)))))