Category Theory & Haskell programming language
 http://www.seas.upenn.edu/~cis194/lectures.html
 https://wiki.haskell.org/Learning_Haskell
 http://yogsototh.github.io/CategoryTheoryPresentation
 https://bartoszmilewski.com/2014/10/28/categorytheoryforprogrammersthepreface/
My Notes:
Part One
1) Category: The Essence of Composition
Category is about composition of objects with arrows = morphisms
Category if:
 composition is associative
 for any object
a
there is an arrow which is unit of composition = identity exists
Analogy: surface area has to increase slower than their volume for chucks to be well composable
 Surface = information to compose
 Volume = information to implement
Haskell:
 Double colon means “has the type of…”
 Standard library is called Prelude
 Types begin with capital letter, variables with lowercase
2) Types and Functions
Type ≈ a set of values (+ bottom  Halting problem)
Set: category of sets, object = set, morphism = function
Function is either:
 Total: ∀ input, ∃ output
 Partial function: may return bottom
Eugenio Moggi discovered that computational effects can be mapped to monads
Types:
 for ∅: type without values, e.g. Void in Haskell((void in C++ is a singleton, not the same)) absurd :: Void → a
 singleton: type that has only one value, () = unit in Haskell, void in C++
 function a → Bool is called a predicate
Haskell:
 Types: Void, (), Bool, Char, String, Integer
 Bottom: , ⊥, undefined
 Hask: Category of Haskell types
 all functions are pure
 () is the type for singleton, is a constructor, is sometimes also value
 function returning () discards argument
Checks:
 operational semantics: simulation = tests
 denotational semantics: math = proof
3) Categories Great and Small
 Empty Category: ∅ objects, ∅ arrows
 Simple Graph: add arrows to make it a category → free category generated by a graph
 HomSet: In Category C, Set of morphisms a → b = HomC(a,b)
Orders:
 Preorder: Set + order relation (HomSet is either ∅ or singleton), cycles allowed
 Partial order: if a ≤ b and b ≤ a ⇒ a = b, tsort possible, no cycles
 Total order: every object is in relation, quicksort, bubble sort ... possible
Monoid:
 Set + associative binary operator, ∃ neutral element ≈ unit of composition
 e.g. (ℕ, +, 0) ((commutative)), (String, Concat, "") ((non commutative))
 Monoid Category: Single object category, set of morphisms is monoid
class Monoid m where
mempty :: m
mappend :: m > m > m
Notes:
 There are things larger than Set, morphisms don’t have to form a set
 A category in which morphisms between any two objects form a set is called locally small
 A lot of interesting phenomena in category theory have their root in the fact that elements of a homset can be seen both as morphisms, which follow the rules of composition, and as points in a set.
4) Kleisli Categories
Idea: embellishing return types of a bunch of functions in order to piggyback some additional information
Writer In C++
pair<bool, string> isEven(int n) {
return make_pair(n % 2 == 0, "isEven ");
}
pair<bool, string> negate(bool b) {
return make_pair(!b, "Not so! ");
}
In order to create the function isOdd, these cannot be composed directly (mismatching type)
pair<bool, string> isOdd(int n) {
pair<bool, string> p1 = isEven(n);
pair<bool, string> p2 = negate(p1.first);
return make_pair(p2.first, p1.second + p2.second);
}
template<class A>
using Writer = pair<A, string>;
template<class A, class B, class C>
function<Writer<C>(A)> compose(function<Writer<B>(A)> m1,
function<Writer<C>(B)> m2)
{
return [m1, m2](A x) {
auto p1 = m1(x);
auto p2 = m2(p1.first);
return make_pair(p2.first, p1.second + p2.second);
};
}
Alternative in C++14
auto const compose = [](auto m1, auto m2) {
return [m1, m2](auto x) {
auto p1 = m1(x);
auto p2 = m2(p1.first);
return make_pair(p2.first, p1.second + p2.second);
};
};
Writer in Haskell
type Writer a = (a, String)
The composition is a funny infix operator, sometimes called the “fish”:
(>=>) :: (a > Writer b) > (b > Writer c) > (a > Writer c)
m1 >=> m2 = \x >
let (y, s1) = m1 x
(z, s2) = m2 y
in (z, s1 ++ s2)
isOdd :: Integer > Writer [Bool]
isOdd = isEven >=> negate
Kleisli category
Kleisli category — a category based on a monad
A Kleisli category((For our limited purposes)): objects = types of programming language, morphisms from A > B to A > type derived from B using a particular embellishment
Each Kleisli category defines: own way of composing these morphisms + identity morphisms((with respect to that composition)).
Writer monad used for logging or tracing the execution of functions = Example of a more general mechanism for embedding effects in pure computations
You’ve seen previously that we could model programminglanguage types and functions in the category of sets (disregarding bottoms, as usual). Here we have extended this model to a slightly different category, a category where morphisms are represented by embellished functions, and their composition does more than just pass the output of one function to the input of another. We have one more degree of freedom to play with: the composition itself. It turns out that this is exactly the degree of freedom which makes it possible to give simple denotational semantics to programs that in imperative languages are traditionally implemented using side effects.
“embellishment”: = endofunctor
5) Products and Coproducts
 There is a common construction in category theory called the universal construction for defining objects in terms of their relationships.
 The initial object is the object that has one and only one morphism going to any object in the category
 The terminal object is the object with one and only one morphism coming to it from any object in the category.
 initial object and final object if they exist are unique up to one (also unique) isomorphism
 Duality: for any category C we can define the opposite category Cop just by reversing all the arrows
 Product: A product of two objects a and b is the object c equipped with two projections such that for any other object c’ equipped with two projections there is a unique morphism m from c’ to c that factorizes those projections.
 Coproduct: A coproduct of two objects a and b is the object c equipped with two injections such that for any other object c’ equipped with two injections there is a unique morphism m from c to c’ that factorizes those injections.
Examples:
 In a poset, the initial object, if it exists, is its least object. The terminal object, if it exists, is its biggest object.
 In the category of sets and functions, the initial object is the empty set. The terminal object is a singleton.
Universal constructions:

initial object

terminal object

product

coproduct

This “uniqueness up to unique isomorphism” is the important property of all universal constructions.
6) Simple Algebraic Data Types
Product Types
The canonical implementation of a product of two types in a programming language is a pair
data Pair a b = Pair a b
Records
Better than just a tuple:
data Element = Element { name :: String
, symbol :: String
, atomicNumber :: Int }
Isomorphisms:
tupleToElem :: (String, String, Int) > Element
tupleToElem (n, s, a) = Element { name = n
, symbol = s
, atomicNumber = a }
elemToTuple :: Element > (String, String, Int)
elemToTuple e = (name e, symbol e, atomicNumber e)
Sum Types
data Either a b = Left a  Right b
Algebra of types
^ Logic ^ Numbers ^ Types ^
 cpptrue
 0  haskellVoid

 cppfalse
 1  haskell()

 cppab
 a + b  haskellEither a b = Left a  Right b

 cppa&&b
 a * b  haskell(a, b) or Pair a b = Pair a b

  2 = 1 + 1  haskelldata Bool = True  False

 cppfalsea
 1 + a  haskelldata Maybe = Nothing  Just a

This analogy goes deeper, and is the basis of the CurryHoward isomorphism between logic and type theory.
7) Functors
A functor is a mapping between categories. Given two categories, C and D, a functor F maps objects in C to objects in D and also maps morphisms.
 A functor preserves the structure of a category: what’s connected in one category will be connected in the other category.
 A functor preserves composition
 A functor may smash objects together, it may glue multiple morphisms into one, but it may never break things apart.
Functor laws: fmap preserves identity and composition
Functors in programming
 Maybe functor
 List functor
 Reader functor