最近关于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想要远离无限制实例化。 所有这些表达力都是有代价的,到目前为止还没有找到负担得起并且全面的解决方案。