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
Logic | Numbers | Types (haskell) |
---|---|---|
true | 0 | Void |
false | 1 | () |
`a | b` | a + b |
a && b | a * b | (a, b) or Pair a b = Pair a b |
2 = 1 + 1 | `data Bool = True | |
`false | a` | 1 + a |
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"