📖Category Theory for Programmers

Milewski, Bartosz

1.1 Motivation and Philosophy

Category Theory 1.1: Motivation and Philosophy

  • Curry–Howard–Lambek correspondence

    • Computation–Logic–Category theory are isomorphic

  • OOP is bad for concurrent programming because OOP hides data mutation and sharing (pointers). Mixing sharing and mutation is data race.

    • this makes objects non-composable

    • locks do not compose either

  • Template metaprogramming in C++ draws many ideas from Haskell. So you translate Haskell ideas into ugly C++ metaprogramming language.

    • Haskell draws many ideas from Category Theory. So you translate concise Category Theory ideas into ugly Haskell language.

  • Category Theory unifies different branches of mathematics: type theory, logic, algebra, etc.

    • Mathematics get philosophical: do mathematicians invent things or discover truth?

  • It might be that composition and this universal structure is not the property of the universe, but the property of human minds.

    • It might be that humans evolved to work with abstraction and composition, and we don’t understand what we can’t explore using these tools.

    • In that sense, Category Theory might be about human minds really and be closer to epistemology.

1.2 What is a category?

Category Theory 1.2: What is a category?

7.1: Functoriality, bifunctors

  • Functors consist of functions and functions compose, so we can compose functors

  • Identity functor is trivial

  • Cat = Category of functors

    • Objects are categories

    • Morphisms are functors

    • It’s a category of small categories. For large categories, we need a more powerful mechanisms

  • (Now, Haskell does not really allow composition of functors. If you have a Maybe [Int] (composition of two functors: Maybe and []), you have to use two fmaps instead of one.)

  • all algebraic data types are automatically functorial

  • bifunctor — is a functor from a product category (C×D → E)

    • sum type is bifunctor as well

7.2: Monoidal Categories, Functoriality of ADTs, Profunctors

  • (cartesian) product (operator) + terminal object (Void) (a unit) is a monoidal category

    • terminal object is a unit of product

  • by the same token, coproduct + initial object is a monoidal category

  • a monoidal category (or tensor category)

    • a bifunctor: :C×CC\otimes: C \times C \to C called a tensor product

      • (e.g., product or coproduct)

    • an object II or 11 called the unit object or identity object.

  • Contravariant functor — is a functor defined on the opposite category (cofunctor? no)

    • haskelly-speaking

      class Contravariant f where
        contramap :: (a -> b) -> f b -> f a
        -- must satisfy:
        -- contramap id = id
        -- contramap f . contramap g = contramap (g . f)
    • (Strictly speaking, “cofunctor” is not the right name as the dual of a functor is a functor)

    • you can think of Contravariant as an opposite of container. it does not contain As, but it requires As

  • function

    • (->) a b is Contravariant in a and Covariant in b

    • Cop×CCC^{op} \times C \to C

      • that is called a Profunctor

    • haskell

      class Profunctor p where
        dimap :: (a' -> a) -> (b -> b') -> p a b -> p a' b'
      instance Profunctor (->) where
        -- dimap :: (a' -> a) -> (b -> b') -> (a -> b) -> (a' -> b')
        dimap f g h = g . h . f
    • (how does that definition match to the Profunctor definition on wikipedia or nLab? ϕ:CDϕ:Dop×CSet\phi: C \nrightarrow D \equiv \phi: D^{op}\times{}C \to Set)

8.1: Function objects, exponentials

  • hom-set between two objects (if it’s a set), can be represented as an object in the same category

    • “internal hom-set”

  • function objects:

    • pattern

      • z is a function, a is an argument type, b—result type

      • the category must have products

    • universal construction

      • \varab is a function object    z,!h:z(ab)g=\vareval(h×id)\var{a \Rightarrow b} \text{ is a function object} \iff \forall z, \exists! h: z \to (a \Rightarrow b) \ni g = \var{eval} \circ (h \times id)

        • (this relies on that a morphism between two products can be constructed as a product of two morphisms (hh and idid here), and we know that that is a correct way to obtain (ab)×a(a \Rightarrow b) \times a from z×az \times a using h:z(ab)h: z \to (a \Rightarrow b))

      • in haskell, the next two are equivalent

        h :: z -> (a -> b)
        g :: (z, a) -> b


        curry :: ((a, b) -> c) -> (a -> (b -> c))
        curry f = \a -> \b -> f (a, b)
        uncurry :: (a -> (b -> c)) -> ((a, b) -> c)
        uncurry f = \(a, b) -> f a b
  • exponentials

    • abbaa \Rightarrow b \equiv b^a

    • e.g., BoolInt(Int,Int)Int×IntInt2IntBoolBool \to Int \equiv (Int, Int) \equiv Int \times Int \equiv Int^2 \equiv Int^{Bool}

      • 1=()1 = ()

      • 2=Bool2 = Bool

    • cartesian closed category (CCC)

      • cartesian — has products

      • closed — has all exponentials a,b,ab\forall{}a,b, \exists{}a^b

        • A category CC is closed if for any pair a,ba,b of objects the collection of morphisms from aa to bb can be regarded as forming itself an object of CC.

      • has a terminal object (0th power of an object)

    • Bicartesian closed category (BCCC)

      • has products, co-products, exponentials, and initial and terminal objects

      • bicartesian = both cartesian and cocartesian

    • a0=1    Voida()a^0 = 1 \implies Void \to a \sim () (absurd)

    • 1a=1    a()()1^a = 1 \implies a \to () \sim ()

    • a1=a    ()aaa^1 = a \implies () \to a \sim a

8.2 Type algebra, Curry-Howard-Lambek isomorphism

  • ab+c=ab×aca^{b+c} = a^b \times a^c