gpt4 book ai didi

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

转载 作者:行者123 更新时间:2023-12-03 14:06:11 25 4
gpt4 key购买 nike

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有自己的范围,但这不是很有帮助。为什么是 rList auncons 相比翻转?为什么 LHS 上有额外的括号?
我可能在这里混淆了类型和术语级别..

最佳答案

什么是List ?正如您所说,当提供一个常量(如果列表为空时该怎么办)和延续(如果列表非空该怎么办)时,它会做其中的一件事情。在类型中,它需要 ra -> List a -> r并产生 r .
那么,我们如何制作 list 呢?好吧,我们需要支持这种行为的函数。也就是说,我们需要一个本身采用 r 的函数。和 a -> List a -> r并对它们做一些事情(大概是直接返回 r 或在某些 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应该可以为任何 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

关于haskell - 如何推断 Scott 编码的 List 构造函数的类型?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/66093671/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com