Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Programming with union, intersection, and negation types

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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

https://hal-cnrs.archives-ouvertes.fr/hal-03389659
Contributor : Giuseppe Castagna Connect in order to contact the contributor
Submitted on : Friday, October 29, 2021 - 12:29:39 PM
Last modification on : Sunday, November 7, 2021 - 3:10:57 AM

Files

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03389659, version 1
  • ARXIV : 2111.03354

Collections

Citation

Giuseppe Castagna. Programming with union, intersection, and negation types. 2021. ⟨hal-03389659⟩

Share

Metrics

Record views

30

Files downloads

14