如何解决如何推断 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)))))
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。