haskell - 什么是 "System FC2 grammar for Kinds"？

Question

我正想把我的头绕在this blog post关于ConstraintKinds延期。
评论区有个帖子我全部不清楚，不知道，不懂。这里是:

Adam M says: _{14 September 2011 19:53 UTC}

Wow, this sounds great. Is it scheduled to be part of the official GHC 7.4? Also, does this mean that you've introduced a third production in the in System FC2 grammar for Kinds? Currently it has * and k~>k as the only alternatives where k1~>k2 is (basically) the kind of (forall a::k1 . (t::k2)). It sounds like this would add k1==>k2 which is the kind of (a::k1 => (t::k2)). Or are the two kinds actually the same?

有人可以吗，请一步一步地分析这个，或者至少提供一些链接，这将帮助我自己解决这个问题。我应该指出的一些关键时刻:

什么是“种类的系统 FC2 语法”？ (可能是主要和最通用的一个，其答案将嵌入其他两个。)

我试着解释为什么“k1~>k2(基本上)是 (forall a::k1 . (t::k2)) 的那种？据我了解，~>是 -> 的一些特殊符号在种类中，如 *和 k1 -> k2标准 Haskell 类系统的唯一居民(符合他们的描述:“目前它有 * 和 k~>k 作为唯一的选择”)。因此，(forall a::k1 . (t::k2))公式意味着如果我们取一个有人居住的类型 k1 ，它可以映射到另一个 k2如果它有人居住(由于 Curry-Howard 对类型的工作方式与对类型的工作方式相同)。那正确吗？ (PS:如果我不理解种类的居住概念，我会看到这种直觉是如何失败的；种类是否对应于 True 可证明的公式 (见评论)当他们有一个居住类型作为居民或任意类型？直觉在第二种情况下失败。)

=>有什么用k1==>k2 的公式中的平均值，即 (a::k1 => (t::k2)) ?

这条评论得到的回应:

Max says: _{14 September 2011 21:11 UTC}

Adam: it's not that complicated! It just adds the base kind Constraint to the grammar of kinds. This is a kind of types inhabited by values, just like the existing kinds * and #.

所以作者声称 Adam M 使扩展过于复杂。他们的 react 很容易理解。无论如何，即使Adam M的评论不是真的，我认为它完全值得关注，因为它向我介绍了一些不熟悉的概念。

Answer 1

“系统 FC2”是 Weirich 等人在 2010 年的论文“生成类型抽象和类型级计算”(link)中创造的一个术语。它指的是向 System FC 添加“角色”，并形成了在 2016 年论文 "Safe Zero-cost Coercions for Haskell 中描述的 GHC 中实现的基础。 .反过来，系统 FC 是最初在 this paper 中描述的系统。 (或者实际上是一篇较早的论文，这是出版后的扩展版本)，它扩展了系统 F 的常用多态 lambda 演算与类型相等。
然而 ，我认为 Adam M 可能不太正式地使用术语“系统 FC2”来指代撰写评论时 GHC 正在实现的任何类型的系统。所以，这句话的意思是:

introduced a third production in the System FC2 grammar for Kinds

是真的:

added a third production rule to the grammar of kinds, as kinds are currently implemented in GHC

他声称种类的语法目前有两个产生式规则:

*是一种

如 k1和 k2是种类，然后k1 ~> k2是一种。

他问这个扩展是否给出了第三个产生式规则:

如 k1和 k2是种类，然后k1 ==> k2是一种。

正如你所猜到的，他引入了运算符 ~>区分种类级箭头和类型级箭头。 (在 GHC 中，种类级和类型级箭头运算符的书写方式相同 ->。)他给出了 ~> 的定义。作为:

where k1~>k2 is (basically) the kind of (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，一个带有 a 的类型级别的 lambda作为参数和 t作为它的 body :

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语法水平与种类相同 *和 # .实物级~>运算符与类型级应用程序具有相同的关系 f a涉及的原始种类是否为*或 #或 Constratin .因此，例如，给定:

{-# LANGUAGE ConstraintKinds, RankNTypes #-}
type Whatever a = Maybe [a]
type Something a = a => Int

种类Whatever和 Something都用种类运算符 ~> 表示(在 GHC 中，简单地写成 -> ):

λ> :kind Whatever
Whatever :: * -> *
λ> :kind Something
Something :: Constraint -> *