Philip Wadler
Draft, March 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 solicited!
15 comments:
Hi, I have no useful comment on the contents except to say that it is a very interesting read!
However I found some typos:
2, §2 "Pricipia" -> "Principia"
2, §3 "Entsheidungsproblem" -> "Entscheidungsproblem"
2, §3 "Könisberg" -> "Königsberg"
2, §8 "how encode" -> "how to encode"
4, last §, missing reference for the four-color theorem
4, last §, "implementation of C" -> "implementation of a C compiler"
7, §2 "being" -> "begin"
Dear Unknown, Thank you! Corrections now made. Thanks also to Daniel Marsden and Gabor Grief, who e-mailed corrections.
If folk post their name with their corrections, I will add an acknowledgement.
I'm "Unknown" above, Blogger wasn't configured to display my name but it is now fixed.
Hey Philip, great paper....minor pedantic suggestion. "Buses" is probably a better plural for bus than "busses" - the later probably means a number of kisses or perhaps a number of those electrical connector thingies.
Here's a StackExchange commentary on it:
http://english.stackexchange.com/questions/48421/what-is-the-preferred-plural-form-of-bus
- Keith
Page 2: (untyped lambda) calclus
page 4: Subequently,
Typos I've found:
p.2: "baldly claimed"
p.4: "resource concious"
Thanks, Mikhail. 'Baldly' not a typo; a 'bald' claim is one unadorned by justification. Thanks for catching misspell of 'conscious'.
Typo page 1: "Martin-Löf" instead of "Martin Löf".
Here are some comments (not already posted, I think).
Typos in brackets:
- p 2 "...recursive functions, and Turing [M]achines.
- p 4 "...In classical, intuitionistic, and modal logic[,] any hypothesis..."
- I found it jarring that the reference to Fig. 3 came after that to Fig. 4. Likewise with Fig. 7 and 8.
- It would have been nice if you could have sneaked a small dependent types/predicate logic example into the paper, but perhaps you were short on room.
Great paper!
Thank you, Lee.
The references I checked have Turing machine, not Turing Machine.
Referring to Figure 4 before Figure 3 is jarring, but I want to keep the figures in logical order (general rule before example). Do you think I should just give in and swap the figures, or do you have a suggested fix?
I would love a simple example of dependent types that has a clear reading both as a proof and a program. If you have such an example, please post it here.
Typo fixed and acknowledgement added.
> The references I checked have Turing machine, not Turing Machine.
My comment was just about consistency---you have it capitalized in a few places, it appears.
> Do you think I should just give in and swap the figures, or do you have a suggested fix?
I think a forward reference in the text would be sufficient, so the reader doesn't get confused. Something like, "Now consider a larger proof built from this smaller proof, as shown at the top of Figure 4, that we will shortly describe how to simplify using the rules from Figure 3."
> I would love a simple example of dependent types that has a clear reading both as a proof and a program. If you have such an example, please post it here.
Good point! Let me think about that.
Dr. Wadler -
Just wanted to drop a note to say that this paper is FANTASTIC. It helps cement many concepts that I've been trying for a while now to keep in my head at once. You're amazing! Thanks for sharing.
Best,
Michael R. Bernstein
http://michaelrbernste.in
What a fun paper! Loved it.
I found two typos, both in the second column of the second page:
"... at this time, the term referred [to] a human performing a computation ..."
"... while the application of lambda calculus to logic requires [that] every program halt."
Cheers,
Tom Moertel
Thanks, Tom. Typos corrected and acknowledgement added.
Post a Comment