- Dissect a programming language into its components (composition as substitution)
- Give the definition of category
- Define new programming languages by defining new categories
At the end of the day, what is a programming language? Category theory gives one possible structured, formal, precise answer to this question.
For the rest of this lecture (and the next ones) we will take a restricted version of Rust: no infinite loops, no printing, no writing to files, no outside communication.
Intuition, a category is a programming language with a set of types and a set of programs between each type.
This induces a graph built in the following way:
- Objects: the types of the programming language.
- Edges: an edge for each program that goes from one type to the other.
Why ask for composition? Composition corresponds to syntactic substitution of programs: this is achieved by replacing the input variable of the second program with the entire body of the first program:
fn program1(a: A) -> B {
... a ...
}
fn program2(b: B) -> C {
b ... b
}
fn program3(c: C) -> D {
... c ... c ...
}
// program2 is the one that does not have dots at beginning at end of programs. Keep this in mind to be able to distinguish it in later examples.What does it mean to compose programs? There are two possible ways in which one can answer this question.
-
The first is the syntactic one: composing programs means substituting the code of one into the code of the other, i.e., I take the first program and replace the input variable of the second program with the code of the first whenever the input variable appears. This is syntactic substitution. Syntactic composition is associative: this is why we will require an associativity law when combining programs together.
/////////////////// // POSSIBILITY 1 // First, take the code of program3, then replace each input variable with program2, then replace each input variable with program1: // step 1. fn program3(c: C) -> D { ... c ... c ... } // step 2. fn program2_then_3(b: B) -> D { ... program2(b) ... program2(b) ... } // ...equivalent to, by unfolding... fn program2_then_3(b: B) -> D { ... (b ... b) ... (b ... b) ... } // step 3. fn program1_then_2_then_3(a: A) -> D { ... (program1(a) ... program1(a)) ... (program1(a) ... program1(a)) ... } // ...equivalent to, by unfolding... fn program1_then_2_then_3(a: A) -> D { ... ((... a ...) ... (... a ...)) ... ((... a ...) ... (... a ...)) ... } /////////////////// // POSSIBILITY 2 // First, take the code of program2, then replace each input variable with program 1. After having done this, replace the program obtained like this into the input variable of program3. // step 1. fn program2(b: B) -> C { b ... b } // step 2. fn program1_then_2(a: A) -> C { program1(a) ... program1(a) } // ...equivalent to, by unfolding... fn program1_then_2(a: A) -> C { (... a ...) ... (... a ...) } // step 3. take this program, substitute it fn program(1_then_2)_then_3(a: A) -> D { ... program1_then_2(a) ... program1_then_2(a) ... } fn program(1_then_2)_then_3(a: A) -> D { ... (program1_then_2(a)) ... (program1_then_2(a)) ... } // ...equivalent to, by unfolding... fn program(1_then_2)_then_3(a: A) -> D { ... ((... a ...) ... (... a ...)) ... ((... a ...) ... (... a ...)) ... } /////////////////// // The result you obtain is the same! Because substitution for the source code of programs is associative.
This behaviour is exactly what the composition map for categories abstracts.
-
The other intuition for composition is the semantic composition: this is the kind of composition that happens at runtime, i.e., feed the data produced by the execution of the first into the second. This is typically much simpler to achieve/justify: you just call the first function and feed its input into the second. This is also associative.
///////////////////////////////////// // Composite program, semantically: fn composition123(a: A) -> D { program3(program2(program1(a))) } /////////////////// // POSSIBILITY 1 fn composition23(b: B) -> D { program3(program2(b)) } fn composition1_then_23(a: A) -> D { composition23(program1(a)) } // ...equivalent to, by unfolding... fn composition1_then_23(a: A) -> D { program3(program2(program1(a))) } /////////////////// // POSSIBILITY 2 fn composition12(a: A) -> C { program2(program1(a)) } fn composition12_then_3(a: A) -> D { program3(composition12(a)) } // ...equivalent to, by unfolding... fn composition12_then_3(a: A) -> D { program3(program2(program1(a))) } // In both cases I get the same result!
This kind of substitution/composition behaviour is typical of programs. A good mathematical model for programming languages ought to satisfy exactly this subtitution behaviour.
// The function which simply returns whatever input you have to it.
// Note that the type of the argument matches exactly the type of the output.
fn identity(a: i32) -> i32 {
a
}Categories are a way to symbolically capture the situations above. We will have a symbol (e.g., a value in a Rust enum) for each type, and for each two symbols for types we will have a collection (again, some Rust enum) of symbols for programs.
A category is defined by the following choices:
- (Objects.) A choice of a Rust type, which we call
Obj. Each valuea:Objin this type is going to be called "an object of the category".
Intuition: every value/symbol of this type is going to represent a type of our programming language. - (Arrows.) For every possible value
a: Objandb: Obj, a choice of another Rust type, which we callArr[a,b]. Each valuef:Arr[a,b]in one of these types is going to be called "an arrow of the category, going fromatob".
Intuition: every value/symbol of this type is going to represent *an expression of our programming language which takes something of typeaas input and gives me something of typebas output. - (Identities.) For every possible value
a: Obj, a choice of a valueid[a]: Arr[a,a]in the typeArr[a,a]. Intuition: there always exists a symbol for the program which takes an input of typeaand immediate returns that something of typea. - (Composition.) For every possible value
a: Obj,b: Obj,c: Obj, a choice of a Rust function with the following signature:Intuition: for every two programs such that the output type of the first coincides with the output type of the second, there is always a "composite program" which combines the two processes together into a single process that, intuitively, does one after the other.fn compose[a][b][c](f: Arr[a,b], g: Arr[b,c]) -> Arr[a,c] { ... }
This concludes the part for choices/data. Now we ask that the choices above are in some sense well-behaved: the following three conditions are called the category laws:
- (Left unitality.) Given a value
f: Arr[a,b]for some valuesa:Obj,b:Obj, the following thing must happen: if you call the functioncompose[a][a][b](id[a], f)onid[a]as the first argument it must happen that this function returns exactlyf. In other words,compose[a][a][b](id[a], f) = f
- (Right unitality.) Given a value
f: Arr[a,b]for some valuesa:Obj,b:Obj, the following thing must happen: if you call the functioncompose[a][b][b](f, id[b])onid[b]as the second argument it must happen that this function returns exactlyf. In other words,compose[a][b][b](f, id[b]) = f
- (Associativity.) For every value
a,b,c,d: Obj, and every valuef:Arr[a,b], g:Arr[b,c], h:Arr[c,d], the following function calls must give you the same result:compose[a][b][d](f, compose[b][c][d](g, h)) = compose[a][c][d](compose[a][b][c](f, g), h)
The key intuition is that in the first part of the equation I have to do an intermediate step: I have to construct an intermediate program in which I substitute the code of the first program (f) into the code of the second program (g). The line at the top proceeds in the usual way.
-- End of the definition of Category. --
In the Rust notation, note that one can often remove the square brackets, because it's unambiguous what kind of element of Obj must be placed there for the entire expression to make sense: for example, if I know that f:Arr[a,b] and g: Arr[b,c] the indices of compose(f, g) must be [a][b][c].
| Math notation | Rust notation |
|---|---|
id[a] |
|
f: Arr[a,b] |
|
compose(f, g) |
|
| (Identity laws) | |
| (Associativity) |
The associativity law is extremely important! It means that any way I put the brackets it does matter, so one can simply write
You will often hear other books use the work "morphism" instead of arrow, and "hom-set" intead of "type of arrows" (for some objects
In order to define a new category, I must make all the choices above; after that, I have to make sure that my choices satisfy the category laws.
For the type of objects Obj, I choose the following type:
enum Obj {
Int,
Bool
}I make the following choices for arrows:
enum Arr_Int_Int {
IntIdentity,
}
enum Arr_Int_Bool {
IsEven,
IsEvenNot,
}
enum Arr_Bool_Int {
}
enum Arr_Bool_Bool {
BoolIdentity,
Not
}All possible choices that I have to make for compose:
fn compose_Int_Int_Int(f: Arr_Int_Int, g: Arr_Int_Int): Arr_Int_Int { ... }
fn compose_Int_Int_Bool(f: Arr_Int_Int, g: Arr_Int_Bool): Arr_Int_Bool { ... }
fn compose_Int_Bool_Int(f: Arr_Int_Bool, g: Arr_Bool_Int): Arr_Int_Int { ... }
fn compose_Int_Bool_Bool(f: Arr_Int_Bool, g: Arr_Bool_Bool): Arr_Int_Bool { ... }
fn compose_Bool_Int_Int(f: Arr_Bool_Int, g: Arr_Int_Int): Arr_Bool_Int { ... }
fn compose_Bool_Int_Bool(f: Arr_Bool_Int, g: Arr_Int_Bool): Arr_Bool_Bool { ... }
fn compose_Bool_Bool_Int(f: Arr_Bool_Bool, g: Arr_Bool_Int): Arr_Bool_Int { ... }
fn compose_Bool_Bool_Bool(f: Arr_Bool_Bool, g: Arr_Bool_Bool): Arr_Bool_Bool { ... }Here are some cases:
fn compose_Int_Int_Int(f: Arr_Int_Int, g: Arr_Int_Int): Arr_Int_Int {
match f {
IntIdentity =>
match g {
IntIdentity => IntIdentity
}
}
}
fn compose_Bool_Bool_Bool(f: Arr_Bool_Bool, g: Arr_Bool_Bool): Arr_Bool_Bool {
match f {
BoolIdentity => g,
Not =>
match g {
Not => BoolIdentity,
BoolIdentity => Not,
}
}
}
fn compose_Int_Bool_Bool(f: Arr_Int_Bool, g: Arr_Bool_Bool): Arr_Int_Bool {
match f {
IsEven =>
match g {
BoolIdentity => IsEven,
Not => IsEvenNot,
},
IsEvenNot =>
match g {
BoolIdentity => IsEvenNot
Not => IsEven,
}
}
}
// There is nothing I have to specify since Arr_Bool_Int is the empty type!
// Other empty cases follow.
fn compose_Int_Bool_Int(f: Arr_Int_Bool, g: Arr_Bool_Int): Arr_Int_Int {
match f {
IsEven =>
match g {
}
IsEvenNot =>
match g {
}
}
}
fn compose_Int_Bool_Int(f: Arr_Int_Bool, g: Arr_Bool_Int): Arr_Int_Int {
IntIdentity
}
fn compose_Bool_Int_Int(f: Arr_Bool_Int, g: Arr_Int_Int): Arr_Bool_Int {
match f {
}
}
fn compose_Int_Bool_Int(f: Arr_Int_Bool, g: Arr_Bool_Int): Arr_Int_Int {
match g {
}
}
// Which one of these two definitions works?
fn compose_Bool_Int_Bool(f: Arr_Bool_Int, g: Arr_Int_Bool): Arr_Bool_Bool {
Not
}
fn compose_Bool_Int_Bool(f: Arr_Bool_Int, g: Arr_Int_Bool): Arr_Bool_Bool {
BoolIdentity
}
fn compose_Bool_Int_Bool(f: Arr_Bool_Int, g: Arr_Int_Bool): Arr_Bool_Bool {
match f { }
}
// Answer in https://rot13.com/: obgu pubvprf jbex orpnhfr jr zhfg purpx havgnyvgl/nffbpvngvivgl sbe rirel inyhr bs Nee_Obby_Vag, bs juvpu gurer ner abar! Fb gurer vf abguvat gb purpx.In general, for the choices above (not for this last example), we now have to show that these choices satisfy the category laws!
- I must check that whenever f is
BoolIdentitythe functioncomposereturns g. - I must check that whenever f is
IntIdentitythe functioncomposereturns g. - I must check that whenever g is
BoolIdentitythe functioncomposereturns f. - I must check that whenever g is
IntIdentitythe functioncomposereturns f. - Associativity.
// Intuition for the type Pair<Int,Bool>
// struct IntAndBool {
// a: Int,
// b: Bool,
// }
// Intuition for the type Either<Int,Bool>
// enum EitherIntBool {
// Int(i32),
// Bool(bool),
// }
// Intuition for Either<A,B>
// enum Either<A,B> {
// left: A
// right: B
// }
// Intuition for Pair<A,B>
// struct Pair<A,B> {
// left: A
// right: B
// }
// Recursive algebraic data type
enum Obj {
Int,
Bool,
Pair(Obj,Obj),
Either(Obj,Obj),
}
// What are some examples of objects?
// - Int
// - Bool
// - Pair(Int, Int)
// - Pair(Int, Pair(Int, Int))
// - Pair(Int, Bool)
// - Either(Bool, Bool)
// We now define some examples of morphisms
enum Arr_Int_Bool {
IsEven,
IsEvenNot,
}
enum Arr_PairIntInt_Int {
First,
Second,
...
}
enum Arr_Int_PairIntInt {
Duplicate,
...
}
/*
// Intuition for duplicate
fn duplicate(n: i32) -> Pair<Int,Int> {
Pair { left: n, right: n }
}
*/enum Obj {
One
}
// Type synonym. Whenever you see Arr_One_One you can simply replace it with the type on the right.
// (In Rust this is typically used to make things more readable.)
type Arr_One_One = i32We have to pick a value id[One] : Arr_One_One.
At this point we have two possible choices:
-
Pick the value
0: i32. -
For the composition function, we pick this function:
fn compose_One_One_One(f: Arr_One_One, g: Arr_One_One) -> Arr_One_One { f + g }
-
We have to check unitality: this boils down to the fact that for any value
g: Arr_One_Onethe equationscompose_One_One_One(0, f) = f // Given f: i32, 0 + f = f compose_One_One_One(f, 0) = f // Given f: i32, f + 0 = f
are satisfied. This is clearly true because of a general property of 0 and + for i32!
-
We have to check associativity: for every value
f,g,h:Arr_One_Onecompose_One_One_One(f, compose_One_One_One(g, h)) compose_One_One_One(compose_One_One_One(f, g), h)
this holds because of a general property of numbers: given
f,g,h:i32, addition is associative:$f+(g+h) = (f+g)+h$ .(This is the only index we have to check! We use it 4 times from the definition of associativity)
- Pick the value
1: i32. - For the composition function, we pick this function:
fn compose_One_One_One(f: Arr_One_One, g: Arr_One_One) -> Arr_One_One { f * g }
- Similar properties as above:
$1 * f = f = f * 1$ and$(f * g) * h = f * (g * h)$ .
The above situation can be abstracted with the following definition:
- (Objects.) A choice of a Rust type
M. - (Identity.) A choice of a specific value
id:Min the typeM. - (Operation.) A choice of a Rust function with the following signature:
fn op(a: M, b: M) -> M { ... }
Subject to the following laws:
- (Left unitality.) For every value
a:M, the following equation must hold:op(id, a) = a
- (Right unitality.) For every value
a:M, the following equation must hold:op(a, id) = a
- (Associativity.) For every value
a,b,c:M, the following equation must hold:op(a, op(b, c)) = op(op(a, b), c)
enum Obj {
One // keep in mind that I can simply pick anything here
}
type Arr_One_One = str
// As identity, we pick the empty string.
let id = "";
fn compose_One_One_One(f: Arr_One_One, g: Arr_One_One) -> Arr_One_One {
f + g // string concatenation
}This works because concatenation of strings is associative, and because concatenating with the empty string just gives you the other string. More in general, one can think of strings as lists of characters.
Assume we pick some type A, for instance i32. This will give us the type of lists List<i32>.
enum Obj {
One // keep in mind that I can simply pick anything here
}
enum List<A> {
Empty,
Element { value: A, tail: List<A> }
}
type Arr_One_One = List<A>
// As identity, we pick the empty list.
let id = [];
// Solution for the exercise in Lecture 1
fn append<A>(a: List<A>, b: List<A>) -> List<A> {
match a {
Empty => b,
Element { value: v, tail: t } =>
Element { value: v, tail: append(t, b) }
}
}
fn compose_One_One_One(f: Arr_One_One, g: Arr_One_One) -> Arr_One_One {
append(f, g) // concatenation of lists
}Important takeaway: objects are not always """types in a programming language""" and arrows are not always """programs in a programming language""": they can be thought of such, but that need not be the case.
- In one of the examples for monoids, we saw that a program is a number!! Very strange. A number surely does not represent a process, nor a function, nor a transformation.