From SIPB Cluedumps
Haskell: Compiler as Theorem-Prover
|Date: November 19, 2007, at 3:30 PM|
|Presenters: Greg Price (price)|
| Notes: UPDATE May 2008: Jesse has a new implementation of session types, complete with a paper explaining it and prototype implementations in five other languages.
For protocol/session types, see the literature, or check out Oleg Kiselyov's work, particularly "HList", for some of the tools that make Jesse Tov's Haskell implementation, which I presented, possible. Or look at Jesse's web page to see if he's put up a paper or a new version. UPDATE: he has, see above.
For "theorems for free", see Phil Wadler's 1989 and later writeups.
| Abstract: Haskell is the world's most *reasonable* programming language. Every language's optimizing compilers reason about programs, and every programmer reasons about the code they write ("this loop never indexes this array out of bounds"; "this resource is never accessed without holding the lock") -- but in no more mainstream language do the compiler and the programmer have an adequate medium in which to communicate about their reasoning: a rich static type system. In Haskell the programmer has in the type system a powerful theorem-prover ready at hand, and if the programmer's theorem is of the form "task X can be done", the compiler's proof can be the very code that carries out task X.
This cluedump will briefly introduce Haskell and its type system, describe the Curry-Howard isomorphism between code with types and propositions with proofs, and show you how you can make a Haskell implementation verify the units you attach to physical quantities; guarantee code to be free of side effects; write code for you to traverse a complicated data structure; and guarantee your lock-free code threadsafe with software transactional memory.