27.6.14

 

Propositions as Types, updated

Propositions as Types has been updated. Thanks to all the readers and reviewers who helped me improve the paper.

Propositions as Types
Philip Wadler
Draft, 26 June 2014

The principle of Propositions as Types links logic to computation. At first sight it appears to be a simple coincidence---almost a pun---but it turns out to be remarkably robust, inspiring the design of theorem provers and programming languages, and continuing to influence the forefronts of computing. Propositions as Types has many names and many origins, and is a notion with depth, breadth, and mystery.
Comments still solicited!

Labels: , , ,


Comments:
There are two threads on the homotopy type theory list that may be of interest if you take another pass over this paper:

https://groups.google.com/forum/#!topic/homotopytypetheory/o-cVRGFF-Ig

and

https://groups.google.com/forum/#!topic/homotopytypetheory/OzCQ6vrzAN0

On the latter, the place to begin reading is Streicher's message of January 15. I believe he address a common misconception, which your paper does not participate in, but nor does it directly challenge -- the idea that since all propositions may be given types, then we must associate all types with propositions. This leads to such silliness as Haskell users being introduced to Curry-Howard asking what the proposition is corresponding to the type of hGetLine. (Ok, sure, this is not entirely silly, but still..).

The former thread also points to a lacunae in your paper, but again one that you are perfectly within your rights to not address -- the unfortunate (in my mind) underplaying of the role of realizability with regards to the notion of "proofs as computations." This is in a sense not directly in the CH lineage the same way BHK is, but nonetheless, it was an important step in a similar direction. Of course your paper is not just a discourse on history, but is a work intended for education and exposition, so this may all be a bit besides the point.
 
@sclv: Thanks!

It is not clear to me where Kleene's work on realisability sits in the history. Is it simply a fleshing out of BHK, or did it make a more profound contribution?

Regarding 'Propositions as Types' vs 'Types as Propositions': if it is an isomorphism, then there should be correspondences both ways. In that sense, 'What is the proposition corresponding to Nat?' or 'What is the proposition corresponding to the type of hGetLine?' is not a completely silly question. The first might be answered in terms of the definition of Nat in F2, which equates naturals with an induction principle, the second might (partially) be answered by observing the correspondence between monads and one variant of modal logic.
 
Post a Comment

<< Home

This page is powered by Blogger. Isn't yours?