Posted on February 21, 2014
by Kwang Yul Seo
Tags: Combinatory logic, Curry-Howard Isomorphism, Djinn, Girard-Reynolds, Hindley-Milner, Intuitonistic logic, lambda calculus, Lennart Augustsson, Phil Gossett
A talk by Phil Gossett given in Google’s Advanced Programming Language series is the best explanation of Curry-Howard isomorphism I’ve seen.
He briefly mentioned the origin of type system at the beginning and explained Hindley-Milner, Type Classes (Wadler-Blott), Curry-Howard and Girard-Reynolds. Especially, he showed the relationship between parametricity and Girard-Reynolds isomorphism.
He finished his talk by describing Lennart Augustsson’s Djinn, which is small program that takes a (Haskell) type and gives you back a function of that type if one exists.
In his talk, he gave some examples of Curry-Howard isomorphism.
- Intuitonistic logic <-> Combinatory logic (-> Lambda Calculus)
- Girard representation theorem <-> Reynolds abstraction theorem
- F2 <-> P2
BTW, there are a few technical errors in the talk. Please refer to Wadler’s comment on the talk.