Ephox engineer Dylan Just continues his “Talks We Love” series on the blog discussing influential lectures in the world of Functional Programming. In this post, he explores the relationship between Logic and Type Theory.
There is a direct correspondence between Logic and Type Theory. A proposition in a logic directly corresponds to a type in a type system. As such, the techniques of logical reasoning can be applied to types in programming languages. Defining an instance of a type in a programming language constitutes a proof of the corresponding logical proposition. This is sometimes called the “Curry-Howard-Lambek Correspondence” (or a few variants), after the people who discovered it.
This property is very important for software quality, by providing a means to statically prove properties about programs. It is particularly useful for formally-verified systems, but any developer using a static type system can take advantage of it. In fact, if you are using a static type system, you are making use of this property possibly without even knowing it.
In this post, I highlight some videos and resources to help you learn more about this important concept.
Phillip Wadler, “Propositions as Types”
Phillip Wadler’s talk does a great job of explaining the correspondence between logic and types. He starts by introducing three formulations of computability—Lambda Calculus (by Alonzo Church), Recursive Functions (by Kurt Gödel)and Turing Machines (by Alan Turing). He shows the history of their development and how they were shown to be equivalent.
After this, he introduces Natural Deduction, the primary system of logic in use today. He shows how this relates to the Simply Typed Lambda Calculus. Through this he shows three important facets of the correspondence between logic and types:
- propositions correspond to types
- proofs correspond to terms
- simplification of proofs corresponds to evaluation of programs
These are very powerful ideas. He goes on to show how several other logics correspond to type systems.
A key theme of this talk is an appeal to the view that mathematics is discovered, not invented. He cites, as evidence of this, the fact that the above concepts were all discovered independently multiple times. Whatever your view on this debate, he makes an interesting point.[youtube https://www.youtube.com/watch?v=IOiZatlZtGU]
Wadler has also published a paper on Propositions as Types.
Chris Taylor, The Algebra of Algebraic Data Types
The correspondence between Logic and Type Theory can be taken further, to Category Theory.
At its simplest level, there is an “algebraic” interpretation, wherein a type is described by the number of values it has. For example, Void is 0, Unit is 1, Boolean is 2, a 32-bit integer is 2^32. Then, types like Either, Pair and functions behave as operators on these numbers, and our normal rules of algebra actually work on the resulting expressions.
The best explanation of this I’ve found is Chris Taylor’s talk “The Algebra of Algebraic Data Types”. If you prefer reading, the accompanying blog post presents the same content.[youtube https://www.youtube.com/watch?v=RFRpRiMX-GM]
(The above video is an edit removing noise in the audio. The original video is here.)
Bartosz Milewski, The Truth about Types
This talk by Bartosz Milewski follows on well from the previous two. He goes right into the details, showing the 3-way relationship between Logic, Types and Category Theory.
Interestingly, Milewski offers a counterpoint to Wadler’s argument about mathematics being discovered. He argues that mathematics facilitates human thinking, and that we are actually really discovering things about the human mind.[youtube https://www.youtube.com/watch?v=dgrucfgv2Tw]
In my last post, I mentioned Milewski’s lecture series on Category Theory. The below lecture from this series specifically deals with propositions as types. I’d recommend watching the whole series, though, to see this explanation in context.[youtube https://www.youtube.com/watch?v=iXZR1v3YN-8]
I think it’s important for all programmers to look under the covers to come to a deeper understanding of the craft. To look not only about what our programs do, but what they mean.
The resources above show that our programs mean something more than their runtime semantics. If we’re using a static type system, then our types have an interpretation in logic. We are stating propositions and proving them. By being cognizant of this fact, we can use it to our advantage.
We can make use of the logical interpretation to prove properties of our programs and see which properties are left for our tests to cover. Furthermore, we can apply logical operations to transform our types into different encodings, which may have different implications for efficiency or elegance of code.
When I first came across the concept of propositions as types, it blew my mind and gave me a whole new perspective on my programs. I hope that you find the above resources as informative and enjoyable as I have.