haskell - Rank2Types/RankNTypes 在没有多型变量的情况下是否实用？

Question

由于类型变量不能容纳多类型，似乎使用 Rank*Types 我们不能重用现有函数，因为它们的单型限制。

例如，当中间类型是多类型时，我们不能使用函数 (.)。我们被迫在现场重新实现(.)。这对于 (.) 来说当然是微不足道的，但对于更重要的代码体来说是一个问题。

我还认为使 ((f . g) x) 不等于 (f (g x)) 对引用透明度及其好处造成严重打击。

在我看来，这似乎是一个引人注目的问题，并且似乎使 Rank*Types 扩展对于广泛使用几乎不切实际。

我错过了什么吗？是否有计划让 Rank*Types 与类型系统的其余部分更好地交互？

编辑:您如何使 (runST . forever) 的类型有效？

Answer 1

Rank-N 类型的最新提议是 Don 的链接 FPH 论文。在我看来，它也是最好的。所有这些系统的主要目标是需要尽可能少的类型注释。问题是，当从 Hindley/Milner 到 System F 时，我们会丢失主要类型，并且类型推断变得无法确定——因此需要类型注释。

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

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's PhD thesis 第 3 部分首次尝试了这种变体。 (第 1 部分和第 2 部分也很有趣；它们通过“图形类型”描述了一种更直观的 MLF 表示。)

回到 FPH，它的基本思想是在内部使用 MLF 技术，但需要在 let 上进行类型注释。绑定(bind)。如果您只需要 Hindley/Milner 类型，则不需要注释。如果您想要更高级别的类型，您需要指定请求的类型，但仅限于 let (或顶级)绑定(bind)。

FPH(如 MLF)支持强制实例化，所以我认为您的问题不适用。因此，输入您的 f . g 应该没有问题。上面的表达。但是，FPH 尚未在 GHC 中实现，而且很可能不会实现。困难来自与平等强制(以及可能的类型类约束)的交互。我不确定最新的状态是什么，但我听说 SPJ 想要摆脱不可靠的状态。所有这些表现力都是有代价的，到目前为止，还没有找到负担得起的全方位解决方案。