Philip Wadler
Propositions as Types

Discussion: Issue #213

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.

Discussion

Since types and classes are strongly related, a large part of our discussion revolved around trying to come up with a good distinction between functional programming and object oriented programming. Since most patterns can be converted from one to the other, the only handle we could find was mutable state, but even that may be viewed more like a cultural thing rather than an intrinsic necessity of OOP. We also discussed an important practical aspect of a type system’s expressiveness: the more expressive the type system, the more specific you can be with your expected inputs and the outputs, thus, the fewer tests you have to write.

Join us any time and get to be a better coder!