haskell - 没有多型变量，Rank2Types/RankNTypes是否可行？

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

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

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

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

我想念什么吗？是否有计划使Rank * Types与其余类型系统更好地交互？

编辑:如何使(runST。永远)的类型计算出来？

最佳答案

针对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)

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

MLF则用有界量化扩展了系统F。上面示例的主体(=最通用)类型为:

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

您可以将其读为“choose id的类型为a，其中a必须是a的实例”。

有趣的是，仅此一项就没有标准的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技术，但需要在forall b. b -> b绑定(bind)上进行类型注释。如果只需要Hindley / Milner类型，则不需要任何注释。如果要使用更高级别的类型，则需要指定请求的类型，但只能在let(或顶级)绑定(bind)处指定。

FPH(如MLF)支持强制性实例化，因此我认为您的问题不适用。因此，在上面键入您的let表达式应该没有问题。但是，FPH尚未在GHC中实施，很可能不会实施。困难来自与相等强制的交互(可能还有类型类约束)。我不确定最新的状态是什么，但是我听说SPJ希望摆脱障碍。所有这些表达能力都是有代价的，到目前为止，还没有找到负担得起的，全面的解决方案。

关于haskell - 没有多型变量，Rank2Types/RankNTypes是否可行？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/3076909/