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

Question

Scott 编码列表可以定义如下：

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

与 ADT 版本相反 List 是类型和数据构造函数。 Scott编码通过模式匹配来确定ADTs，本质上就是去掉一层构造函数。这是没有隐式参数的完整 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 有自己的作用域，但这不是很有用。与 uncons 相比，为什么 r 和 List a 颠倒了？为什么 LHS 上有额外的括号？

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

Answer 1

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

那么，我们如何制作列表呢？好吧，我们需要这个行为的基础功能。也就是说，我们需要一个函数，它本身接受 r 和 a -> List a -> r 并对它们做一些事情（大概是直接返回 r 或在某些 [=21= 上调用函数] 和 List a)。 that 的类型类似于：

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！相反，我们将 forall 放在的第一组括号内，表示 List 的创建者必须提供一个可以在 [=43= 上工作的函数]any 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)))))

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

How to infer the type of the Scott encoded List constructor?

haskell

functional-programming

algebraic-data-types

higher-rank-types

scott-encoding