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.
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.
-
Associativity Composition is associative
h∘(g∘f) = (h∘g)∘f = h∘g∘f -
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 = fNote that identity is a function, hence, it is composable.
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.