Inklings: a tumblelog

Type Theory and Functional Programming by Simon Thompson

Yet another book currently out-of-print but freely available in electronic form. More writers (or, more to the point, publishers) should do this kind of thing. It makes things better.