Polymorphic Functions with Set-Theoretic Types
Polymorphic Functions with Set-Theoretic Types
复制标题
DOI：
10.1145/2775051.2676991
复制
发表时间：
2015-01
影响因子：
--
通讯作者：
Giuseppe Castagna;K. Nguyen;Zhiwu Xu;P. Abate
中科院分区：
文献类型：
--
作者：
Giuseppe Castagna;K. Nguyen;Zhiwu Xu;P. Abate
本文是关于具有递归类型和集合论类型连接词(并、交和否定)的类型系统中的高阶多态函数的定义的两篇系列文章的第二部分。在第一部分中，我们定义并研究了演算的显式类型版本的语法、语义和求值，在该版本中，类型实例化由显式实例化注释驱动。在第二部分中，我们介绍了一个局部类型推理系统，它允许程序员省略函数应用程序的显式实例化注释，以及一个类型重构系统，它允许程序员省略函数定义的显式类型注释。这两篇文章中介绍的工作提供了设计和实现具有并集和交集类型的高阶多态函数式语言和/或半结构化数据处理所需的理论基础和技术机制。
This article is the second part of a two articles series about the definition of higher order polymorphic functions in a type system with recursive types and set-theoretic type connectives (unions, intersections, and negations). In the first part, presented in a companion paper, we defined and studied the syntax, semantics, and evaluation of the explicitly-typed version of a calculus, in which type instantiation is driven by explicit instantiation annotations. In this second part we present a local type inference system that allows the programmer to omit explicit instantiation annotations for function applications, and a type reconstruction system that allows the programmer to omit explicit type annotations for function definitions. The work presented in the two articles provides the theoretical foundations and technical machinery needed to design and implement higher-order polymorphic functional languages with union and intersection types and/or for semi-structured data processing.