Wadler's Blog

A talk by Phil Gossett given in Google's Advanced Programming Language series. Cites my work on type classes and the Girard-Reynolds isomorphism; I was pleased to see he began by discussing Frege and Russell, and finished by describing Lennart Augustsson's Djinn. Nice talk, and has me looking forward to speaking at Google (which I'm scheduled to do this Friday); my talk will cover some similar material. (I tried to find Gossett's e-mail and failed, maybe this will help me get in touch.)

I spotted a couple of technical errors in the talk. (1) He suggested that the Girard-Reynolds Isomorphism guarantees that every term that has a given polymorphic type is isomorphic; in fact, distinct proofs of a theorem correspond to distinct terms of a type. (2) In answer to a question, he said that parametricity does not extend to type classes; in fact, my paper Theorems for Free includes a sketch of how parametricity does extend to type classes (see Section 3.4).