Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Notes on Bartosz Milewski' Category Theory for Programmers https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/

Category: The Essence of Composition

Roughly, category theory is a general mathematical theory of structures and of systems of structures [1]. Generally, is best represented with Objects and Arrows that go between them.

A -> B -> C
A -> C

If there is an arrow from object A to object B, and another arrow from B to C, then there must be an arrow from A to C. Hence, Milewski argues that the essence of a category is composition, or rather, the essence of composition is a category.

Arrow as Functions

In previous example, let's say that a function f takes an argument of type A and returns type of B and a function g that takes type B and returns a type C, we can compose those two functions by passing the output of f as the input of g. Hence, we have created a new function that takes an A and returns a C. In mathematical notation this composition is denoted with a circle ∘.

g ∘ f

The order of composition is right to left, hence in mathematic it is usually called "g after f".

Arrow is also called as morphism.

Properties of Composition

  1. Associativity Composition is associative

    h∘(g∘f) = (h∘g)∘f = h∘g∘f
    
  2. Identity

    For every object A there is an arrow which is a unit of composition. This arrow loops from the object to itself Being a unit of composition means that, when composed with any arrow that either starts at A or ends at A, respectively, it gives back the same arrow. The unit arrow for object A is called idA (identity on A). In math notation, if f goes from A to B then

    f∘idA = f
    idB∘f = f
    

    Note that identity is a function, hence, it is composable.

Types and Functions

The theme for this chapter is types are about composability. To be composable, the output of the source function's type has to be the same with the next's input type: A -> B -> C. The stronger the type of a language, the better this match can be describe and be mechanically verified.

In a simple term, types are sets of values. Bool is a set of two values True and False. Char is a set of all Unicodes characters like t and u.

Milewski argues that in an ideal world, Haskell types are sets and functions are mathematical functions between sets. Hence, we can have mathematical model for our program. However, in a real world, it is difficult to describe a programming language formally using its semantics. Fortunately, there is an alternative called denotational semantics [[2]][[3]] that is based on math.

In denotational semantics every programing construct is given its mathematical interpretation. With that, if you want to prove a property of a program, you just prove a mathematical theorem.

One of the important advantages of having a mathematical model for programming is that it’s possible to perform formal proofs of correctness of software

In programming languages, functions that always produce the same result given the same input and have no side effects are called pure functions. In a pure functional language like Haskell all functions are pure. Because of that, it’s easier to give these languages denotational semantics and model them using category theory. As for other languages, it’s always possible to restrict yourself to a pure subset, or reason about side effects separately. Later we’ll see how monads let us model all kinds of effects using only pure functions.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.