Category Theory & Haskell programming language

• https://www.seas.upenn.edu/~cis194/spring15/lectures.html
• https://wiki.haskell.org/Learning_Haskell
• http://yogsototh.github.io/Category-Theory-Presentation
• https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/

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 lower-case

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
• a 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
• Hom-Set: In Category C, Set of morphisms a → b = HomC(a,b)

Orders:

• Preorder: Set + order relation (Hom-Set 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 hom-set 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 is 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 programming-language 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

This analogy goes deeper, and is the basis of the Curry-Howard 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.
• preserves composition
• 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

Definition in Haskell:

class Functor f where
  fmap :: (a -> b) -> f a -> f b

• Maybe functor

data Maybe a = Nothing | Just a
instance Functor Maybe where
  fmap _ Nothing = Nothing
  fmap f ( Just x) = Just (f x)

• List functor

data List a = Nil | Cons a ( List a)
instance Functor List where
  fmap _ Nil = Nil
  fmap f ( Cons x t) = Cons (f x) (fmap f t)

• Reader functor

( -> ) a b
instance Functor (( -> ) r) where
  fmap f g = f . g

• Const c functor (ignores its type parameter)

data Const c a = Const c
instance Functor ( Const c) where
  fmap _ ( Const v) = Const v

Composition

Factors between categories compose like functions between sets compose. Endofunctors are particularly "composition-friendly"

8) Functoriality

9) Function Types

10) Natural Transformations

Part Two

1) Declarative Programming

2) Limits and Colimits

3) Free Monoids

4) Representable Functors

5) The Yoneda Lemma

6) Yoneda Embedding

Part Three

1) It’s All About Morphisms

2) Adjunctions

3) Free/Forgetful Adjunctions

4) Monads: Programmer’s Definition

5) Monads and Effects

6) Monads Categorically

7) Comonads

8) F-Algebras

9) Algebras for Monads

10) Ends and Coends

11) Kan Extensions

12) Enriched Categories

13) Topoi

14) Lawvere Theories

15) Monads, Monoids, and Categories