什么是“种类的系统 FC2 语法”？

编程问答 2022-05-10

问题描述

我正在尝试围绕 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))。还是这两种其实是一样的？

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

  1. 什么是“种类的 System FC2 语法”？ （可能是主要和最通用的一个，其答案将嵌入其他两个。）
  2. 我试着解释为什么“k1~>k2（基本上）是那种(forall a::k1 . (t::k2))”？据我了解，~> 是 -> 在种类中的一些特殊符号，因为 * 和 k1 -> k2 是标准 Haskell 种类系统的唯一居民（符合他们的描述： “目前它有 * 和 k~>k 作为唯一的选择”）。因此，(forall a::k1 . (t::k2)) 公式意味着如果我们采用一个有人居住的类型 k1，它可以映射到另一个 k2，当它是有人居住的（由于 Curry-Howard 为类型工作它对类型的工作方式相同）。是对的吗？ （PS：如果我不理解类的居住概念，我会看到这种直觉是如何失败的；当它们有一个居住类型作为居住类型还是任意类型？在第二种情况下直觉失败。）
  3. => 的公式中的 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 中实现

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

  1. * 是一种
  2. 如果 k1 和 k2 是种类，则 k1 ~> k2 是种类。

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

  1. 如果 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 中，简写为 ~>）：

->
constraintsfunctional-programminghaskellhaskelltype-kindstype-theory