Philip Wadler - Propositions as Types (Lambda Days 2016)

Slides and more info: www.lambdadays.org/lambdadays2...
Alternative recording: • "Propositions as Types...
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. Learn why functional programming is (and is not) the universal programming language.

[@sophiagold5892]

The slide around 42:09 showing the various correspondences between forms of logic and model of computation is worth everything for me. The one part I find particularly interesting, and am unsure how much is supported in the literature, is the association of modal logic with monads. I can see what Wadler is getting at with that, but would argue monads are at best just a special case of the correspondence and possibly not at all (I can't see any relationship outside the context of computer science). A better candidate might be actor model theory, as Hewitt himself argued for lexical scope as representing possible worlds and even mentioned them being temporally quantified. In the original actor model paper he coauthored with Bishop & Steiger, environments are referred to as "extension worlds," which give rise to the concept of "world directed invocation" that proposes an embedding of intuitionistic logic through "alternative worlds" and "perceptual viewpoints."

[@His-Soldier]

Model logic itself is essentially a focus on special correspondences . So that would make sense. The degree your suggested correspondence would be correct is perhaps just another area of specialised isomorphism between monads and logical systems with expressions for modalities.

[@OttoNascarella]

I wish he was my grandfather...

[@dgphi]

The link to the slides is broken. This is where it should go: www.lambdadays.org/lambdadays2016/philip-wadler

[@jovaha]

Thanks for that. Good lecture and funny guy to.

[@zapazap]

The problem at 51:00 is this. Given the two statements
(i) I cannot conceive of a universe where Modus Ponens does not hold.
(ii) There exists [or can exist] no universe where Modus Ponens does not hold.
I have no problem with his claiming (i). But he then goes on to claim (ii) as if it follows immediately from (i).
It doesn't.

[@GeorgWilde]

Depend's on whether you are idealist, anti-realist, or realist.

[@acykablyatley]

it might be more of a recognition of what we call existence is something we can conceive, rather than an assertion that we can conceive anything that exists.

[@gillbates2685]

You missed the point completely. He was not making a deduction from (i) to (ii).
It's simply him expressing his conviction that there is no universe where Modus Ponens does not hold.
This is the drawback of giving speech (as opposed to writing paper), if you are not eloquent at all time some people who don't understand the point will nitpick some details where you absentmindedly say your thoughts out of order, or when you stutter.
He wanted to say "There is no universe where Modus Ponens does not hold, I cannot conceive of it".
There's no (i) -> (ii)
And the point to justify this belief (that he implied) is: there is a fundamental difference between
(1) proposition about weak electromagnetic force
and
(2) Modus Ponens.
(1) is true of this universe, hence a universal law. It is fact based. It might not be true of other universes e.g. one where there is no matter.
(2) isn't even dependent on the physical world, it is form based, hence calling it "universal" isn't quite right. In universe with completely different physical laws, if A is true and B follow from A, then B is true, with or without matter, energy, field. That's his point. Students who took introductory logic classes can understand this.

[@gillbates2685]

If you want more formal justification, these are claims of modal logic i.e. it involves the notion of possible worlds.
A possible world is a complete and consistent way the world is or could have been.
Modal logic adds two extra operators to predicate logic: possibility and necessity.
So the law about weak electromagnetic force is a "possible" truth: it is true in a "possible world" i.e. our world/universe.
Modus Ponens on the other hand is an inference rule to build modal logic (actually, all usable logics from classical to intuitionistic all have Modus Ponens), it is not even in the same category as propositions to be assigned truth values.
How do you justify using Modus Ponens? by simply explore its consequence and show how logics built from it have all the properties you want (completeness, soundness etc).
You may assume something else and deduce MP, but then your logic would just look ugly.
If you want to assume nothing to "prove" it, then you have stopped doing logic :))
Anyway his point is Modus Ponens/Lambda Calculus isn't merely "universal" because it's not tied to any constraints of this universe or any other.
cf. en.wikipedia.org/wiki/Modal_logic

[@ElizaberthUndEugen]

26:40
what?? To get to that result he had to do the exact same thing in the step before where
[B] [A]
----------- &-I
B & A
That is the same thing as
[A] [B]
----------- &-I
A & B
so where was the point in this whole deduction of A & B if it just follow from the &-I rule?

[@andresgoens]

2 years late, but since there is no answer, I'll give one: the point is that at 25:00 he is introducing another premise to the right, assuming B and assuming A he can deduce B & A, and that PLUS the proof that B & A implies A & B yields A & B. All of that is the proof he's simplifying, not the A & B implies B & A part. That whole proof he can simplify to the last part, that assuming A and assuming B yields A & B, because the implication (A & B implies B & A) was just an intermediate step to prove A & B.

[@jamiebertram9744]

Jeez, you guys gotta do better editing in your videos... That's the second one so far where the slides aren't visible for half the talk.