Philip Wadler on why category theory is relevant for developers, discussing the principle of Propositions as Types connecting propositions and proofs in logic, and types and programs in computing.
Philip Wadler is Professor at the University of Edinburgh. He contributed to the design of Haskell, Java, and XQuery.
Joy of Coding is a one-day conference that celebrates the art, craft, science but foremost the joy of software development. It is a day for talking and collaborating with like-minded coders. The non-profit conference is not targeted towards a particular language or platform.
- There are deep connections between logic, lambda calculus, and category theory.
- In category theory we've got objects and arrows. An object in category theory is a type. Arrows are functions that have an argument of a given type and return a result of a given type.
- The three most important structures in programming (records, variant records, and functions) arise in category theory (product, sum, exponential) and their correspondence with the three most important construct in logic (and, or, implication).
- In category theory a function, that is an arrow, can also be an object. This corresponds to the most profound idea in programming: that programs are also data.
- All of this was built to explain deep connections between lambda calculus and ideas from logic. You should prefer using a programming language based on lambda calculus.
- 1:54 Formal logic and lambda calculus were both formalized in the 1930s, and after 50 years, in 1980, William A. Howard published a paper saying they are exactly the same thing.
- 2:26 The fact that Gerhart Gentzen and Alonzo Church both came up with the same idea but it took about 40 years before people recognize that they are the same idea, then it took another 10 years for Howard to get around to publishing it, is what makes us say that they had not invented something, but they had discovered something.
- 3:34 There are deep connections between logic, lambda calculus, and category theory, which is the focus on this presentation.
- 4:55 In category theory we've got objects and arrows. An object in category theory is a type. Arrows are functions that have an argument of a given type and return a result of a given type.
- 5:32 There are many instances of this kind of renaming: in set theory, objects are sets and arrows can be functions between the sets or relations between the sets; in domain theory, objects are domains and arrows are again functions between the domains; in abstract algebra, objects are groups and arrows are morphisms between groups.
- 6:50 Two simple notions that will be used in the remainder of the talk are those of identity function and function composition. The identity function is a function that simply returns its argument. Function composition allows to take a function
Band another function
Cand create a third function
f;g(also denoted by
- 8:10 Function composition is governed by some laws. The first law says the identity function,
id, followed by
fis the same as
- 9:00 Another law states that if you compose three functions, it doesn't matter what order you compose them, i.e., composition is associative.
- 9:26 This talk will show how the three most important structures in programming (records, variant records, and functions) arise in category theory (product, sum, exponential) and their correspondence with the three most important construct in logic (and, or, implication).
- 9:50 Given an object
Aand an object
B, we form the product
A x B(A times B). In set theory, this would be Cartesian product; in programming, tuple record with two fields, the first of type
Aand the second of type
- 10:45 Let's call
fsta function which given an
A x Bpair returns the
snda function which given an
A x Bpair returns the
- 12:00 If
fis a function from
gis a function from
B, I can build a pair from that - let's call this function
is how you build a pair.
sndare how you take it apart.
- 12:46 The diagram shown above, called a commutative diagram, tells us that if you build a pair using
and you extract its
fstcomponent, that is the same as using
falone. Similarly, using
sndto get the second component of the pair, is the same as using
galone. This is expressed in the following isomorphism:
- 13:25 The above property only holds if
ghave no side effects. This is an argument against having side effect, as it gives you useful and simple laws.
- 14:12 The dotted line in the diagram as a special meaning, i.e., if a function makes this diagram commute, it is unique.
- 14:30 A commuting diagram means that if there are two different pathways from one place to another that involve applying different functions, they must be equivalent.
- 15:30 In short, what the diagram tells us is: you can take pairs apart using
snd; you can build pairs using
; those operations are inverse to each other and
is the unique thing that makes this work.
- 15:51 Being unique important yet there are all sorts of things that you can work out from that are really useful like you can prove things (example follows)
- 21:40 The product corresponds to the
- 23:00 Another major data structure is the sum, which is sometimes called a disjoint union, or record variants in Pascal, either in Haskell, etc.
- 24:00 To build a disjoint union, given an
Awe can inject it into the type
A+B. This could be represented in a particular case as something with a numeric tag field followed by a value, which could be of a different type depending on the tag.
- 24:49 We can build one of these sum values using two functions:
inr(in-right). We can take it apart doing case analysis. If
fis a function from
gis a function from
C, we can get a
[f,g], which looks at the concrete type in the sum and, if it is an
fto it; if it's a
B, it applies
- 25:18 The commutative diagram for a sum tells us that if you have
[f,g], that is the same as
f; if you have
[f,g]that is the same as
g. Again the dotted line means that
[f,g]is universal, meaning that if you have some
hthat makes this diagram commute you know that that's the same as
- 27:50 Using the commuting diagram for
A+B, it is possible to prove the following isomorphism:
which means that having an arrow from an
Cand precomposing it using either
inris the same as having an arrow from an
Cand having an arrow from
- 31:00 We can define an additional contract for the sum, called distributivity:
- 31:35 Sum types correspond to disjunction in logic, that is the
- 32:35 The exponential leads us to currying, i.e., to the concept of higher-order functions. In this case the commutative diagram shows the following isomorphism:
- 34:40 The commutative diagram for exponential, show how you can go from a product of two objects to a product that includes as its first term a function
What this means is that in category theory a function, that is an arrow, can also be an object. This corresponds to the most profound idea in programming: that programs are also data. Not every data is a program, but every program can be converted into data.
- 37:30 Exponential corresponds to implication in logic.
- 37:40 Product, sum, and exponential represent the three most important concepts in programming: the record, the variant record, and the function.
- 38:00 The commutative diagrams for products and sums have an interesting relation: they are just the same diagram with reversed arrows. They are dual.
- 41:24 All of this was built to explain the semantics of lambda calculus and to explain deep connections between programming languages based on lambda calculus and logical ideas for natural deduction.
- Howard, William A. (September 1980) [original paper manuscript from 1969], "The formulae-as-types notion of construction", in Seldin, Jonathan P.; Hindley, J. Roger, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Boston, MA: Academic Press, pp. 479-490, ISBN 978-0-12-349050-6.
Languages, tools and projects
See more presentations with show notes
I agree - it was cool