没有使用polytype变量，Rank2Types/RankNTypes是否实用？

Question

由于类型变量不能持有多态类型，因此似乎在Rank*Types中无法重用现有函数，因为它们具有单态限制。

例如，当中间类型是多态类型时，我们无法使用函数(.)。我们被迫在现场重新实现(.)。当然，对于(.)这样的小问题来说，这很琐碎，但对于更实质性的代码主体而言，这是一个问题。

我认为，使((f . g) x)与(f (g x))不等价，对引用透明性及其好处来说是一个严重的打击。

在我看来，这是一个致命的问题，似乎使得Rank*Types扩展几乎不适合广泛使用。

我有什么遗漏的地方吗？是否有计划使Rank*Types更好地与其他类型系统交互？

编辑：如何使(runST . forever)的类型工作？

- Peaker

Answer 1

最近关于Rank-N类型的提议是Don的链接FPH论文。在我看来，它也是其中最好的一个。所有这些系统的主要目标是尽可能少地需要类型注释。问题在于，从Hindley/Milner到System F时，我们失去了主类型，类型推断变得不可判定，因此需要类型注释。

“盒状类型”工作的基本思想是尽可能地传播类型注释。类型检查器在类型检查和类型推断模式之间切换，希望不再需要更多的注释。缺点在于是否需要类型注释很难解释，因为它取决于实现细节。

Remy的MLF系统是迄今为止最好的提议；它需要最少量的类型注释，并且在许多代码转换下是稳定的。问题在于它扩展了类型系统。以下标准示例说明了这一点：

choose :: forall a. a -> a -> a
id :: forall b. b -> b

choose id :: forall c. (c -> c) -> (c -> c)
choose id :: (forall c. c -> c) -> (forall c. c -> c)

以上两种类型在System F中都是可接受的。第一种是标准的Hindley/Milner类型，使用谓词实例化，第二种使用非谓词实例化。两种类型都不比另一种更通用，因此类型推断必须猜测用户想要哪种类型，这通常是一个坏主意。

相反，MLF通过有限量词扩展了System F。上面示例的主要（=最普遍）类型将是：

choose id :: forall (a < forall b. b -> b). a -> a

你可以将其解读为“choose id 具有类型 a 到 a，其中 a 必须是 forall b. b -> b 的实例。”有趣的是，仅凭这一点并不比标准的 Hindley/Milner 更加强大。因此，MLF 还允许进行刚性量化。以下两种类型是等价的：

(forall b. b -> b) -> (forall b. b -> b)
forall (a = forall b. b -> b). a -> a

介绍刚性量化通过类型注释引入，技术细节确实相当复杂。优点是，MLF只需要非常少的类型注释，并且有一个简单的规则确定何时需要它们。缺点是：

- 类型可能变得更难读，因为“<”右侧可能包含进一步嵌套的量化。 - 直到最近，MLF没有明确类型的变体。这对于类型编译器转换（例如GHC）很重要。Boris Yakobowski的博士论文的第3部分首次尝试了这样的变体。（第1和2部分也很有趣；它们通过“图形类型”描述了更直观的MLF表示。）

回到FPH，其基本思想是在内部使用MLF技术，但要求在let绑定上添加类型注释。如果您只需要Hindley / Milner类型，则无需注释。如果您需要更高秩的类型，则需要在let（或顶层）绑定处指定请求的类型。

FPH（类似于MLF）支持无限制实例化，因此我认为您的问题不适用。 因此，它应该没有问题来对您上面的f . g表达式进行类型标记。 但是，GHC尚未实现FPH，并且很可能不会实现。 困难在于与等式强制和可能的类型类约束的交互。 我不确定最新状态是什么，但我听说SPJ想要远离无限制实例化。 所有这些表达力都是有代价的，到目前为止还没有找到负担得起并且全面的解决方案。

- nominolo

Answer 2

关于ImpredicativeTypes：我相信这并不影响peaker的问题。该扩展与数据类型有关。例如，GHC会告诉你：

Maybe :: * -> *
(forall a. a -> a) :: *

然而，这种说法有点虚假。在一个不可预测的系统中是正确的，在这样的系统中，你可以编写以下代码：

Maybe (forall a. a -> a) :: *

并且它将正常运行。这就是ImpredicativeTypes所能实现的。如果没有这个扩展，适当的思考方式应该是：

Maybe :: *m -> *m
(forall a :: *m. a -> a) :: *p

因此，在尝试构建应用程序时会存在一种不匹配的情况。

然而，GHC在泛型类型方面相当不一致。例如，我上面给出的id函数的类型为：

id :: (forall a :: *m. a -> a)

但是启用了RankNTypes，而未启用ImpredicativeTypes的情况下，GHC将很乐意接受这个注释：

id :: (forall a. a -> a) -> (forall a. a -> a)

尽管forall a. a -> a不是单态（monotype），但它允许应用标注来使用只与(->)一起使用的量化变量的非预测实例化。但我猜它本身不会这样做，这导致了runST $ ...的问题。曾经有一个特定的实例化规则解决了这个问题（我从未完全理解其细节），但该规则不久后被删除。

- Dan Doel

Answer 3

有没有计划使Rank*Types与类型系统的其他部分更好地互动？

考虑到ST Monad的普遍性，至少Rank2类型足够普遍以证明相反的观点。然而，您可以查看“sexy/boxy types”系列论文，了解如何处理任意等级多态性并与其他方法更好地配合使用。

请参见FPH : First-class Polymorphism for Haskell ，Dimitrios Vytiniotis，Stephanie Weirich和Simon Peyton Jones，提交给ICFP 2008。

此外，请参见-XImpredicativeTypes ——有趣的是，该扩展已标记为过时！

- Don Stewart