作者 Ivan Chien
始于 2023/03/01
分类：Category_Theory
Tags: [ PL Maths Category_Theory ]
Notes for 🐱 theory

Category Theory for Programmers

Kleisli Category

A Kleisli category is a category based on a monad:

Objects: the types of the underlying programming language
Morphisms: from type $A$ to a type derived from type $B$ using the particular embellishment
Kleisli-category-defined composition and identity morphisms

Form in Haskell:

module Main where
import Data.Char (toUpper)

type Writer a = (a, String)

(>=>) :: (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)

return :: a -> Writer a
return x = (x, "")

upCase :: String -> Writer String
upCase s = (map toUpper s, "upCase ")

toWords :: String -> Writer [String]
toWords s = (words s, "toWords ")

process :: String -> Writer [String]
process = upCase >=> toWords

main :: IO ()
main = do
    let (res, _) = process "hello world"
    print res

>=> is the composition of such a category. The Writer is the monad.

In C++:

#include <cmath>
#include <functional>
#include <iostream>
using std::sqrt;
using std::function;

template<typename A> class optional {
    bool _isValid;
    A _value;
public:
    optional() : _isValid(false) {}
    optional(A v) : _isValid(true), _value(v) {}
    bool isValid() const { return _isValid; }
    A value() const { return _value; }
};

template<typename A, typename B, typename C>
function<optional<C>(A)> compose(function<optional<B>(A)> f, function<optional<C>(B)> g) {
    return [f, g](A a) -> optional<C> {
        auto fa = f(a);
        if (!fa.isValid()) return optional<C>{};
        auto gb = g(fa.value());
        if (!gb.isValid()) return optional<C>{};
        return optional<C>{gb.value()};
    };
}

template<typename A>
optional<A> identity(A a) {
    return {a};
}

optional<double> safe_root(double x) {
    if (x >= 0) return {sqrt(x)};
    else return {};
}

optional<double> safe_reciprocal(double x) {
    if (x == 0) return {};
    else return { 1. / x };
}

auto safe_root_reciprocal = compose<double, double, double>(safe_reciprocal, safe_root);

int main() {
    auto res = safe_root_reciprocal(0.25);
    if (res.isValid()){
        std::cout << res.value() << std::endl;
    }
}

The optional is the monad.

Universal Construction

Initial Object & Terminal Object

The initial object is the object that has one and only one morphism going to any object in the category.

The initial object in a partially ordered set(a.k.a. poset) is its least element. In the category of sets and functions, the initial object is the empty set(which is corresponding to type Void in Haskell).

If there is a morphism going from $a$ to $b$, we called the $b$ is more terminal than $a$.

The terminal object is the object with one and only one morphism coming to it from any object in the category.

The uniquenss of the initial object and the terminal object is up to isomorphism.

In the poset, the terminal object is the biggest element when the biggest element exists.

Isomorphisms

An isomorphism is an invertible morphism, or a pair of morphisms, one being the inverse of the other.

Products & Coproducts

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.

A higher order function that produces the factorizing function $m$ from two candidates which sometimes called factorizer:

factorizer :: (c -> a) -> (c -> b) -> (c -> (a, b))
factorizer p q = \x -> (p x, q x)

Product types in Haskell:

type Pair = (Int, Bool)                            -- pair or tuple?
type Pair a b = Pair a b
data Element = Element { name :: String            -- record
                       , symbol :: String
                       , atomicNumber :: Int }

A coproduct is the product’s dual. 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.

In the category of sets, the product is the Cartesian product and the coproduct is the disjoint union of two sets.

The factorizer for the coproduct(which is implemented as Either in Haskell) produces the factoring function:

factorizer :: (a -> c) -> (b -> c) -> Either a b -> c
factorizer i j (Left a) = i a
factorizer i j (right b) = j b

Coproduct/sum types in Haskell:

data Either a b = Left a | Right b
data OneOfThree a b c = Sinistral a | Medial b | Dextral c

Functors

Given two categories, $\mathbf{C}$ and $\mathbf{D}$, a functor $F$ maps objects in $\mathbf{C}$ to objects in $\mathbf{D}$, and maps morphisms in $\mathbf{C}$ to morphisms in $\mathbf{D}$, and satisfies that:

\[\forall f :: a \rightarrow b, a \in Ob(\mathbf{C}), b \in Ob(\mathbf{D}) \\ F f :: f a \rightarrow f b\]

F :: a -> b

\[\forall h = g \circ f, f \in \mathbf{C}(a, b), g \in \mathbf{C}(b, c) \\ F h = F g \circ F f\]

F :: (a -> a) -> (b -> b)

\[F\mathbf{id_A} = \mathbf{id}_{Fa}\]

fmap

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

The functor laws:

fmap id = id
fmap (g . f) = fmap g . fmap f

We have to prove that fmap preserves identity and composition.

Reader Functors

fmap :: (a -> b) -> (r -> a) -> (r -> b)
fmap = (.)

Equational reasoning:

  fmap id ra
= id . ra
= ra
  
  fmap (g . f) ra
= (g . f) . ra
= g . (f . ra)
= g . (fmap f ra)
= fmap g (fmap f ra)
= (fmap g . fmap f) ra

Maybe

fmap :: (a -> b) -> Maybe a -> Maybe b
fmap _ Nothing = Nothing
fmap f (Just x) = Just $ f x

Proof:

  fmap id Nothing
= Nothing
= id Nothing

  fmap id (Just x)
= Just x
= Just (id x)

  fmap (g . f) Nothing
= Nothing
= fmap g Nothing
= fmap g (fmap f Nothing)

  fmap (g . f) (Just x)
= Just $ (g . f) x
= Just (g (f x))
= fmap g (Just (f x))
= fmap g (fmap f (Just x))

List

fmap :: (a -> b) -> List a -> List b
fmap _ [] = []
fmap f (x:xs) = Cons (f x) $ fmap f xs

Proof:

  fmap id []
= []
= id []

-- Use induction, assume that: fmap id xs = xs.
  fmap id (x:xs)
= Cons (id x) $ fmap id xs     -- induction
= Cons x xs

  fmap (g . f) []
= []
= fmap g []
= fmap g (fmap f [])

-- Use induction, assume that: fmap (g . f) xs = fmap g (fmap f xs).
  fmap (g . f) (x:xs)
= Cons ((g . f) x) $ fmap (g . f) xs
= Cons (g (f x)) $ fmap (g . f) xs       -- induction
= Cons (g (f x)) $ (fmap g (fmap f xs))
= fmap g (Cons (f x) $ fmap f xs))
= fmap g (fmap f (x:xs))

Functor Composition

composeMaybeList :: ((a -> b) -> List a -> List b) -> ((List a -> List b) -> Maybe List a -> Maybe List b) -> (a -> b) -> Maybe List a -> Maybe List b
composeMaybeList = (.)

Bifunctors

import Data.Bifunctor (Bifunctor)
class MyBifunctor f where
    bimap :: (a -> c) -> (b -> d) -> f a b -> f c d
    bimap g h = first g . second h
    first :: (a -> c) -> f a b -> f c b
    first g = bimap g id
    second :: (b -> d) -> f a b -> f a d
    second = bimap id

Functorial ADTs

newtype BiComp bf fu gu a b = BiComp (bf (fu a) (gu b))

instance (MyBifunctor bf, Functor fu, Functor gu) =>
    MyBifunctor (BiComp bf fu gu) where
        bimap f1 f2 (BiComp x) = BiComp (bimap (fmap f1) (fmap f2) x)

f1 :: a -> fu a
fmap f1 :: fu a -> fu c
f2 :: a -> gu a
fmap f2 :: gu b -> gu d
bimap :: (fu a -> fu c) -> (gu b -> gu d) -> bf (fu a) (gu b) -> bf (fu c) (gu d)

Kleisli Category (Writer Functor)

type Writer a = (a, String)

(>=>) :: (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)

myReturn :: a -> Writer a
myReturn x = (x, "")

instance Functor (Writer a) where
    fmap :: (a -> b) -> Writer a -> Writer b
    fmap f = id >=> (\x -> return (f x))
		-- fmap f = id >=> (myReturn . f)

id :: Writer a -> Writer a
myReturn . f :: a -> Writer b
f :: a -> b

Covariant and Contravariant Functor

type Reader r a = r -> a

instance Functor (Reader r) where
    fmap f g = f . g

For every category $\mathbf{C}$ there is a dual category $\mathbf{C}^{op}$. It’s a category with the same objects as $\mathbf{C}$, but with all the arrows reversed.

Consider a functor that goes between $\mathbf{C}^{op}$ and some other category $\mathbf{D}$:

\[F :: \mathbf{C}^{op} \rightarrow \mathbf{D}\]

Such a functor maps a morphism $f^{op} :: a \rightarrow b$ in $\mathbf{C}^{op}$ to the morphism $Ff^{op} :: Fa \rightarrow Fb$ in $\mathbf{D}$. But the morphism $f^{op}$ secretly corresponds to some morphism $f :: b \rightarrow a$ in the original category $\mathbf{C}$.

Consider a $G$ which is not a functor:

it maps objects the same way $F$ does
when it comes to mapping morphisms, it reverses them

then:

\[Gf :: (b \rightarrow a) \rightarrow (Ga \rightarrow Gb)\]

When it is a functor, it is called a contravariant functor.

The regular functor is called a covariant functor.

type Op r a = a -> r

class Contravariant f where
    contramap :: (b -> a) -> (f a -> f b)

instance Contravariant (Op r) where
    contramap f g = g . f

Is Pair a Bifunctor?

data Pair a b = Pair a b
instance Bifunctor Pair where
    bimap f g (Pair a b) = Pair (f a) (g b)
    first f (Pair a b) = Pair (f a) b
    second g (Pair a b) = Pair a (g b)

Proof:

  bimap g h (Pair a b)
= Pair (g a) (h b)
= bimap g id (Pair a (h b))
= first g (Pair a (h b))
= first g (bimap id h (Pair a b))
= first g (second h (Pair a b))
= (first a . second h) (Pair a b)

  first g id (Pair a b)
= Pair (g a) b
= bimap g id (Pair a b)

  second id h (Pair a b)
= Pair a (h b)
= bimap id h (Pair a b)

Proof Isomorphism of Maybe and Maybe’

import Data.Functor.Identity

newtype Const c a = Const c
type Maybe' a = Either (Const () a) (Identity a)

maybe'2Maybe :: Maybe' a -> Maybe a
maybe'2Maybe (Left (Const _)) = Nothing
maybe'2Maybe (Right (Identity a)) = Just a

maybe2Maybe' :: Maybe a -> Maybe' a
maybe2Maybe' (Just a) = Right $ Identity a
maybe2Maybe' Nothing = Left $ Const ()

Proof:

   proof. maybe'2Maybe . maybe2Maybe' = id
1. maybe'2Maybe . maybe2Maybe' (Just a)
 = maybe'2Maybe (maybe2Maybe' (Just a))
 = maybe'2Maybe (Right (Identity a))
 = (Just a)
2. maybe'2Maybe . maybe2Maybe' Nothing
 = maybe'2Maybe (maybe2Maybe' Nothing)
 = maybe'2Maybe (Left (Const ()))
 = Nothing
   
   proof. maybe2Maybe' . maybe'2Maybe = id
1. maybe2Maybe' . maybe'2Maybe (Left (Const ()))
 = maybe2Maybe' (maybe'2Maybe (Left (Const ())))
 = maybe2Maybe' Nothing
 = Left $ Const ()
2. maybe2Maybe' . maybe'2Maybe (Right (Identity a))
 = maybe2Maybe' (maybe'2Maybe (Right (Identity a)))
 = maybe2Maybe' (Just a)
 = Right $ Identity a
 
\qed

Proof PreList is a Bifunctor

data PreList a b = Nil | Cons a b

instance MyBifunctor PreList where
    bimap _ _ Nil = Nil
    bimap f g (Cons a b) = Cons (f a) (g b)
    first _ Nil = Nil
    first f (Cons a b) =  Cons (f a) b
    second _ Nil = Nil
    second g (Cons a b) = Cons a (g b)

Then proof that Nil and Cons a b are functors to qed, because the composition of a bifunctor and functors is a bifunctor.

Proof:

def. instance (Functor b) => Functor (PreList a) where
         fmap f Nil = Nil
         fmap f (Cons a b) = Cons a (fmap f b)

proof. Nil is a functor
  fmap id Nil
= Nil
= id Nil

  fmap (g . f) Nil
= Nil
= fmap g Nil
= fmap g (fmap f Nil)
= (fmap g . fmap f) Nil

proof. Cons a b is a functor when a is fixed:
  fmap id (Cons a b)
= Cons a (fmap id b)
= Cons a (id b)
= Cons a b
= id (Cons a b)

  fmap (g . f) (Cons a b)
= Cons a (fmap (g . f) b))
= Cons a (g . f b)
= Cons a (fmap g (f b))
= Cons a (fmap g (fmap f b))
= fmap g (Cons a (fmap f b))
= fmap g (fmap f (Cons a b))
= (fmap g . fmap f) (Cons a b)

\qed

⇦ ⇨