¶Abstract

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.

¶BiBTex

@inproceedings{10.1145/2676726.2676991,
author = {Castagna, Giuseppe and Nguyen, Kim and Xu, Zhiwu and Abate, Pietro},
title = {Polymorphic Functions with Set-Theoretic Types: Part 2: Local Type Inference and Type Reconstruction},
year = {2015},
isbn = {9781450333009},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2676726.2676991},
doi = {10.1145/2676726.2676991},
booktitle = {Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
pages = {289–302},
numpages = {14},
keywords = {xml, types, type constraints, semantic subtyping, polymorphism, intersection types},
location = {Mumbai, India},
series = {POPL '15}
}

@article{10.1145/2775051.2676991,
author = {Castagna, Giuseppe and Nguyen, Kim and Xu, Zhiwu and Abate, Pietro},
title = {Polymorphic Functions with Set-Theoretic Types: Part 2: Local Type Inference and Type Reconstruction},
year = {2015},
issue_date = {January 2015},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {50},
number = {1},
issn = {0362-1340},
url = {https://doi.org/10.1145/2775051.2676991},
doi = {10.1145/2775051.2676991},
journal = {SIGPLAN Not.},
month = jan,
pages = {289–302},
numpages = {14},
keywords = {xml, types, type constraints, semantic subtyping, polymorphism, intersection types}
}