Future of Coding â€˘ Episode 68
Philip Wadler â€˘ Prop...

# share-your-worki

Ivan Reese

11/19/2023, 6:02 AM

Future of Coding â€˘ Episode 68
Philip Wadler â€˘ Propositions as Types
đ’‚¶ https://futureofcoding.org/episodes/068
The subject of this episodeâ€™s paper â€” Propositions as Types by Philip Wadler â€” is one of those grand ideas that makes you want to go stargazing. To stare out into space and just disassociate from your body and become one with the heavens. *Everything â€” life, space, time, existence â€” all of it is a joke!* A cosmic ribbing delivered by the laws of the universe or some higher power or, perhaps, higher order. Humanity waited two thousand years, from the time of the ancient Greeks through until the 1930s, for a means to answer questions of calculability, when three suddenly arrived all at once:
â€˘ General recursive functions by GĂ¶del in 1934, with functions of sets of natural numbers.
â€˘ Lambda calculus by Alonzo Church in 1936, with anonymous single-variable functions.
â€˘ Turing machines by Alan Turing in 1937, with a process for evaluating symbols on a tape.
Then it was discovered that these three models of computation were, in fact, perfectly equivalent. That any statement made in one could be made in the others. A striking coincidence, sure, but not without precedent. But *then* it was quietly determined (in 1934, again in 1969, and finally published in 1980) that computation itself is in a direct correspondence with logic. That every proposition in a given logic corresponds with a type in a given programming language, every proof corresponds with a program, and the simplification of the proof corresponds with the evaluation of the program.
The implications boggle the mind. *How could this be so?* Well, how could it be any other way? Why did it take so long to discover? What other discoveries like this are perched on the precipice of revelation?
Philip Wadler is here to walk us through this bit of history, suggest answers to some of these questions, and point us in a direction to search for more.
And *we* are here, dear listener, to level with you that a lot of this stuff is miserably hard to approach, presented with the symbols and language of formal logic that is so often inscrutable to outsiders. By walking you through Wadlerâ€™s paper (and the much more approachable ), and tying it in with the cultural context of modern functional programming, we hope youâ€™ll gain an appreciation for this remarkable, divine *pun* that sits beneath all of computation.

j

Jimmy Miller

11/19/2023, 3:50 PM

I have been blasphemed! I did not need to be censored! **@Ivan Reese** is lying to you with his edits. Do not believe him. Hear with your own ears:

i

Ivan Reese

11/19/2023, 3:57 PM

Look at how he manipulates us all! Do not be fooled into action by his duplicitous, underhanded provocations. See clearly that he has played me like a puppet, and performs for you even now. Pull the wool from your eyes, he is more than the creator of sufficiently evil compilers, he isâ€¦ a *neurolinguistic* programmer!

a

Arcade Wise

11/19/2023, 7:34 PMEntscheidungsproblem :3

c

Csongor Bartus

11/20/2023, 8:05 AMI saw this idea first in https://ncatlab.org/nlab/show/computational+trilogy from the category theory people on nCatLab.
Beside type theory & programming languages it adds the category/topos theory aspect to this general computation context.
It was crucial for me to understand the difference between classical computing, parametrized computing (effects) and quantum computing.
I hope it's helpful also to you đź™‚

f

FreeMasen

11/22/2023, 6:26 PMThe ask at the end of this episode I think Eugenia Chen might cover the category theory for a lay person?
https://en.wikipedia.org/wiki/Eugenia_Cheng

p

Personal Dynamic Media

11/26/2023, 9:47 AMI found the discussion of the history of logic fascinating, but I didn't really follow what the actual correspondences were between propositions and types, proofs and programs, and reduction and execution. Did you actually explain how these correspondences work and I missed it?

i

Ivan Reese

11/27/2023, 12:32 AM

To **@Csongor Bartus** and **@FreeMasen** â€” Thank you!
**@Personal Dynamic Media**, no, you didn't miss anything. We didn't explain it. I don't even understand it, and twice now I *almost* finished reading the paper, and watched the talk a handful of times (which certainly doesn't try to explain it).
I would at least be curious to know how *subtle* or *obscure* the explanation is. Like, would an undergraduate-level understanding of logic suffice?

j

Jimmy Miller

11/27/2023, 2:02 AM

Maybe I'm remembering the conversation rather than the edit, but I'm fairly sure we give Wadler's example correspondence between Gentzen's Natural Deduction and the Simply Typed Lambda calculus. Disjunction is the disjoint sum, conjunction is a cartesian product, and implications are functions. Of course the correspondence doesn't stop there, there are tons of logic's for which you can do similar things. Here the two little snippets from the paper. The one with red and blue is Lambda Calculus the only blue is Natural Deduction and you can see the direct correspondence

i

Ivan Reese

11/27/2023, 2:04 AM

Yeah, but how does the correspondence work? Like, what's the proof that they're equivalent? I've just been taking it as granted because I have little hope of understanding the explanation.

Ivan Reese

11/27/2023, 2:05 AM

Eg â€” "disjunction is the disjoint sum" â€” why? How? What other things might disjunction correspond to elsewhere, say in physics or geometry, and how do we prove that?

p

Personal Dynamic Media

11/27/2023, 2:10 AMj

Jimmy Miller

11/27/2023, 2:11 AM

Jimmy Miller

11/27/2023, 2:13 AM

p

Personal Dynamic Media

11/27/2023, 2:16 AMAlso, thanks for the reference to the incredible proof machine. That was a pleasant way to kill a few hours so far, and I've still got a lot of proofs left. đź™‚

j

Jimmy Miller

11/27/2023, 2:16 AM

As for the arbitrary program, you could find its correspondence by converting it to lambda calculus and then converting to a proposition. If the program is expressible in the simply typed lambda calculus, you can directly see the proposition it is a proof of.
Of course the simply typed lambda calculus isn't the most expressive, so people usually add more. For example, this was a proof I wrote forever ago in Idris whose type system is based on this stuff. https://github.com/jimmyhmiller/PlayGround/blob/master/idrisTests/src/AbstractAlgebra.idr
(You can ignore the elab stuff which is more tradition proof system stuff. The code below is really just functional programming that gives you proofs)

p

Personal Dynamic Media

11/27/2023, 2:24 AMj

Jimmy Miller

11/27/2023, 2:28 AM

What other things might disjunction correspond to elsewhere, say in physics or geometry, and how do we prove that?I don't understand the physics part. Physics just uses math. As for geometry, there are a bunch of complicated stuff like homotopy type theory that deal with that kind of thing. But as you mentioned in the episode, there are unions and intersections which are sums and products in the same way disjunction and conjunction are.

i

Ivan Reese

11/28/2023, 2:13 AM

j

Jimmy Miller

11/28/2023, 2:18 AM

i

Ivan Reese

11/28/2023, 2:19 AM

Yeah, but but but *I don't liiiike category theory. It's haaaard and the people say mean things about CoffeeScript.*

s

shalabh

12/03/2023, 2:09 AMI listened to the episode today and wanted to share my thoughts:
â€śWriting programsâ€ť is a narrow framing of whatâ€™s possible in a programmable dynamic medium, so on seeing this episode title my first thought was â€śhas this podcast now dropped into **#present-company**?â€ť However, I thoroughly enjoyed the episode, since I do enjoy correspondences in math/logic and also like listening to the decidability problem discussed from different angles. I found myself emphatically nodding and clapping along (mentally, I was on a plane at the time) with Ivanâ€™s â€ścritiqueâ€ť on the implied legitimacy in this paper.
I donâ€™t think programming is more fundamental than any other human activity, essentially we are just interacting with the universe and grappling with the outcomes. Any material we work with is just as fundamental. Why is rolling a ball down an incline less fundamental than arranging some electronic bits in a machineâ€™s memory and letting them roll?
I was left thinking this: clearly I canâ€™t create a program that does not comply with some fundamental laws of the universe. That would be firstly, really cool (like inventing a machine that doesnâ€™t follow the laws of gravity) and secondly, more powerful. Jimmy alluded to this when saying these things still have a correspondence with the theory here, just â€ścomplicated correspondenceâ€ť. Which then raises the question as to if the types/proposition theory is just *one* perspective that by co-incidence is being considered the primary perspective of the universal. It just happens to match certain kinds of programming models. Perhaps there are other perspectives, maybe even with some theory or formalism yet to be devised, in a medium yet to be invented, that will have a complicated correspondence to this type/proposition business, but a simpler correspondence to the future â€śprogramming mediumâ€ť we are seeking. What if weâ€™re on the wrong track here with (present day) types?

shalabh

12/03/2023, 8:39 AMThis episode also reminded me of this essay about two view on computation: the theory of computation (machine oriented) and the theory of programming (language/logic oriented). https://pron.github.io/posts/what-we-talk-about-when-we-talk-about-computation

shalabh

12/03/2023, 8:40 AMWe can summarize the two positions in the following way: The TOP people say, â€ścomputations are programs, and programs are mathematical objects whose structure is captured by their types; the two models of computations are equivalent when asked to represent first-order functions, but diverge when asked to represent higher-order functionsâ€ť. The TOC response is, put simply, â€śwhat the hell is a function?â€ť Just as a falling apple doesnâ€™t compute integrals â€” it just falls â€” so too Turing machines and any other machine model compute neither higher-order nor first-order functions; they compute bits. What imaginary mathematical concepts we then choose to describe those computations is a different matter altogether, one that does not affect the nature of the computation just as calculus has had no impact on the behavior of falling apples.Iâ€™m definitely in team computation.

m

Marcel Weiher

12/03/2023, 9:31 AMYeah, also very much on team computation. Or actually, team running programs on a computer.
I also find Wadlerâ€™s idea of universality+ fun to contemplate, but he actually misses a rather significant problem with that idea: it doesnâ€™t even cover computing, never mind the multiverse.
â€śReducing terms to produce an answerâ€ť describes only a small and ever-diminishing portion of what we program our computers to do. They store data, retrieve data previously stored, communicate, have effects in the world, interpret stuff that happens in the world etc.
And that is not the incidental stuff, that is the main task of programs. Algorithmic work does occur, but it is more and more incidental.
But thatâ€™s just the practical view, apparently thereâ€™s theory to back it up as well:
https://cs.brown.edu/people/pw/strong-cct.pdf
I am not sure how relevant those theoretical objections are, but the practical ones seem pretty strong to me.
(And yes, you can obviously implement many of these other concerns using term-reduction/substitution. But you can also do that using NAND gatesâ€¦)

2 Views