¶Abstract

In this essay I present the advantages and, I dare say, the beauty of programming in a language with set-theoretic types, that is, types that include union, intersection, and negation type connectives. I show by several examples how set- theoretic types are necessary to type some common programming patterns, but also how they play a key role in typing several language constructs—from branching and pattern matching to function overloading and type-cases—very precisely.

I start by presenting the theory of types known as semantic subtyping and extend it to include polymorphic types. Next, I discuss the design of languages that use these types. I start by defining a theoretical framework that covers all the examples given in the first part of the presentation. Since the system of the framework cannot be effectively implemented, I then describe three effective restrictions of this system: (i) a polymorphic language with explicitly-typed functions, (ii) an implicitly typed polymorphic language á la Hindley-Milner, and (iii) a monomorphic language that, by implementing classic union-elimination, precisely reconstructs intersection types for functions and implements a very general form of occurrence typing.

I conclude the presentation with a short overview of other aspects of these languages, such as pattern matching, gradual typing, and denotational semantics.

¶BiBTex

@Inbook{Castagna2024,
author="Castagna, Giuseppe",
editor="Meyer, Bertrand",
title="Programming with Union, Intersection, and Negation Types",
bookTitle="The French School of Programming",
year="2024",
publisher="Springer International Publishing",
address="Cham",
pages="309--378",
isbn="978-3-031-34518-0",
doi="10.1007/978-3-031-34518-0_12",
url="https://doi.org/10.1007/978-3-031-34518-0_12"
}