Channels

#share-your-work

Title

# share-your-work

i

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.

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

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.*