Polymorphic Functions with Set-Theoretic Types. Part 1: Syntax, Semantics, and Evaluation
Résumé
We define and study the type system, local type inference, and execution model for a calculus with higher-order polymorphic functions, recursive types with arrow and product type constructors and set-theoretic type connectives (union, intersection, and negation). This work provides the theoretical foundations and technical machinery needed to design and implement higher-order polymorphic functional languages for semi-structured data and is presented in two parts. 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 show why this requires to solve the longstanding problem of the definition of an explicitly-typed λ-calculus with intersection types, we solve it, and define an efficient evaluation model for it. In the second part, described in a companion paper, we present 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.