|
|
@@ -0,0 +1,1517 @@ |
|
|
CATEGORY THEORY FOR PROGRAMMERS |
|
|
|
|
|
Category Theory 1.1: Motivation and Philosophy |
|
|
https://www.youtube.com/watch?v=I8LbkfSSR58&index=1&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_ |
|
|
|
|
|
Composability, Abstraction, Reusability |
|
|
|
|
|
Category Theory is a higher-level language. |
|
|
Not a practical, executable language. |
|
|
|
|
|
CT unifies over Mathematics |
|
|
Curry-Howard-Lambek correspondence |
|
|
* Logic <-> TypeTheory <-> CT |
|
|
https://wiki.haskell.org/Curry-Howard-Lambek_correspondence |
|
|
The Curry-Howard-Lambek correspondence is a three way isomorphism between types (in programming languages), propositions (in logic) and objects of a Cartesian closed category. Interestingly, the isomorphism maps programs (functions in Haskell) to (constructive) proofs in logic (and vice versa). |
|
|
|
|
|
|
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
|
Category Theory 1.2: What is a category? |
|
|
https://www.youtube.com/watch?v=p54Hd7AmVFU&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&index=2 |
|
|
|
|
|
Abstraction: Get rid of the details; things that are different at lower level |
|
|
may be identical at higher levels of abstraction |
|
|
Composition: Combine small parts to build larger structures |
|
|
Identity: |
|
|
|
|
|
(Homotopy type Theory: What things are identical? What are isomorphic?) |
|
|
|
|
|
CT encompasses Composition and Identity |
|
|
|
|
|
Definition: Category |
|
|
A bunch of objects and morphisms (arrow) |
|
|
|
|
|
Definition: Object |
|
|
A primitive of CT. It has no properties! |
|
|
"Names for the ends of arrows" |
|
|
|
|
|
Definition: Morphism (a.k.a. Arrow) |
|
|
Goes from one object to another |
|
|
|
|
|
Definition: Composition |
|
|
If there is an arrow A -> B and an arrow B -> C then there is an arrow A -> C |
|
|
A -> C is the `composition` of A -> B and B -> C |
|
|
Composition is *associative*: h . (g . f) = (h . g) . f |
|
|
|
|
|
Definition: Identity |
|
|
For every object, there is an Identity arrow A -> A |
|
|
If f is an arrow A -> B and id_B is the Identity arrow of B, then |
|
|
id_B . f = f Left Identity |
|
|
likewise g . id_A = g Right Identity |
|
|
|
|
|
In Programming: |
|
|
Objects are Types |
|
|
Morphisms are Functions |
|
|
|
|
|
What are Types? Sets of values |
|
|
What are Functions? Functions on Sets of values |
|
|
|
|
|
|
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
|
Category Theory 2.1: Functions, epimorphisms |
|
|
https://www.youtube.com/watch?v=O2lZkr-aAqk&index=3&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_ |
|
|
|
|
|
Semantics: |
|
|
Operational = How expressions/statements can be transformed |
|
|
Denominational = Map expressions into another domain, e.g. mathematics |
|
|
|
|
|
Partial functions = functions that are not defined for all arguments of its type |
|
|
Total functions = are defined for all arguments of its type |
|
|
In programming, a function is "pure" if you can memoize it. |
|
|
|
|
|
How can we use functions in our category "set" which contains (sets, function) |
|
|
* Functions have direction -- unlike a Relation |
|
|
* Function may be many-to-one or one-to-one, but never one-to-many. |
|
|
* domain: Set of inputs |
|
|
* codomain: Set of all possible outputs |
|
|
* image: Set of actual outputs (may be a subset of the codomain) |
|
|
|
|
|
Is the function invertible? Usually it is *not*. |
|
|
a function f :: a -> b *does not imply* there is a function g :: b -> a |
|
|
|
|
|
if g . f = id then f and g are invertible; this implies f . g = id |
|
|
|
|
|
An invertible function is called an isomorphism. This is the definition in any category. |
|
|
Notice that the definition is in CT terms, i.e. composition and identity. |
|
|
|
|
|
Why are most functions not isomorphic? |
|
|
* A function may collapse elements of the codomain (e.g. isEven maps numbers to T|F) : ABSTRACTION |
|
|
* A function's image is a strict subset of the codomain. : MODELING |
|
|
|
|
|
A function that is not invertible increases entropy. |
|
|
|
|
|
injective function: every x maps to a unique y |
|
|
surjective function: every y is mapped to by an x. forall y . exists x s.t. y = f x |
|
|
|
|
|
An isomorphism is both injective and surjective. That is the set/Latin. |
|
|
|
|
|
In CT: |
|
|
|
|
|
monomorphism = injective |
|
|
epimorphism = surjective |
|
|
|
|
|
Epimorphism (CT definition) |
|
|
* f is an epimorphism from a -> b if for every other object C in the whole category, |
|
|
and every pair of morphisms b -> c (e.g. g1 and g2) if g1 . f == g2 . f => g1 == g2 |
|
|
This definition works for any category. In Set context, it is a surjection. |
|
|
Proven with "post-composition" (add category C after) |
|
|
|
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
|
Category Theory 2.2: Monomorphisms, simple types |
|
|
https://www.youtube.com/watch?v=NcT7CGPICzo&index=4&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_ |
|
|
|
|
|
Monomorphism |
|
|
|
|
|
Start with something *not* a monomorphism. |
|
|
e.g. a non-injective function that maps two different xs into the same y. |
|
|
|
|
|
forall c . forall g1,g2 :: c -> a if f . g1 == f . g2 => g1 == g2 |
|
|
|
|
|
Epimorphism and monmomorphism is defined for every category |
|
|
|
|
|
---- |
|
|
|
|
|
Simple sets |
|
|
|
|
|
In Haskell: |
|
|
* Empty Set corresponds to Void type |
|
|
* Singleton Set is () (Unit type) |
|
|
|
|
|
|
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
|
Category Theory 3.1: Examples of categories, orders, monoids |
|
|
https://www.youtube.com/watch?v=aZjhqkD6k6w&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&index=5 |
|
|
|
|
|
Simplest possible category: zero objects, zero morphisms |
|
|
Then: 1 object, Id Arrow |
|
|
|
|
|
In general, we can start with a graph. (n.b.: Not every graph is a category!) |
|
|
You can add arrows to any graph until it *is* a category. |
|
|
1. Identity: For every node, add Id Arrow |
|
|
2. Composition: For every pair of arrows a -> b, b -> c, add arrow a -> c |
|
|
3. Associativity also must be satisfied |
|
|
|
|
|
Free Construction of a category (from a graph). Unconstrained except by properties above. |
|
|
|
|
|
Orders: |
|
|
A category where arrows are *not* functions |
|
|
An arrow represents a relation, viz. <= |
|
|
in this context a -> b means a <= b |
|
|
|
|
|
Preorder: |
|
|
A relation that satisfies the minimum of conditions |
|
|
* Composable. If a < b && b < c then a < c |
|
|
* Associative. |
|
|
* Identity. a <= a duh. Reflexivity. |
|
|
* There may or may not be an arrow betwee two objects. |
|
|
* May not have multiple arrows from one object to another. (In Total Order there is an arrow between any two arrows.) |
|
|
* Thin Category corresponds to a Preorder, and Preorder corresponds to a This category. |
|
|
|
|
|
Note that a Thin Category is both an epimorphism and a monomorphism. But it is not invertible. |
|
|
|
|
|
Most general category: A Preorder that is *thick*. Multiple arrows a -> b. |
|
|
Each arrow represents a different proof of the relation. |
|
|
A "proof-relevant relation" |
|
|
|
|
|
|
|
|
Hom-set: |
|
|
A set of arrows C(a, b) (or C(a, a)) |
|
|
If C is a category containing objects A and B then Hom(A,B) is the collection of all morphisms from A to B: |
|
|
Hom(A,B) = {f∈C | f: A -> B } |
|
|
where: A = Dom(f) and B = Cod(f) |
|
|
|
|
|
Partial Order: |
|
|
No loops! |
|
|
If there is an arrow a -> b, then there is not an arrow b -> a |
|
|
Corresponds to a directed acyclic graph. |
|
|
Some objects are not comparable |
|
|
|
|
|
Partial Order is also not invertible -- by defintion, you cannot have both a -> b and b -> a |
|
|
|
|
|
|
|
|
Total Order: |
|
|
There is an arrow between any two objects |
|
|
|
|
|
Back to single-object category. |
|
|
The single object may have several arrows. |
|
|
Composable: Obviously. Trivially. |
|
|
|
|
|
That is a Monoid! A single object and however many arrows you want. |
|
|
|
|
|
Monoid is known from Algebra & Set theory: |
|
|
A set of elements and a (total) binary operator. |
|
|
* One element in the set is "unit" (a.k.a. identity element, or "empty") |
|
|
exists e . forall a : e `op` a == a `op` e == a |
|
|
* Associativity. |
|
|
* (a `op` b) `op` c == a `op` (b `op` c) |
|
|
|
|
|
Examples: Natural numbers with (+, 0) |
|
|
Natural numbers with (*, 1) |
|
|
Strings with (concat, "") (n.b. this is not symmetric!) |
|
|
Lists with (concat, []) (n.b. this is not symmetric!) |
|
|
|
|
|
Hom-set of Monoid is M(m, m), i.e. set of arrows m -> m |
|
|
|
|
|
Monoid can be seen as the basis of multiplication -- M(m, m) implies other |
|
|
arrows may be produced as the product/composition of m -> m |
|
|
|
|
|
In a monoid, any two functions are composable! |
|
|
Corresponds to "weakly typed" language, i.e. there is only one type |
|
|
|
|
|
|
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
|
Category Theory 3.2: Kleisli category |
|
|
https://www.youtube.com/watch?v=i9CU4CuHADQ&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&index=6&spfreload=1 |
|
|
|
|
|
Consider subset relation. Is this Order? Preorder? |
|
|
* Identity: Every set is a subset of itself (reflexivity) |
|
|
* Composability: if a `subset` b and b `subset` c then a `subset` c |
|
|
|
|
|
OK, so it is at least a Preorder. |
|
|
|
|
|
* There are no loops -- if a `subset` b and b `subset` a then a == b |
|
|
So it is a Partial Order. |
|
|
|
|
|
Not a Total Order: There may be disjoint subsets, e.g. |
|
|
|
|
|
Kleisli Category |
|
|
Suppose we have a lib of functions. |
|
|
Business comes up with a new requirement: Every function must have an audit trail. |
|
|
Task: Go and rewrite the lib to satisfy this requirement. |
|
|
|
|
|
Naive solution: Global String log |
|
|
|
|
|
Later ... |
|
|
Business requires this to work in a multithreaded environment. ummm .... |
|
|
|
|
|
Now what? |
|
|
|
|
|
Starts by redifining simple functions to return pair of ('a returnValue * string logText) |
|
|
Build a compose function: |
|
|
|
|
|
compose (a -> b) -> (b -> c) -> (a -> c) // this looks familiar. |
|
|
|
|
|
Have to extend that for pairs: |
|
|
|
|
|
compose (a -> (b, p1)) -> (b -> (c, p2)) -> (a -> (c, p1 + p2)) |
|
|
|
|
|
Hmmm. Is there a category here? |
|
|
* Composition: Check. That is the point |
|
|
* Associativity: Yes, regular function composition and string concatenation are both associative. |
|
|
* Identity: (a, "") -> (a, "") |
|
|
|
|
|
Hey! That's a monoid! |
|
|
This is a category with types as objects and functions a -> (b, String) as morphisms. |
|
|
|
|
|
This is the Kleisli category. a -> (b, x) is a Kleisli arrow. |
|
|
|
|
|
These arrows are composable because this embellishment is a monad. watch out. |
|
|
Don't fear the Monads. Just a special way of composing functions. |
|
|
|
|
|
|
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
|
Category Theory 4.1: Terminal and initial objects |
|
|
https://www.youtube.com/watch?v=zer1aFgj4aU&index=7&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_ |
|
|
|
|
|
Recap Kleisli Category |
|
|
* Start with category C |
|
|
* trying to build Kleisli category K |
|
|
* For every object a in C, there is an object a in K |
|
|
* The *arrows* are not the same. For every arrow a -> m b in C, there is an arrow a -> b in K |
|
|
* Therefore, Identity in K is a -> m a in C (looks like flatMap ...) |
|
|
And that m a has to be `unit` with respect to the composition in K |
|
|
* K must also be associative |
|
|
* So K has Identity, Composability, and Associativity. |
|
|
* uh-oh, that's a monad |
|
|
|
|
|
----- |
|
|
Back to Set theory vs. Catageory "Set" |
|
|
|
|
|
Set Theory: "Sets are things that have elements that we can use to define things." |
|
|
Set category: "We have arrows between objects. We don't know about sets or elements. We know composition." |
|
|
|
|
|
Rediscover/redfine things in terms of arrows under composition. |
|
|
|
|
|
Method for doing this rediscovery: Universal Construction. |
|
|
* Define a pattern (pattern: some combination of objects and arrows) |
|
|
* Find everything that matches this pattern |
|
|
* Order the matches |
|
|
* The top match is it |
|
|
|
|
|
Example 1: Singleton set |
|
|
* A singleton set has an arrow from every other object in the category: a -> () |
|
|
... including a function from Void -> () (but you can't call it) |
|
|
This doesn't give us much; almost all sets have this property |
|
|
(except non-empty set to empty set) |
|
|
* The difference is that there is a *unique* arrow from any set to the singleton set. |
|
|
* `unit` is a "Terminal object". All arrows converge on it. |
|
|
* A terminal object is an object in a category s.t. |
|
|
1. forall a . exists f :: a -> () |
|
|
2. forall f :: a -> (), g :: a -> () => f == g |
|
|
|
|
|
Terminal object example: Order |
|
|
* The arrows in N e.g. represent <= |
|
|
* There is no "largest" n in N |
|
|
* hence, there is no terminal object in this category over N |
|
|
|
|
|
Example 2: Empty set |
|
|
* Can be defined in terms of outgoing arrows. |
|
|
* Void -> a (`absurd`) |
|
|
* "You cannot prove that I don't have this function" |
|
|
* Initial object: Has a unique outbound arrow to every other object (incl. itself, i.e. Identity) |
|
|
|
|
|
When a category has an Initial or Terminal object, then ... |
|
|
* Any path to a Terminal object can be shrunk to a unique arrow |
|
|
* Likewise in the opposite direction for Initial object |
|
|
|
|
|
Arrows can be shown to be equal, by comparing their ends |
|
|
What does it mean for objects to be "equal"? Dunno! |
|
|
We can say they are isomorphic (or not) f::a -> b and g::b -> a, and composition = Identity |
|
|
|
|
|
Terminal object is unique up to an isomorphism |
|
|
(if you have two terminal objects, then they describe a unique isomorphism) |
|
|
|
|
|
Proof |
|
|
Suppose we have two Terminal objects a and b |
|
|
By definition there is a unique arrow from every object |
|
|
Therefore there are unique arrows f::a -> b and g::b -> a |
|
|
let h = Identity of a (similarly for Id b) |
|
|
By definition, h must be unique |
|
|
note that g . f = Id a and f . g = Id b (this defines the isomorphism) |
|
|
Therefore, this is a unique isomorphism -- there cannot be any other arrows because a and b are terminal. |
|
|
|
|
|
Example Universal Construction |
|
|
1. Pick a pattern. |
|
|
- A single object. |
|
|
2. Find all the matched |
|
|
- All objects in the category |
|
|
3. Order them (maybe partial) |
|
|
- a is better than b if there is a unique arrow b -> a |
|
|
4. What is the best fit? |
|
|
- The object b at the top of the arrows, viz. the terminal object |
|
|
|
|
|
Note you can find the initial object by inverting the sense of the comparison |
|
|
|
|
|
|
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
|
Category Theory 4.2: Products |
|
|
https://www.youtube.com/watch?v=Bsdl_NKbNnU&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&index=8 |
|
|
|
|
|
One more note on terminal objects: What about outgoing arrows from terminal object? |
|
|
There usually are outgoing arrows. |
|
|
|
|
|
Reversing the arrows of the Construction reveals a deeper truth: |
|
|
Every construction implies another construction with the arrows reversed |
|
|
|
|
|
For every category, you can create another category with the arrows reversed. |
|
|
|
|
|
Category C = f :: a -> b => C^{op} = f^{op} :: b -> a |
|
|
g :: b -> c g^{op} :: c -> b |
|
|
g . f g^{op} . f^{op} |
|
|
|
|
|
so (g . f)^{op} = g^{op} . f^{op} |
|
|
|
|
|
It's Composable. |
|
|
And since Id^{op} = Id, we have the "op" category. |
|
|
|
|
|
Cartesian Product |
|
|
|
|
|
Set definition: forall x in X, y in Y => (x, y) |
|
|
Category definition (in terms of arrows/functions): |
|
|
* Projection: for every Cartesion Product A x B, there are two arrows fst and snd |
|
|
* All we know is we have an object, and an arrows going from it to a and another going to b |
|
|
|
|
|
Now let's rank/order patterns that match |
|
|
|
|
|
c' |
|
|
/|\ |
|
|
p' / | \ q' |
|
|
/ |m \ |
|
|
v v v |
|
|
a<--c-->b |
|
|
p q |
|
|
|
|
|
|
|
|
Compare candidates c and c'. |
|
|
* c has arrows p and q to a and b, resp. |
|
|
* c' has arrows p' and q' to a and b, resp. |
|
|
* (p' p', q, and q' are "projections") |
|
|
* c is better than c' if there is a unique morphism (arrow) m from c' to c |
|
|
* p . m = p' |
|
|
* q . m = q' |
|
|
* The factors of p' are p and m |
|
|
* The factors of q' are q and m |
|
|
* p' and q' share a common factor, so we can factor it out and get c |
|
|
|
|
|
|
|
|
Let c = (Int, Bool) |
|
|
Let c' = Int |
|
|
|
|
|
The morphism m is :: Int -> (Int, Bool) |
|
|
:: x -> (x, Bool) |
|
|
|
|
|
Let c = (Int, Bool) |
|
|
Let c' = (Int, Int, Bool) |
|
|
p' :: (Int, Int, Bool) -> Integer |
|
|
p' x _ _ = x |
|
|
q' :: (Int, Int, Bool) -> Bool |
|
|
q' _ _ b = b |
|
|
|
|
|
The morphism m is :: (x, y, b) -> (x, b) |
|
|
|
|
|
|
|
|
Define Product with arrows & objects (Categorical Product) |
|
|
A product of two objects a and b is a third object c with arrows p :: c -> a and q :: c -> b |
|
|
For any other c' (p' :: c' -> a and q' :: c' -> b) there is a unique morphism m :: c' -> c |
|
|
that factorizes the two projections (p' = p . m and q' = q . m) |
|
|
|
|
|
c is the product of a * b |
|
|
|
|
|
|
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
|
Category Theory 5.1: Coproducts, sum types |
|
|
https://www.youtube.com/watch?v=LkIRsNj9T-8&index=9&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_ |
|
|
|
|
|
|
|
|
Coproduct: Dual of the Product; take the Product and reverse the arrows. a.k.a "Injection" |
|
|
|
|
|
i j |
|
|
a-->c<--b |
|
|
\ | / |
|
|
i' \ |m / j' |
|
|
\ | / |
|
|
vvv |
|
|
c' |
|
|
|
|
|
Observe that: |
|
|
j' = m . j |
|
|
i' = m . i |
|
|
|
|
|
Note that the order of the composition is reversed as well. |
|
|
|
|
|
How do I use it? |
|
|
Product is Cartesian Product, Tuples, Pairs. What is a Coproduct? |
|
|
|
|
|
Like union of two disjoint sets |
|
|
|
|
|
Or you could "tag" elements from a and b in c and get a Discriminated Union, a.k.a. Tagged Union, Variant, Sum type. |
|
|
Used to hold a value that may take on several different, but fixed types. |
|
|
|
|
|
Example: |
|
|
Boolean = True | False : Tagged Union. A value is one or the other. |
|
|
|
|
|
Contrast with |
|
|
Tuple = (Int, Bool) : Product type. |
|
|
|
|
|
Another Example: Enum is a Tagged type |
|
|
|
|
|
Another Example: |
|
|
data Either a b = Left a | Right b |
|
|
|
|
|
takes two types (a and b) and can be constructed two ways (as above). |
|
|
n.b. Left/Right correspond to i/j in the Coproduct diagram. |
|
|
|
|
|
Product types + Sum types are the foundation of the type system. |
|
|
|
|
|
Why are they called Product & Sum? |
|
|
* Product is like Cartesian pairs; |
|
|
* Sum is like ... addition? |
|
|
|
|
|
|
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
|
Category Theory 5.2: Algebraic data types |
|
|
https://www.youtube.com/watch?v=w1WMykh7AxA&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&index=10 |
|
|
|
|
|
Multiplication: |
|
|
* Monoid: associative, closed binary operation, unit element |
|
|
|
|
|
How does this translate to types? |
|
|
|
|
|
Associativity: |
|
|
((a, b), c) /= (a, (b, c)) NOT THE SAME |
|
|
|
|
|
However, all the info is there, so you can define a function e.g.: |
|
|
assoc ((a, b), c) = (a, (b, c)) |
|
|
Product types are associative in this sense |
|
|
|
|
|
n.b. that since they are associative up to isomorphism, these are essentially the same: |
|
|
((a, b), c) == (a, (b, c)) == (a, b, c) |
|
|
|
|
|
Unit element: Unit Type |
|
|
Again: (a, ()) NOT THE SAME AS a, but isomorphic with these helpers: |
|
|
munit (a, ()) = a {- munit = fst -} |
|
|
munit_inv x = (x, ()) |
|
|
|
|
|
Product types are isomorphic to multiplication |
|
|
|
|
|
Product types are "symmetric up to isomorphism" : |
|
|
(a, b) is isomorphic to (b, a) : |
|
|
|
|
|
swap :: (a, b) -> (b, a) |
|
|
swap p = (snd p, fst p) |
|
|
|
|
|
So... Sum Types |
|
|
Also monoidal: |
|
|
Symmetric up to isomorphism, e.g. Either a b ~ Either b a |
|
|
Associative up to isomorphism, e.g. data Triple a b c = Left a | Middle b | Right c |
|
|
Ordering does not matter! |
|
|
Unit of Sum: Void type => Either a Void ~ a |
|
|
a + 0 == a |
|
|
|
|
|
Combine Sum & Product types |
|
|
|
|
|
a * 0 = 0 |
|
|
(a, Void) ~ Void |
|
|
|
|
|
Distributive: |
|
|
a * (b + c) = a * b + a * c |
|
|
|
|
|
Also true (up to isomorphism), e.g.: |
|
|
(a, Either b c) ~ Either (a, b) (a, c) |
|
|
|
|
|
Product & Sum together forms a Semiring (a.k.a. Rig, a "Ring without the 'n'") |
|
|
For a true ring we need an inverse operation. |
|
|
|
|
|
Some isomorphisms: |
|
|
|
|
|
Bool : True | False ~ 2 = 1 + 1 |
|
|
Maybe a : Nothing | Just a ~ 1 + a |
|
|
also Either () a |
|
|
|
|
|
Algerbraic equations |
|
|
|
|
|
l(a) = 1 + a * l(a) |
|
|
|
|
|
l(a) - a * l(a) = 1 |
|
|
l(a)(1 - a) = 1 |
|
|
l(a) = 1/(1 - a) |
|
|
= n=0->infinity sum a^n = 1 + a + a*a + a*a*a + ... |
|
|
= data List a = Nil | Cons a (List a) |
|
|
|
|
|
|
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
|
Category Theory 6.1: Functors |
|
|
https://www.youtube.com/watch?v=FyoQjkwsy7o&index=11&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_ |
|
|
|
|
|
Functor is a mapping from one category to another |
|
|
How do we define mapping between categories? |
|
|
Map objects (e.g. sets in a small category) => Functions |
|
|
- But functions are mapping between sets, and sets have no *structure* |
|
|
- We want to find a way to map while preserving structure |
|
|
- Discrete Category: No arrows except Id. Corresponds to a Set (objects are elements |
|
|
in the Set); models "structurlessness". |
|
|
- Any category that is not Discrete has structure, i.e. other arrows |
|
|
- Therefore: We need to be able to map the arrows as well! |
|
|
|
|
|
F |
|
|
a ----------------> F a |
|
|
| | |
|
|
f | | F f (mapping the morphism f) |
|
|
| | |
|
|
v v |
|
|
b ----------------> F a |
|
|
|
|
|
Hom-set: Hom-set |
|
|
C(a, b) D(F a, F b) |
|
|
|
|
|
So we need a function that maps objects |
|
|
and a function that maps Hom-sets |
|
|
To preserve structure, we must preserve composition as well |
|
|
e.g. If we have a morphism g :: b -> c, we can also add an arrow g . f :: a -> c |
|
|
We must then have F g :: F b -> F c and F g . F f :: F a -> F c |
|
|
And: F (g . f) == F g . F f |
|
|
And: F Id_a == Id_{F a} |
|
|
|
|
|
And that is a Functor. |
|
|
A mapping of objects and morphisms that preserves composition. |
|
|
Any morphism in the source category must have an associated arrow in the target category. |
|
|
|
|
|
Faithful Functor: Injective on hom-sets |
|
|
Full Functor: Surjective on hom-sets |
|
|
n.b.: Objects are not part of the definition of Faithful/Full. Objects may be squeezed |
|
|
and still be Faithful or Full. |
|
|
|
|
|
Constant Functor: Maps all objects into one, and all morphisms into Id (e.g. \delta c) |
|
|
Endofunctor: A mapping of objects/morphisms into the same category |
|
|
|
|
|
What does this have to do with programming? |
|
|
|
|
|
Objects => Types |
|
|
Morphisms => Functions |
|
|
|
|
|
Mapping of types: Type Constructor (Parameritzed Data Type, Generic Type, Template Type, etc.) |
|
|
Maybe a: maps a -> Maybe a |
|
|
Mapping of functions: |
|
|
|
|
|
F |
|
|
a ----------------> Maybe a |
|
|
| | |
|
|
f | | fmap f (mapping the morphism f) |
|
|
| | |
|
|
v v |
|
|
b ----------------> Maybe a |
|
|
|
|
|
Transforms (a -> b) into the lifted context |
|
|
fmap :: (a -> b) -> (Maybe a -> Maybe b) |
|
|
fmap f Nothing = Nothing |
|
|
fmap f (Just x) = Just (f x) |
|
|
|
|
|
Theorems for Free: read this paper later |
|
|
From the type of a polymorphic function we can derive a theorem that it satisfies. |
|
|
Every function of the same type satisfies the same theorem. This provides a free |
|
|
source of useful theorems, courtesy of Reynolds' abstraction theorem for the |
|
|
polymorphic lambda calculus. |
|
|
http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html |
|
|
http://homepages.inf.ed.ac.uk/wadler/papers/free/free.dvi |
|
|
|
|
|
|
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
|
Category Theory 6.2: Functors in programming |
|
|
https://www.youtube.com/watch?v=EO86S2EZssc&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&index=12&spfreload=1 |
|
|
|
|
|
Is Maybe a lawful functor? |
|
|
[x] Maps types (objects) |
|
|
[x] Maps functions (morphisms) |
|
|
[?] Preserves composition |
|
|
[?] Preserves identity |
|
|
|
|
|
Type system cannot encode preservation of composition/identity. |
|
|
But, we may still be able to prove Maybe preserves structure. |
|
|
|
|
|
Equational Reasoning: inline & refactor to show semantics are the same |
|
|
|
|
|
1. Claim: |
|
|
fmap id = id |
|
|
Proof: |
|
|
fmap id Nothing = Nothing |
|
|
= id Nothing |
|
|
fmap id (Just x) = Just (id x) |
|
|
= Just x |
|
|
id (Just x) = Just x |
|
|
|
|
|
2. Claim: |
|
|
fmap (g . f) = (fmap g) . (fmap f) |
|
|
This follows from parametric polymorphism & proof of id law. "Theorem for Free" |
|
|
|
|
|
* Usually when you define a functor with ADTs, it will satisfy these laws (in Haskell) |
|
|
|
|
|
How do we define a functor in general in Haskell? |
|
|
|
|
|
Lifting: f gets "lifted" into Maybe context |
|
|
|
|
|
fmap f |
|
|
Maybe a --------> Maybe b |
|
|
^ ^ |
|
|
| | |
|
|
| | |
|
|
| | |
|
|
a --------> b |
|
|
f |
|
|
|
|
|
ad hoc polymorphism: Typeclasses |
|
|
* Define a family of types that share a common interface (OO anyone?) |
|
|
* Example: |
|
|
class Eq a where |
|
|
(==) :: a -> a -> Bool |
|
|
"There is an operator `==` that takes two 'elements' of type a and produce a Boolean." |
|
|
This is just a signature -- different types can implement for their needs |
|
|
n.b. Eq is parameterized by type "a" |
|
|
|
|
|
Functor is not parameterized by types, it is a type *constructor*. e.g., Maybe takes a type, produces a type. |
|
|
class Functor f where |
|
|
fmap :: (a -> b) -> (f a -> f b) -- this sig tells the compiler that `f` acts on types |
|
|
|
|
|
More functor examples! |
|
|
|
|
|
data List a = Nil | Cons a (List a) |
|
|
1. List is a type constructor (List of Int, List of Bool, etc.) |
|
|
2. Is it a functor? define an instance of functor: |
|
|
instance Functor List where |
|
|
fmap :: (a -> b) -> List a -> List b |
|
|
fmap f Nil = Nil |
|
|
fmap f (Cons head tail) = Cons (f head) (fmap f tail) |
|
|
-- fmap = map |
|
|
|
|
|
type Reader r a = r -> a |
|
|
= (->) r a |
|
|
|
|
|
fmap :: (a -> b) -> (f a -> f b) |
|
|
(a -> b) -> (r -> a) -> (r -> b) |
|
|
fmap f g = f . g |
|
|
= (.) f g |
|
|
fmap = (.) -- fmap for Reader/Function is composition. Neat. |
|
|
|
|
|
What is the general intuition behind Functor? |
|
|
* A functor acting on a type encapsulates the value of the type. Sort of. |
|
|
* Analogous to a "container" |
|
|
* How is Reader a container? |
|
|
- A function (Bool -> *) can be described as a container of two values |
|
|
- A function (Int -> *) can be described as a container of a sequence of values |
|
|
* Distinction between DataType/Function is weak |
|
|
- e.g. infinite list [1..] is implemented as a function |
|
|
- e.g. data types are implemented as thunks |
|
|
- conclusion: There is no real distinction between Data Type and Function |
|
|
|
|
|
|
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
|
Category Theory 7.1: Functoriality, bifunctors |
|
|
https://www.youtube.com/watch?v=pUQ0mmbIdxs&index=13&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_ |
|
|
|
|
|
Composing Functors G . F |
|
|
|
|
|
F G |
|
|
a ----------------> F a ----------------> G (F a) |
|
|
| | | |
|
|
f | | F f | G (F f) |
|
|
| | | |
|
|
v v v |
|
|
b ----------------> F a ----------------> G (F b) |
|
|
|
|
|
|
|
|
|
|
|
Functor Identity (map everything to itself) |
|
|
|
|
|
F . Id = F |
|
|
Id . F = F |
|
|
|
|
|
Functors define a category "Cat" where Functors are the morphisms and categories are the objects |
|
|
|
|
|
Example of composition of functors, Maybe and List: |
|
|
|
|
|
safeTail :: [a] -> Maybe [a] |
|
|
safeTail [] = Nothing |
|
|
safeTail (x:xs) = Just xs |
|
|
|
|
|
Maybe List is also a functor. Define fmap: |
|
|
|
|
|
fmap (fmap f) ms |
|
|
(fmap . fmap) f ms |
|
|
|
|
|
fmap for each level of composition. |
|
|
|
|
|
Claim: |
|
|
Algebraic Data Structures are automatically Functorial. |
|
|
i.e. Product & Sum types |
|
|
|
|
|
Is a Product (a, b) a Functor? |
|
|
|
|
|
(a, b) == (,) a b |
|
|
|
|
|
If we fix a, we get a functor in b. It is a type constructor in b. |
|
|
Then a function is applied to the b. |
|
|
|
|
|
(e, a) -------> (e, b) |
|
|
^ ^ |
|
|
| | |
|
|
| | |
|
|
a ------------> b |
|
|
|
|
|
fmap f (e, x) = (e, x) -> (e, f x) |
|
|
|
|
|
The pair is a "container" for the second object. You could also flip |
|
|
and use the same reasoning. |
|
|
|
|
|
Is it a functor in both a and b at the same time? Yes. |
|
|
We can define a functor that works on a pair of categories, i.e. a product of two categories. |
|
|
|
|
|
Define a product of two categories: |
|
|
In small categories, objects form sets. |
|
|
Take objects from C and D and form CxD = (c, d) |
|
|
Morphisms pair in the same way. Hom-sets are sets, so you can take the Cartesian Product. |
|
|
Composition: (f', g') . (f, g) = (f' . f, g' . g) |
|
|
Identity: (id_a, id_b) = id_{(a, b)} |
|
|
|
|
|
It's just a category. So we can define a functor from CxD -> E (some category E) |
|
|
|
|
|
Bifunctor: A functor from CxD -> E. A functor from the Product category. |
|
|
A mapping from two types into a type. |
|
|
Two functions are lifted at the same time. |
|
|
|
|
|
Haskell Example: |
|
|
|
|
|
class Bifunctor b where |
|
|
bimap :: (a -> a') (b -> b') -> f a b -> f a' b' |
|
|
|
|
|
"A Product is a Bifunctor" |
|
|
|
|
|
So... What about Sum? Is that functorial? |
|
|
|
|
|
* Use the same bifunctor id. |
|
|
* Either a b is a bifunctor. Takes two types, returns a single type. |
|
|
|
|
|
Category with a bifunctor is called Monoidal. That meeans there is a unit as well. |
|
|
|
|
|
|
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
|
Category Theory 7.2: Monoidal Categories, Functoriality of ADTs, Profunctors |
|
|
https://www.youtube.com/watch?v=wtIKd8AhJOc&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&index=14 |
|
|
|
|
|
Monoidal Categories |
|
|
* What does it mean to "multiply" two objects? |
|
|
- Categorical Product |
|
|
- Associativity |
|
|
- Unit |
|
|
* in Haskell we have Unit type; in CT this corresponds to Terminal Object |
|
|
Claim: |
|
|
a * () = a |
|
|
() * a = a |
|
|
|
|
|
Proof: |
|
|
Candidiate |
|
|
|
|
|
a |
|
|
id / \ unit |
|
|
v v |
|
|
a () |
|
|
|
|
|
add object b with projection p :: b -> a and unit_b :: b -> () |
|
|
Is there a unique morphism from b -> a? |
|
|
observe id . p = p |
|
|
So we have the same object (a). |
|
|
QED |
|
|
|
|
|
So: If you have a Categorical Product for every pair of objects and Terminal object |
|
|
for the category, then you have monoidal structure for objects, i.e. a |
|
|
Monoidal Category. |
|
|
|
|
|
Tensor Product: A monoidal category has a Tensor Product and a unit. (., 1) |
|
|
|
|
|
---- |
|
|
Const Functor |
|
|
Takes any type a, and maps it into a single object c (a.k.a. \delta c) |
|
|
|
|
|
data Const c a = Const c |
|
|
|
|
|
`a` disappears. Is this a functor? |
|
|
|
|
|
instance Functor (Const c) -- note that `Const c` requires a type argument (`a`) |
|
|
-- fmap :: (a -> b) -> Const c a -> Const c b |
|
|
fmap f (Const c) = Const c |
|
|
|
|
|
Identity Functor |
|
|
|
|
|
data Identity a = Identity a |
|
|
|
|
|
instance Functor (Identity a) |
|
|
fmap f (Identity a) = Identity (f a) |
|
|
|
|
|
|
|
|
Maybe redux |
|
|
|
|
|
data Maybe a = Nothing | Just a |
|
|
|
|
|
this is equivalenet to saying: |
|
|
|
|
|
Either () (Identity a) |
|
|
-- or |
|
|
Either (Const () a) (Identity a) |
|
|
|
|
|
Since we can produce Maybe by composing Functors, it is a Functor. QED. |
|
|
|
|
|
extension to Haskell: |
|
|
{-# LANGUAGE DeriveFunctor #-} |
|
|
|
|
|
e.g. |
|
|
data MyF = ..... deriving Functor |
|
|
|
|
|
If you data type parametrically polymorphic, there can be only one `fmap`. Theorem for free. |
|
|
|
|
|
Function |
|
|
"arrow" is a type constructor of two arguments: |
|
|
|
|
|
(->) a b = a -> b |
|
|
|
|
|
(see Reader functor above. Function is Functorial in the second argument.) |
|
|
newtype Reader c a = Reader (c -> a) |
|
|
-- recall `fmap` for Reader = (.), i.e. composition. |
|
|
|
|
|
|
|
|
data Op c a = Op (a -> c) |
|
|
fmap :: (a -> b) -> Op c a -> Op c b |
|
|
= fmap :: (a -> b) -> (a -> b) -> (b -> c) |
|
|
problem |
|
|
here |
|
|
|
|
|
arrow from a -> b prevents composing to get b -> c |
|
|
We can invert the arrows in the Co-category ... |
|
|
|
|
|
This should be called Cofunctor! But it's NOT! It's called "Contravariant." |
|
|
|
|
|
class Contravariant f where |
|
|
contramap :: (b -> a) -> (f a -> f b) |
|
|
|
|
|
Back to (->) as a "Functor thingie" |
|
|
|
|
|
(->) a b goes from C^{op} x C -> C |
|
|
Take a pair of morphisms, but the first one is flipped. |
|
|
This is called a Profunctor. |
|
|
|
|
|
classProfunctor p where |
|
|
dimap :: (a' -> a) -> (b -> b') -> (p a b) -> (p a' b') |
|
|
|
|
|
first morphism is "flipped" (C^{op}). |
|
|
|
|
|
Define `dimap` for (->) |
|
|
dimap :: (a' -> a) -> (b -> b') -> (p a b) -> (p a' b') |
|
|
f g h::a->b a'->b' |
|
|
dimap = g . h . f |
|
|
|
|
|
(->) is the simplest Profunctor. |
|
|
|
|
|
|
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
|
Category Theory 8.1: Function objects, exponentials |
|
|
https://www.youtube.com/watch?v=REqRzMI26Nw&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&index=15 |
|
|
|
|
|
Function types (finally) |
|
|
When a and b are sets: |
|
|
* Hom-set is a set, so there is a set a -> b that corresponds to the hom-set between objects a and b. |
|
|
* the homset is also an object in the category. |
|
|
|
|
|
* In an arbitrary category, we have the Hom-set as an external thing. |
|
|
* What we want is an *internal* Hom-set. |
|
|
* In many categories it is possible to define such a Hom-set. |
|
|
|
|
|
We can use Universal Construction to construct a Function object. |
|
|
|
|
|
First we must have a Category with Product. |
|
|
Model Function as a Pair, Function z and Argument a, that returns result b. |
|
|
So we have a Cartesian Product of z x a like so: |
|
|
|
|
|
+-+ +-----+ |
|
|
| | | | eval |
|
|
|z| |z * a|-----> b |
|
|
| | | | |
|
|
+-+ +-----+ |
|
|
+-----+ |
|
|
| a | |
|
|
+-----+ |
|
|
|
|
|
Now, do the Universal Construction thing. Imagine another candidate z'. |
|
|
There is a Product z' * a, and a morphism g :: (z', a) -> b |
|
|
|
|
|
Now we need to factor through g and eliminate g'. |
|
|
Add an arrow h from z' to z. But we also need an arrow from (z', a) and (z, a) |
|
|
so we can factor out g'. |
|
|
|
|
|
Remember: Product is a *Bifunctor*: Takes two morphisms and produces a third morphisms. |
|
|
So the first morphism is h :: z' -> z, and the second morphism is Identity (a -> a). |
|
|
That maps (z', a) into (z, a). |
|
|
Now we have a path from (z', a) to b through g. |
|
|
g' = g . (h * id) |
|
|
Therefore, (z, a) is the better candidate. |
|
|
QED |
|
|
|
|
|
In the diagram, you can think of g' as a Function of two arguments. |
|
|
Observe that a function of two arguments is equivalent to a function |
|
|
of one argument that returns a function of one argument (down the `h` arrow). |
|
|
Currying is built into this Universal construction. |
|
|
|
|
|
h :: z -> (a -> b) |
|
|
g :: (z, a) -> b |
|
|
|
|
|
curry f = \a -> \b -> f (a, b) |
|
|
translates a function from a pair into a function of one argument to a new function |
|
|
|
|
|
uncurry f = \(a, b) -> f a b |
|
|
translates a curried function into a function that takes a pair of arguments. |
|
|
|
|
|
In Haskell: |
|
|
* Function Arrows associate to the right. |
|
|
* Function application (call) associates to the left |
|
|
|
|
|
In category theory, this is NOT called a function: It is call an "exponential". |
|
|
a -> b ~ b^a |
|
|
Argument on top, result in the base. |
|
|
|
|
|
Example: Bool -> Int is a pair of Integers (one for False, one for True) |
|
|
All possible Bool -> Functions is all possible (Int, Int) pairs. |
|
|
This is the same as Int * Int, or Int^2 or Int^{Bool} |
|
|
|
|
|
As long as the types are finite sets, the number of functions (a -> b) = b^a |
|
|
|
|
|
Cartesian Closed Categories (CCC): |
|
|
Products for every pair of objects. |
|
|
"Closed" means it has exponentials as well, i.e. for every (a, b) there is a^b |
|
|
And it has a Terminal Object. Like the zeroth power of an object. |
|
|
|
|
|
If it has initial object as well, then it is a Bi-Cartesian Closed Category (BCCC) |
|
|
|
|
|
With exponentials, we can do more algebra ... yay? |
|
|
|
|
|
a^0 = 1 |
|
|
a^{Void} = () |
|
|
absurd :: Void -> a = () |
|
|
|
|
|
:. Exponential works for types with a^0 |
|
|
|
|
|
1^a = 1 |
|
|
a -> () |
|
|
|
|
|
a^1 = a |
|
|
() -> a ~ a |
|
|
|
|
|
|
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
|
Category Theory 8.2: Type algebra, Curry-Howard-Lambek isomorphism |
|
|
https://www.youtube.com/watch?v=iXZR1v3YN-8&index=16&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_ |
|
|
|
|
|
a^{b + c} = a^b * a^c |
|
|
Either b c -> a ~ (b -> a), (c -> a) |
|
|
|
|
|
(a^b)^c = a^{b * c} |
|
|
c -> b -> a ~ (c, b) -> a -- currying |
|
|
|
|
|
(a * b)^c a^c * b^c |
|
|
c -> (a, b) ~ (c -> a, c -> b) |
|
|
-- IOW one function that produces a pair can be replaced by two function that produce each element of the pair. |
|
|
|
|
|
----- |
|
|
Programming, Type theory, Category theory, etc.: The same stuff keeps coming up. Why is that? |
|
|
* Curry-Howard isomorphism: Propositions as Types. |
|
|
One-to-One correspondence from type theory/programming/lambda calculus to logic. |
|
|
|
|
|
Proposition corresponds to Type. |
|
|
Proposition is True | False |
|
|
Type is Inhabited | Uninhabited |
|
|
|
|
|
If we can construct an element of a Type, we have "proven the proposition". |
|
|
|
|
|
Logic Type |
|
|
----- ----- |
|
|
True Unit |
|
|
False Void |
|
|
conjunction AND (a, b) |
|
|
disjunction OR Either a b (or Sum type data S = X | Y) |
|
|
implication a => b a -> b |
|
|
modus ponens (a => b) ^ a function application |
|
|
|
|
|
Lambek added a third correspondence to objects in a CCC. |
|
|
https://wiki.haskell.org/Curry-Howard-Lambek_correspondence |
|
|
The Curry-Howard-Lambek correspondence is a three way isomorphism between types (in programming languages), propositions (in logic) and objects of a Cartesian closed category. Interestingly, the isomorphism maps programs (functions in Haskell) to (constructive) proofs in logic (and vice versa). |
|
|
|
|
|
|
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
|
Category Theory 9.1: Natural transformations |
|
|
https://www.youtube.com/watch?v=2LJC-XD5Ffo&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&index=17 |
|
|
|
|
|
Natural Transformations |
|
|
|
|
|
One of the (3) foundations of CT |
|
|
* Definition of Category: |
|
|
- Objects, Morphisms, Composition, Identity. All about structure. |
|
|
* Defintion of Functor: |
|
|
- Mappings between categories that preserve structure. |
|
|
- Embed/Mopdel a category inside another category |
|
|
* Definition of Natural Transformations: |
|
|
- Mappings between functors, preserving structure. |
|
|
|
|
|
Definition (expanded) |
|
|
Two categories, C and D. |
|
|
Functor F maps object a in C to object (F a) in D |
|
|
Functor G maps object a in C to object (G a) in D |
|
|
We need a mapping in D between (F a) and (G a), i.e. F a -> G a |
|
|
- But -- D already has mappings. |
|
|
- We don't want to just arbitrarily add one |
|
|
- But we should be able to pick one from the hom-set (F a -> G a) |
|
|
For every object in C, find two object imagess in D, and choose a morphism in D between those images |
|
|
These morphisms are called a "Component". (A Component is a morphism) |
|
|
- e.g. \alpha_a :: F a -> G a |
|
|
- Observe that although `a` is in C, the Component F a -> F g is in D. |
|
|
|
|
|
All the Components taken together form a family of morphisms, and that is the Natural Transformation. |
|
|
Except we need to talk about structure of C being preserved in D (i.e. morphisms in C) |
|
|
|
|
|
Take objec b in C and map into F b and G b |
|
|
- So we have a Component \alpha_b :: F a -> F b |
|
|
- what about morphism f :: a -> b in C? That will be mapped by Functor F to F f and by G to G f. |
|
|
|
|
|
What is the relationship between F f G f? Are they "similar"? |
|
|
An NT does not have to exist at all. There are such categories. |
|
|
There must be a relation between the four arrows: \alpha_a, \alpha_b, F f, G f. |
|
|
Observe that G f . (F a -> F b) = G b = (F b -> G b) . F f = G b |
|
|
\alpha_a \alpha_b |
|
|
This equality is the "Naturality Condition" and the graph of it is the "Naturality Square" |
|
|
|
|
|
F f |
|
|
F a ------------> F b |
|
|
| | |
|
|
\alpha_a | | \alpha_b |
|
|
| | |
|
|
v v |
|
|
G a ------------> G b |
|
|
G f |
|
|
|
|
|
Another Definition: |
|
|
* NT maps objects to morphisms. |
|
|
* NT maps morphisms to commuting diagrams viz the "Naturality Square" |
|
|
|
|
|
In mathematics, and especially in category theory, a commutative diagram is a diagram of |
|
|
objects (also known as vertices) and morphisms (also known as arrows or edges) such that |
|
|
all directed paths in the diagram with the same start and endpoints lead to the same result |
|
|
by composition. |
|
|
|
|
|
NT gives us a higher-level language in CT for discussing commuting diagrams. |
|
|
We can replace talk of commuting diagrams with |
|
|
"There is a NT between functors." That implies the naturality squares. |
|
|
|
|
|
An invertible NT is called a "Natural Isomorphism" |
|
|
All of the morphisms in the Naturality Square will have arrows in the other direction as well. |
|
|
|
|
|
What is an NT in Programming? |
|
|
* A family of functions parameterized by a type |
|
|
* Hence a NT in programming context is a polymorphic function |
|
|
- e.g. alpha :: forall a . F a -> G a |
|
|
This is defined for all types `a`. |
|
|
(use "explicit forall" extension in Haskell) |
|
|
|
|
|
There is a subtle difference: |
|
|
* In Haskell we are assuming parametric polymorphism, i.e. can only define one formula *for all types* |
|
|
* This is much stronger than categorical definition. |
|
|
|
|
|
Why? |
|
|
Consider Naturality Square. |
|
|
\alpha_b . fmap_F f = fmap_G f . \alpha_a |
|
|
|
|
|
First fmap is for Functor f, second one is for Functor G. |
|
|
In Haskell, specifying the Functor instance is unnecessary. You get it for free. |
|
|
|
|
|
Example: List Functor and Maybe Functor |
|
|
|
|
|
safeHead :: [a] -> Maybe a |
|
|
safeHead [] = Nothing |
|
|
safeHead (x:_) = Just x |
|
|
|
|
|
safeHead works for every Type `a`. |
|
|
It is parametrically polymorphic. |
|
|
Claim: safeHead is automatically "Natural" |
|
|
|
|
|
Proof: |
|
|
Empty List case: |
|
|
1. fmap f [] = [] |
|
|
safeHead [] = Nothing |
|
|
2. safeHead [] = Nothing |
|
|
fmap f Nothing = Nothing |
|
|
|
|
|
Non-empty list case |
|
|
1. fmap f x:xs = f x : (fmap f xs) |
|
|
safeHead (x:xs) = Just x |
|
|
2. safeHead (x:xs) = Just x |
|
|
fmap f (Just x) = Just (f x) |
|
|
|
|
|
Practical benefit? CT provides opportunity for optimization. |
|
|
e.g. safeHead first then fmap is cheaper than fmap then safeHead |
|
|
compiler may be optimized to use these categorical transformations. |
|
|
|
|
|
NT never modifies the contents of the container. |
|
|
Instead it repackages into a different container. |
|
|
There is *no way* to modify the contents because the content is *polymorphic* |
|
|
OTOH, Functor preserves the container but may modify its contents. |
|
|
|
|
|
Naturality Condition means that it does not matter whether you |
|
|
repackage first and then fmap, or fmap first and then repackage. |
|
|
|
|
|
Examples: |
|
|
|
|
|
a -> [a] |
|
|
is a NT because `a` is equivalent to `Identity a`, so this is a mapping of |
|
|
Identity functor into List functor. |
|
|
|
|
|
length :: [a] -> Int |
|
|
Mapping a List Functor to a Const Functor. |
|
|
|
|
|
In general if you have a function from ADT -> ADT, it is a NT |
|
|
* Not all, though: There are mixed functors, e.g. contravariant in one argument, and covariant in the other |
|
|
that do not satisfy Naturality. |
|
|
|
|
|
Back to Kleisli arrows: |
|
|
|
|
|
a -> m b |
|
|
return :: a -> m a |
|
|
|
|
|
return is defined as a NT. (Same as Identity a -> [a], as shown above) |
|
|
|
|
|
|
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
|
Category Theory 9.2: bicategories |
|
|
https://www.youtube.com/watch?v=wrpxBXXgLCI&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&index=18 |
|
|
|
|
|
Generalizing Category Theory. |
|
|
uh-oh: "Deep math." |
|
|
|
|
|
Every time you are mapping ask yourself: Do they compose? |
|
|
What would it mean to compose NTs? |
|
|
|
|
|
NT \alpha :: F -> G |
|
|
NT \beta :: G -> H |
|
|
|
|
|
C D |
|
|
F |
|
|
+---------------------------> F a |
|
|
/ | |
|
|
/ | \alpha_a |
|
|
/ v |
|
|
a ------------------------------> G a |
|
|
\ | |
|
|
\ | \beta_a |
|
|
\ V |
|
|
+--------------------------> H a |
|
|
|
|
|
\alpha_a and \beta_a are morphisms. They compose (obv). So you can compose \beta . \alpha. |
|
|
Is the composition \beta . \alpha a NT? |
|
|
To determin that we would need to verify that: |
|
|
* there is an object b in C with an arrow f :: a -> b |
|
|
* then we have F b, G b, H b, and morphisms F f, G f, H f |
|
|
* Verify Naturality Condition: |
|
|
H a . (\beta_a . \alpha_a) = f a . (\beta_b . \alpha_b) |
|
|
That forms the composed Naturality Square, with corners F a, F b, H b, H a |
|
|
|
|
|
F a ------> F b |
|
|
| | |
|
|
| | |
|
|
G a - - - > G b |
|
|
| | |
|
|
v v |
|
|
H a ------> H b |
|
|
|
|
|
Is there Identity? |
|
|
An Identity NT is the family of morphisms from F a to itself. |
|
|
|
|
|
Is it associative? |
|
|
In Components, it is. |
|
|
|
|
|
Functors between categories [C, D] form a category where Functors are objects and NT are morphisms. |
|
|
Can be written D^C |
|
|
|
|
|
Back to Cat: |
|
|
* Objects are Categories |
|
|
* Morphisms are Functors |
|
|
|
|
|
F |
|
|
+-------------------+ |
|
|
/ || \ |
|
|
/ || \ |
|
|
C || D |
|
|
\ || / |
|
|
\ \/ / |
|
|
+-------------------+ |
|
|
G |
|
|
|
|
|
In Cat there are Functors between categories, and NTs between Functors. |
|
|
|
|
|
This is called a |
|
|
2-category. |
|
|
* in Cat, the Hom-Set is a set of Functors |
|
|
* Note that the Hom-set between two categores is itself a category |
|
|
* Therefore the Hom-set is also an element in Cat |
|
|
* [C, D] = D^C |
|
|
* Conclusion: Cat is CCC |
|
|
|
|
|
To construct a category with Hom-objects (instead of Hom-sets): |
|
|
* Hom-objects must be from a Monoidal category, using monoidal operator for composition |
|
|
* This called an "Enriched category" |
|
|
|
|
|
back to 2-category |
|
|
* There are two axes of composition. |
|
|
1. From object -> object (horizontal) |
|
|
2. From Functor -> Functor (vertical) |
|
|
* Consider two compositions of the horizontal type: G . F and G' . F' |
|
|
- How do we construct a NT from those functors? |
|
|
The functors fan out: |
|
|
1. Start with object a with Functors F a and F' a. There is an NT \alpha_a :: F a -> F' a |
|
|
2. At F a and F' a the split again: |
|
|
F a goes via G to (G . F) a |
|
|
F a goes via G' to (G' . F) a |
|
|
F' a goes via G to (G . F') a |
|
|
F' a goes via G' to (G' . F') a |
|
|
3. We can lift/transport \alpha_a to (G . F) a -> (G . F') a |
|
|
We can lift/transport \alpha_a to (G' . F) a -> (G' . F') a |
|
|
4. We have \beta_a (G . F) a -> (G' . F) a |
|
|
We have \beta_a (G . F') a -> (G' . F') a |
|
|
5. We get our composition G . F -> G' . F' either by: |
|
|
G' \alpha_a . \beta_a |
|
|
\beta . G' \alpha_a |
|
|
6. There is out Naturality Square. The diagram shows it better than I just wrote it, but would be a nightmare to try and do ACII style |
|
|
|
|
|
Wait -- it gets worse: |
|
|
Interchange law: Add \alpha' and beta' and draw arrows until your eyes bleed |
|
|
|
|
|
OK back to the show. |
|
|
|
|
|
If you have morphisms between morphisms, you can have isomorphisms between morphisms. |
|
|
Let's forget about "equality". |
|
|
Let's just say "up to isomorphism". |
|
|
|
|
|
Define a 2-category where things are defined "up to isomorphism": You get a Bicategory |
|
|
In a bicategory: Categorical Laws are up to isomorphism. |
|
|
Since things may not be strictly equal, but only up to isomorphism, you must have coherence laws |
|
|
for Associators and Unitors. |
|
|
Every n-category you go up spawns new coherence laws, and they are not unique. |
|
|
|
|
|
|
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
|
Category Theory 10.1: Monads |
|
|
https://www.youtube.com/watch?v=gHiyzctYqZ0&index=19&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_ |
|
|
|
|
|
Why do we need functions? |
|
|
Functions are about structuring code. |
|
|
Composition is the key. a -> b -> c -> d |
|
|
|
|
|
Monads are about structuring code. |
|
|
Composition is the key. |
|
|
|
|
|
Monad replaces the (.) of function composition with the Kleisli arrow (>=>) (fish operator) |
|
|
a >=> b >=> c >=> d |
|
|
|
|
|
Function Monad |
|
|
composition . >=> |
|
|
identity id return |
|
|
category Types/Functions Kleisli |
|
|
|
|
|
`return` can make functional-composition code look more imperative & maybe more readily understandable |
|
|
|
|
|
`fish` anatomy >=> |
|
|
* (>=>) :: (a -> m b) -> (b -> m c) -> (a -> m c) |
|
|
- `m` is a Functor (it's a Monad, but wait for it) |
|
|
- `m` is a type constructor and has `fmap`, i.e. it knows how to lift functions |
|
|
|
|
|
f >=> g = \a -> let mb = f a in mb >>= g |
|
|
-- need a function (>>=) to unwrap the b from f so g can use it: |
|
|
-- (>>=) :: m b -> (b -> m c) -> m c |
|
|
|
|
|
(>>=) a.k.a. `bind` arises from the need to compose with these "containers". |
|
|
|
|
|
class Monad m where |
|
|
(>>=) :: m a -> (a -> m b) -> m b (a.k.a. bind for composition) |
|
|
return :: a -> m a (Kleisli Identity arrow) |
|
|
|
|
|
Observe we can define `fmap` from `bind` and `return`. (IOW Monad is a Functor) |
|
|
|
|
|
This is sufficient to define a monad, but we can go deeper into the fish guts. |
|
|
Let's break down `bind`: |
|
|
|
|
|
m a >>= (a -> m b) = ??? fmap (a -> m b) (m a) |
|
|
ma >>= f = ??? fmap f ma |
|
|
= ??? m (m b) -- Not quite |
|
|
-- need a function `join :: m (m a) -> m a` to satisfy bind contract |
|
|
= join (fmap f ma) -- With `join`, we can define `bind` |
|
|
|
|
|
So: Alternative definition of Monad: |
|
|
|
|
|
class Functor m => Monad m where |
|
|
join :: m (m a) -> m a |
|
|
return :: a -> m a |
|
|
|
|
|
Why? What problems do Monads solve? |
|
|
* Composition for Kleisli arrows. Ummmm |
|
|
|
|
|
Recast the question: Why are Kleisli arrows useful? |
|
|
* Everything is pure functions |
|
|
* This causes some pain when trying to cope with e.g.: side-effects, state, exceptions, continuations ... |
|
|
* Everything can be converted to pure computation by replacing impure functions with embellished results. |
|
|
|
|
|
Where does the monad come in to this? |
|
|
* start with a giant computation a -> Embellished Result |
|
|
* To decompose this giant computation into small composable parts, you use monads. |
|
|
|
|
|
Examples: |
|
|
|
|
|
Maybe Monad |
|
|
* any partial function a -> b can be converted to a -> Maybe b |
|
|
* Now the partial function is a pure function. |
|
|
* How do you compose these purified functions? Monadic composition. |
|
|
|
|
|
join :: Maybe (Maybe a) -> Maybe a |
|
|
join (Just (Just x)) = Just x |
|
|
join _ = Nothing |
|
|
|
|
|
bind :: Maybe a -> (a -> Maybe b) -> Maybe b |
|
|
bind Nothing _ = Nothing |
|
|
bind (Just x) f = f a |
|
|
|
|
|
-- observe that we do not invoke `f` when we are dealing with `Nothing`. |
|
|
-- this is analogous to an exception. |
|
|
|
|
|
return :: a -> Maybe a |
|
|
return a = Just a |
|
|
|
|
|
Either Monad could also be used to encapsulate exceptions, and pass information about the failure along in the Left. |
|
|
|
|
|
Suppose you have a function a -> b that access some state s. Not a pure function, obv. |
|
|
We can turn it into a pure function by passing the state along explicitly: |
|
|
|
|
|
(a, s) -> (b, s) |
|
|
-- not quite Kleisli arro, but we can get there with curry: |
|
|
|
|
|
a -> (s -> (b, s)) |
|
|
|
|
|
newtype State s a = State (s -> (a, s)) -- parameterized by state s and functorial a (Reader Functor) |
|
|
-- arrow is functorial in the return type |
|
|
|
|
|
---------- |
|
|
Monad Laws |
|
|
|
|
|
1. Associativity |
|
|
2. Unit |
|
|
3. Identity |
|
|
|
|
|
Can't be expressed in Haskell directly, so back to CT we go |
|
|
|
|
|
Terminology map |
|
|
|
|
|
Haskell CT |
|
|
m T -- n.b.: T must be an endofunctor, i.e. mapping a category into itself |
|
|
join \mu |
|
|
return \eta |
|
|
|
|
|
\eta :: Id -> T (NT from Identity Functor to T) |
|
|
\mu :: T^2 -> T (NT from T composed with itself to T) |
|
|
|
|
|
A monad is a Functor T and two NTs. Plus laws. |
|
|
|
|
|
|
|
|
NT #1: \eta (return) |
|
|
Id |
|
|
+-------------------+ |
|
|
/ || \ |
|
|
/ || \ |
|
|
C || \eta C |
|
|
\ || / |
|
|
\ \/ / |
|
|
+-------------------+ |
|
|
T |
|
|
|
|
|
NT #2 \mu (join) |
|
|
T T |
|
|
+------> C ---------+ |
|
|
/ \ |
|
|
/ \ |
|
|
C C |
|
|
|\ T^2 /| |
|
|
| +---------------------+ | |
|
|
+ || + |
|
|
\ || \mu / |
|
|
\ \/ / |
|
|
+-------------------+ |
|
|
T |
|
|
|
|
|
Chase the diagram to show Associativity: |
|
|
|
|
|
\mu . (\mu o I) = \mu . (I o \mu) |
|
|
\mu . (\mu o T) = \mu . (T o \mu) |
|
|
|
|
|
|
|
|
T^3 |
|
|
\mu o I_T / \ I_T o \mu |
|
|
/ \ |
|
|
T^2 T^2 |
|
|
\ / |
|
|
\mu \ / \mu |
|
|
T |
|
|
|
|
|
Identity: |
|
|
|
|
|
Id o T -- \eta o T --> T^2 |
|
|
T o Id -- T o \eta --> T^2 |
|
|
T^2 -- \mu -------> T |
|
|
|
|
|
Id o T = T = T o Id |
|
|
QED |
|
|
|
|
|
|
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
|
Category Theory 10.2: Monoid in the category of endofunctors |
|
|
https://www.youtube.com/watch?v=GmgoPd7VQ9Q&index=20&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_ |
|
|
|
|
|
Let's talk monoids. |
|
|
* Usually defined in terms of sets |
|
|
* Can be represented as a single-object category with a bunch on endomorphisms. |
|
|
Every single object category is a monoid; and |
|
|
Every monoid can be expressed as a single-object category |
|
|
|
|
|
\mu :: a * a -> a -- function from a set of pairs from AxA to the product of those pairs |
|
|
\eta :: () -> a -- function from id element/terminal object to a |
|
|
|
|
|
(Recall that at Cartesian Category has a Product and a Terminal Object) |
|
|
|
|
|
Monoid Laws: |
|
|
* Associativity |
|
|
\mu (\mu (x, y), z) = \mu (x, \mu(y, z)) |
|
|
* Unit |
|
|
Left: \mu (\eta (), x) = x |
|
|
Right: \mu (x, \eta ()) = x |
|
|
|
|
|
See the diagram for how we reduced T^3 to T via \mu and I_T. |
|
|
Doing the same thing with ((a * a) * a) |
|
|
But -- (a * a) * a is not really "equal" to a * (a * a) |
|
|
But we can define morphisms to make these things equal up to isomorphism. |
|
|
|
|
|
Conclusion: Product is monoidal up to isomorphism. |
|
|
|
|
|
So a monoidal category is a category with |
|
|
* A Bifunctor :: (a, b) -> a ⊗ b (i.e. Tensor Product) |
|
|
* Identity object I |
|
|
|
|
|
Monoid: (I, ⊗) |
|
|
* object m |
|
|
* \mu :: m ⊗ m -> m |
|
|
* \eta :: I -> m |
|
|
|
|
|
Category of Endofunctors [C, C] |
|
|
* Objects are Endofunctors |
|
|
* Morphisms are Natural Transformations |
|
|
* Tensor Product is composition of endofunctors |
|
|
* Associativity: (F o G) o H = F o (G o H) |
|
|
* Unit: Identity Functor: Id o F = F = F o Id |
|
|
|
|
|
... |
buzzdecafe revised this gist