Programming with union, intersection, and negation types

authors: Giuseppe Castagna
year: 2024
url: https://doi.org/10.1007/978-3-031-34518-0₁2
publisher: Springer International Publishing
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.