Introductory Readings on Types

September 13, 2017

Here is a short list of useful resources about type systems, ranked roughly from practical to theoretical:

  1. Feldman, Richard. Making Impossible States Impossible. elm-conf 2016. https://youtu.be/IcgmSRJHu_8

    This is a clear, practical lesson on using the type system to utterly prevent certain kinds errors in your code by making it impossible to represent invalid program states—which is, after all, the whole point of having types in programming languages. It may be the most useful 25-minute video you watch all month. It assumes familiarity with Elm1, a statically typed, functional language for front-end web development; if you write much JavaScript, Elm is probably worth learning anyway.

  2. Brady, Edwin. Type-Driven Development with Idris. Manning Publications, Shelter Island, New York, 2017.

    In Type-Driven Development, Brady takes the idea of using the type system to make only valid states possible, and makes a whole methodology out of it. This book uses Brady’s own Idris programming language, which has a much more expressive type system than any mainstream language, but the ideas are more broadly applicable with some work by the reader.

  3. Cardelli, Luca. On Understanding Types, Data Abstraction, and Polymorphism. Computing Surveys, 17 (4). 471–522. http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf

    This is a relatively accessible explanation of several common features of type systems, and how they are used in actual languages. The exact languages used—such as Ada and Pascal—are a little dated, and there are some parts of the paper that may require a dictionary and a few rereadings, but it’s nevertheless a valuable introduction to the breadth of mainstream type systems.

  4. Cardelli, Luca. Type Systems. CRC Handbook of Computer Science and Engineering, 2nd Edition, CRC Press, Boca Raton, Florida, 2004, chapter 97. http://lucacardelli.name/Papers/TypeSystems.pdf

    “Type Systems” has a much more theoretical orientation and mathematical presentation than Cardelli’s previous paper. Cardelli explains the history of and rationale behind type systems in programming languages. He then explains the notation for formalizing type systems, and applies it to a several type systems for both imperative and functional languages. Without prior knowledge of type theory, you probably will not understand everything the first time you read this chapter.

  5. Pierce, Benjamin. Types and Programming Languages. MIT Press, Cambridge, Massachusetts, 2002.

    I have not actually yet read much of TAPL, but I like what I’ve seen so far. The writing is pretty straightforward and readable for such a complex topic, and assumes only moderate experience with discrete mathematics and a functional programming language. Pierce balances theory with practice; early exercises include both pen-and-paper manipulations of the lambda calculus, and actual programming of a Hindley-Milner type checker. TAPL is a good investment for the very curious and those interested in language design.

  1. http://elm-lang.org↩