Wadler's Blog

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.