Guarded impredicative polymorphism
Guarded impredicative polymorphism
复制标题
受保护的命令式多态性
DOI：
10.1145/3192366.3192389
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
S. P. Jones
中科院分区：
文献类型：
--
作者：
A. Serrano;Jurriaan Hage;Dimitrios Vytiniotis;S. P. Jones
支持非断言实例化的类型系统的设计空间是极其复杂的。我们需要在表现力、对最终程序员和类型系统实现者的简单性以及系统与其他高级类型系统概念集成的容易程度之间取得平衡。在本文中，我们提出了一个新的设计空间点，我们称之为保护的不可预测性。它的关键思想是，在应用程序中，允许对类型构造函数下出现的类型变量进行非断言实例化。由此产生的类型系统有一个干净的声明性规范-使程序员很容易预测什么会输入什么不会输入-允许与GHC的OutsideIn（X）约束求解框架平滑集成，同时与HMF，HML，FPH和MLF等系统相比，在表达性方面放弃很少。我们给出了一个完善的推理算法，并证明了系统的一个主要类型性质。
The design space for type systems that support impredicative instantiation is extremely complicated. One needs to strike a balance between expressiveness, simplicity for both the end programmer and the type system implementor, and how easily the system can be integrated with other advanced type system concepts. In this paper, we propose a new point in the design space, which we call guarded impredicativity. Its key idea is that impredicative instantiation in an application is allowed for type variables that occur under a type constructor. The resulting type system has a clean declarative specification — making it easy for programmers to predict what will type and what will not —, allows for a smooth integration with GHC’s OutsideIn(X) constraint solving framework, while giving up very little in terms of expressiveness compared to systems like HMF, HML, FPH and MLF. We give a sound and complete inference algorithm, and prove a principal type property for our system.