如何解决什么是“种类的系统 FC2 语法”?
我正在尝试围绕 this blog post 扩展 ConstraintKinds
。
Adam M 说:2011 年 9 月 14 日 19:53 UTC
哇,这听起来很棒。它是否计划成为官方 GHC 7.4
的一部分?
另外,这是否意味着您已经在 System FC2 种类语法中引入了第三个产生式?目前它有 *
和 k~>k
作为唯一的选择,其中 k1~>k2
是(基本上)(forall a::k1 . (t::k2))
的那种。听起来这会添加 k1==>k2
,这是一种 (a::k1 => (t::k2))
。还是这两种其实是一样的?
有人可以分步分析这个问题,或者至少提供一些链接来帮助我自己解决这个问题。我应该指出的一些关键时刻:
- 什么是“种类的 System FC2 语法”? (可能是主要和最通用的一个,其答案将嵌入其他两个。)
- 我试着解释为什么“
k1~>k2
(基本上)是那种(forall a::k1 . (t::k2))
”?据我了解,~>
是->
在种类中的一些特殊符号,因为*
和k1 -> k2
是标准 Haskell 种类系统的唯一居民(符合他们的描述: “目前它有*
和k~>k
作为唯一的选择”)。因此,(forall a::k1 . (t::k2))
公式意味着如果我们采用一个有人居住的类型k1
,它可以映射到另一个k2
,当它是有人居住的(由于 Curry-Howard 为类型工作它对类型的工作方式相同)。是对的吗? (PS:如果我不理解类的居住概念,我会看到这种直觉是如何失败的;当它们有一个居住类型作为居住类型还是任意类型?在第二种情况下直觉失败。) -
=>
的公式中的k1==>k2
是什么意思,即(a::k1 => (t::k2))
?
这条评论得到的回应:
Max 说: 2011 年 9 月 14 日 21:11 UTC
亚当:没那么复杂!它只是将基本种类 Constraint
添加到种类的语法中。这是一种由值占据的类型,就像现有的 *
和 #
类型一样。
因此作者声称 Adam M 使扩展过于复杂。他们的反应很容易理解。无论如何,即使Adam M的评论不是真的,我认为它完全值得关注,因为它向我介绍了一些不熟悉的概念。
解决方法
“System FC2”是 Weirich 等 在 2010 年的论文“生成类型抽象和类型级计算”(link )。它指的是向 System FC 添加“角色”,并形成了在 2016 年论文 "Safe Zero-cost Coercions for Haskell 中描述的 GHC 中实现的基础。 System FC,反过来,是最初在 this paper 中描述的系统(或者实际上是早期的论文,这是其发布后的扩展版本),它扩展了System F 类型相等。
然而,我认为 Adam M 可能不太正式地使用术语“System FC2”来指代 GHC 在发表评论时实施的任何类型的系统书面。所以,这句话的意思:
在用于 Kinds 的 System FC2 语法中引入了第三种产生式
确实是:
为种类的语法添加了第三条产生式规则,因为种类目前已在 GHC 中实现
他声称种类的语法目前有两个产生式规则:
-
*
是一种 - 如果
k1
和k2
是种类,则k1 ~> k2
是种类。
他问这个扩展是否给出了第三个产生式规则:
- 如果
k1
和k2
是种类,则k1 ==> k2
是种类。
如您所料,他引入了运算符 ~>
来区分种类级箭头和类型级箭头。 (在 GHC 中,种类级和类型级箭头运算符的写法都相同 ->
。)他将 ~>
定义为:
其中 k1~>k2
是(基本上)(forall a::k1 . (t::k2))
的类型。
这是可以解释的,但非常不精确。他试图在这里使用 forall
作为一种类型级别的 lambda。不是,但你可以想象如果你有一个类型 forall a. t
,你可以在特定类型 a
上实例化它,如果对于所有 a :: k1
你得到 t :: k2
,那么这个多态类型就代表了一个 k1 ~> k2
类型的隐式类型函数。但是多态性/通用量化在这里无关紧要。重要的是 a
在表达式 t
中的出现方式,以及您可以将类型级表达式 t
表示为类型级函数的程度:
type Whatever a = t
或者如果 Haskell 有类型级别的 lambda,一个类型级别的 lambda,以 a
作为参数,t
作为它的主体:
Lambda a. t
试图认真地将forall a. t
视为善良的k1 -> k2
,您将一事无成。
基于对 ~>
的这种松散解释,他试图询问是否有一个新的种类级运算符 ==>
,使得种类级运算符 ~>
和类型级表达式 forall a. b
与新的假设种类级运算符 ==>
和类型级表达式 a => b
之间的关系相同。我认为解释这个问题的唯一合理方法是想象他想将类型表达式 a => b
视为被 a
参数化,就像他想象 forall a. b
被参数化一样通过 a
,所以他想考虑以下形式的类型级函数:
type Something a = a => b
并考虑Something
的种类。这里,Something
的种类是 Constraint ~> *
。所以,我猜他最后一个问题的答案是,“这两种实际上是一样的”,除了 ~>
之外,不需要其他种类级别的运算符。
Max 的回复解释说,扩展没有添加任何新的种类级别的运算符,而只是添加了一个新的原始种类,Constraint
与种类 *
和 {{1} 的语法级别相同}.种类级 #
运算符与类型级应用程序 ~>
具有相同的关系,无论涉及的原始种类是 f a
或 *
或 #
。因此,例如,给定:
Constratin
{-# LANGUAGE ConstraintKinds,RankNTypes #-}
type Whatever a = Maybe [a]
type Something a = a => Int
和 Whatever
的种类都用种类运算符 Something
表示(在 GHC 中,简写为 ~>
):
->
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。