Practical type inference for arbitrary-rank types
Practical type inference for arbitrary-rank types
复制标题
DOI：
10.1017/s0956796806006034
复制
发表时间：
2007-01-01
影响因子：
1.1
通讯作者：
Shields, Mark
中科院分区：
文献类型：
--
作者：
Jones, Simon Peyton;Vytiniotis, Dimitrios;Shields, Mark
Haskell的受欢迎程度推动了对更具表现力的系统功能的需求，其中大多数威胁到Damas-Milner类型推理的可决定性和实用性。这样的功能之一就是能够使用较高级别的类型编写功能的能力 - 即将多态函数作为其参数的功能。已知完整的推理对于更高级别（不可思议的）类型系统是不可确定的，但是实际上，程序员非常愿意添加类型的注释来指导类型推理引擎并记录其代码。但是，选择公正的注释以及类型系统及其推理算法所需的更改是一个持续的研究主题。我们将Odersky和Laufer提出的Lambda-Calculus作为起点。他们的系统通过在lambda结合参数和任意子范围内开发类型注释来支持任意的多态性。虽然优雅，而且比其他一些建议更方便，但Odersky和Laufer的系统需要许多注释。我们展示了如何使用局部类型推理（由Pierce和Turner发明）大大减轻注释负担，以至于高级类型变得非常可用。高级类型对类型推理具有非常适中的影响。我们以非常具体的方式来证实这一说法，通过为传统的Damas-Milner类型系统介绍完整的类型 - 推动引擎，然后展示如何扩展其以扩展到更高级别的类型。我们使用Monadic框架编写类型 - 推动引擎：事实证明，这是一个在动作中的单调的特别令人信服的例子。该论文很长，但在风格上是强烈的教程。尽管我们将Haskell用作示例源语言和实施语言，但我们的大部分工作直接适用于任何类似ML的功能语言。
Haskell's popularity has driven the need for ever more expressive type system features, most of which threaten the decidability and practicality of Damas-Milner type inference. One such feature is the ability to write functions with higher-rank types - that is, functions that take polymorphic functions as their arguments. Complete type inference is known to be undecidable for higher-rank (impredicative) type systems, but in practice programmers are more than willing to add type annotations to guide the type inference engine, and to document their code. However, the choice of just what annotations are required, and what changes are required in the type system and its inference algorithm, has been an ongoing topic of research. We take as our starting point a lambda-calculus proposed by Odersky and Laufer. Their system supports arbitrary-rank polymorphism through the exploitation of type annotations on lambda-bound arguments and arbitrary sub-terms. Though elegant, and more convenient than some other proposals, Odersky and Laufer's system requires many annotations. We show how to use local type inference (invented by Pierce and Turner) to greatly reduce the annotation burden, to the point where higher-rank types become eminently usable. Higher-rank types have a very modest impact on type inference. We substantiate this claim in a very concrete way, by presenting a complete type-inference engine, written in Haskell, for a traditional Damas-Milner type system, and then showing how to extend it for higher-rank types. We write the type-inference engine using a monadic framework: it turns out to be a particularly compelling example of monads in action. The paper is long, but is strongly tutorial in style. Although we use Haskell as our example source language, and our implementation language, much of our work is directly applicable to any ML-like functional language.