Last active
January 24, 2022 12:17
-
-
Save buzzdecafe/8bbc77e91b152eb94d8522c6ba9b4b30 to your computer and use it in GitHub Desktop.
Category Theory for Programmers: Notes
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 | |
... |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment