Programming with union, intersection, and negation types.
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.
Read in full here:
This thread was posted by one of our members via one of our news source trackers.