Advanced Topics in Types and Programming Languages edited by Benjamin Pierce
I’d been meaning to read this book for a while, and managed to buy it with various present money after Xmas. It consists of ten chapters by different authors on ten topics ranging from type systems to proof-carrying code.
The first three chapters discuss various type systems – substructural type systems which control the use of variables in the type context and which lead to linear typing in one of the variants, dependent types where you are allowed to do calculations at the type level and which is being popularised by languages such as Idris, and a very interesting chapter on effect systems which discusses the region-based memory management work on Tofte and Talpin. In the latter work, the type of a program contains information about the allocation contexts which can allow the runtime to manage dynamic memory using a stack based approach.
The next two chapters cover the low level use of types. Typed assembly language would allow assembly language to be typed to check properties such as memory safety, and proof carrying code allows an executable to contain proof of its own safety and enough information for the safety to be checked by the target that is going to execute the code.
The next two chapters cover methods for reasoning about programs using their types, followed by a fantastic section on types for programming in the large. This section contains a chapter on the design considerations of the ML type system – this was very interesting. This section also contains a chapter on type definitions.
The last chapter is on type inference and discusses the typing of ML programs using constaint solving, rather than the usual unification based Hindley-Milner approach.
The book contains loads of interesting idea, but some of the theory is perhaps a little off-putting. If you really want to grips with the details, there are lots of exercises, or you can choose to simply skim these and still keep up with the exposition.