Visible Type Application
Visible Type Application
复制标题
可见型应用
DOI：
10.1007/978-3-662-49498-1_10
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Hamidhasan G. Ahmed
中科院分区：
文献类型：
--
作者：
R. Eisenberg;Stephanie Weirich;Hamidhasan G. Ahmed
Hindley-Milner HM类型系统自动推断多态函数的类型。在HM中，推断类型是明确的，并且每个表达式都有一个主类型。类型注释使HM与不可能进行完整类型推断的扩展兼容，例如高阶多态性和类型级函数。然而，程序员不能使用注释来显式地为多态函数提供类型参数，因为HM需要推断类型实例。
我们描述了一个扩展HM，允许可见类型的应用程序。我们的扩展需要一个新的类型推理算法，但它的声明式表示是一个简单的扩展HM。我们证明了我们的扩展系统是HM的保守扩展，并承认主类型。然后，我们将我们的方法扩展到具有双向类型检查的高阶类型系统。我们已经实现了这个系统中的格拉斯哥Haskell编译器，并显示我们的方法如何在复杂的类型系统功能的存在下扩展。
The Hindley-Milner HM type system automatically infers the types at which polymorphic functions are used. In HM, the inferred types are unambiguous, and every expression has a principal type. Type annotations make HM compatible with extensions where complete type inference is impossible, such as higher-rank polymorphism and type-level functions. However, programmers cannot use annotations to explicitly provide type arguments to polymorphic functions, as HM requires type instantiations to be inferred.
We describe an extension to HM that allows visible type application. Our extension requires a novel type inference algorithm, yet its declarative presentation is a simple extension to HM. We prove that our extended system is a conservative extension of HM and admits principal types. We then extend our approach to a higher-rank type system with bidirectional type-checking. We have implemented this system in the Glasgow Haskell Compiler and show how our approach scales in the presence of complex type system features.