Abstract: “There exists an identifiable programming style based on the widespread use of type information handled through mechanical typechecking techniques. This typeful programming style is in a sense independent of the language it is embedded in; it adapts equally well to functional, imperative, object-oriented, and algebraic programming, and it is not incompatible with relational and concurrent programming.
The main purpose of this paper is to show how typeful programming is best supported by sophisticated type systems, and how these systems can help in clarifying programming issues and in adding power and regularity to languages.
We start with an introduction to the notions of types, subtypes and polymorphism. Then we introduce a general framework, derived in part from constructive logic, into which most of the known type systems can be accommodated and extended. The main part of the paper shows how this framework can be adapted systematically to cope with actual programming constructs.
For concreteness we describe a particular programming language with advanced features; the emphasis here is on the combination of subtyping and polymorphism. We then discuss how typing concepts apply to large programs, made of collections of modules, and very large programs, made of collections of large programs. We also sketch how typing applies to system programming; an area which by nature escapes rigid typing. In summary, we compare the most common programming styles, suggesting that many of them are compatible with, and benefit from, a typeful discipline.”
by Luca Cardelli
Cardelli is impressive and this paper (which is kind of a little book) is a seminal work and one of the best papers I have (n)ever (finished) read(ing).
Thank you for posting it!
By the way, it is worth to take a look at Cardelli’s other works. He is what HN loves to call a polyglot and his works on not-standard computation and bioinformatics/computational biology are impressive.
Cardelli is amazing. My favorite work of his was Modula-3. It was a safe, systems language that nicely balanced features vs simplicity, compile speeds, running speeds, safe-by-default, unsafe if necessary, and built-in concurrency. There was some formal verification on standard library, too. SPIN OS was a notable use.