Cardelli, Luca. 1991. Typeful programming. In Formal description of programming concepts, ed. Erich J. Neuhold and Manfred Paul. Berlin: Springer-Verlag.

Discuss this paper by editing this page.

This paper is long and we didn’t properly introduce it in our first meeting, so let me try to point out what to focus on as you read and think.

The technical core is Sections 4.3 (function types), 4.4 (tuple types), 4.5 (option types), 4.7 (recursive types), and 5 (operator kinds). Be sure to understand the example programs and try to vary them. To make sense of All/fun, ALL/Fun, and Tuple/tuple, you’ll probably need to read Section 3, whose figure (on page 9) is invaluable. You should see how to define Ok and Bool in Section 4.2 as a tuple and an option, respectively. The rest of the paper (especially Sections 6 and 7) shows these basic constructs in action.

The paper leaves the connection between types and logic implicit, so let me say a bit about that as well. As you might expect, “all” in the type system corresponds to “for all” (and “implies”) in logic; a function is a proof of a universally quantified proposition (or an implication). (See Table 25 in the other paper by Cardelli, cited below.) “Tuple” or “pair” in the type system corresponds to “exists” (and “and”) in logic; a tuple or pair is a proof of an existentially quantified proposition (or a conjunction). (See ibid., Tables 9, 11, 26.) Finally, “option” or “variant” in the type system corresponds to “or” in logic; an option or variant is a proof of a disjunction. (See ibid., Tables 10, 12.)

Cardelli, Luca. 1997. Type systems. In The computer science and engineering handbook, ed. Allen B. Tucker, Jr., chap. 103, 2208–2236. Boca Raton, FL: CRC Press.

-Ken