Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation
Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation
复制标题
DOI：
10.1145/2535838.2535840
复制
发表时间：
2014-01
期刊：
影响因子：
--
通讯作者：
Giuseppe Castagna;K. Nguyen;Zhiwu Xu;Hyeonseung Im;Sergueï Lenglet;L. Padovani
中科院分区：
文献类型：
--
作者：
Giuseppe Castagna;K. Nguyen;Zhiwu Xu;Hyeonseung Im;Sergueï Lenglet;L. Padovani
这篇文章是关于高阶多态函数的微积分、带有箭头的递归类型和乘积类型构造函数以及集合论类型连接词（并、交和否定）的两篇文章系列的第一部分。在这第一部分中，我们定义和研究显式类型版本的演算，其中类型实例化是由显式实例化注释驱动。特别是，我们定义了一个显式类型的交集类型和一个有效的评估模型，它的演算。在第二部分，在同伴的论文中，我们定义了一个本地类型推理系统，允许程序员省略显式实例化注释，和一个类型重建系统，允许程序员省略显式类型注释。在这两篇文章中提出的工作提供了设计和实现高阶多态函数语言的半结构化数据所需的理论基础和技术机制。
This article is the first part of a two articles series about a calculus with higher-order polymorphic functions, recursive types with arrow and product type constructors and set-theoretic type connectives (union, intersection, and negation). In this first part we define and study the explicitly-typed version of the calculus in which type instantiation is driven by explicit instantiation annotations. In particular, we define an explicitly-typed lambda-calculus with intersection types and an efficient evaluation model for it. In the second part, presented in a companion paper, we define a local type inference system that allows the programmer to omit explicit instantiation annotations, and a type reconstruction system that allows the programmer to omit explicit type annotations. The work presented in the two articles provides the theoretical foundations and technical machinery needed to design and implement higher-order polymorphic functional languages for semi-structured data.