6

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有自己的范围,但这不是很有帮助。为什么都rList a翻转相比uncons?为什么 LHS 上有额外的括号?

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

4

2 回答 2

5

什么是List? 正如您所说,当提供一个常量(如果列表为空时该怎么办)和延续(如果列表非空怎么办)时,它会做其中的一件事情。在类型中,它需要一个r和一个a -> List a -> r并产生一个r

那么,我们如何制作清单呢?好吧,我们需要支持这种行为的函数。也就是说,我们需要一个函数,它本身接受randa -> List a -> r并且对它们做一些事情(大概是直接返回或者在 some andr上调用函数)。它的类型看起来像:aList 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应该可以为any r工作,但使用此功能,r实际上是提前提供的。确实,将这种类型专门用于 的人并没有错,例如Int,导致:

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

但这不好!这List将只能产生Ints! 相反,我们将第一组括号放在forall 里面,表明 a 的创建者List必须提供一个可以在任何 r而不是特定的函数上工作的函数。这会产生类型:

List :: (forall r. r -> (a -> List a -> r) -> r) -> List a
于 2021-02-07T23:49:03.507 回答
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)))))
于 2021-02-08T11:44:16.870 回答