<commit_before>* Category Theory for Programmers

** Definitions

*** Category

A category consists of objects and arrows (morphisms). Arrows can be composed,
and the composition is associative. Every object has an identity arrow that serves
as a unit under composition.

*** Bottom as a representation of non-terminating computation

We can't just ban non-terminating functions because distinguishing between
terminating and non-terminating functions is undecidable - the famous halting
problem.

That's why computer scientists came up with an idea, to extend every type
by one more special value called the bottom (denoted by _|_ in Haskell).

This *value* corresponds to a non-terminating computation. In practice, when
proving correctness of the program, it is easier to drop out Bottom and
treat all functions as always terminating.

*** Denotational Semantics

Testing is a poor substitution of proof.

Consider following Haskell program, which calculates factorial:

fact n = product [1..n]

It has straightforward definition, which is nice and clean, almost equal
with the math book. 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.

However considering more pragmatic and actual problems (which are more
related with programming than with math) usage of *denotational semantics*
is much more harder.

The breakthrough came from category theory. <NAME> discovered that
any computational effect can be mapped to monads.

*** Monoid

A monoid is defined as a set with a binary operation. All that’s required
from this operation is that it’s associative, and that there is one special
element that behaves like a unit with respect to it.

In Haskell we would define a Monoid like this:

class Monoid m where
  mempty  :: m
  mappend :: m -> m -> m

You have to make sure that two properties are enforced - a neutrality of
`mempty` element and that `mappend` is associative. Commutativity is not
part of the definition so thanks to that a `String` or `Array` can be a
Monoid.

*** Kleisli Categories

Kleisli category has, as objects, the types of the underlying programming
language. Morphisms from type A to type B are functions that go from A to
a type derived from B using the particular embellishment. Each Kleisli
category defines its own way of composing such morphisms, as well as the
identity morphisms with respect to that composition.

*** Products and Coproducts

Every object is defined by its relationships - with itself and with 
the other objects. These relationships are defined by morphisms.

The initial object is the object that has one and only one morphism 
going to any object in the category. It guarantees the next best 
thing: uniqueness up to isomorphism.

Example: The initial object in a partially ordered set (often 
called a poset) is its least element. Some posets don’t have an 
initial object — like the set of all integers, positive and negative.

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

The terminal object is unique, up to isomorphism. In the category 
of sets, the terminal object is a singleton.

You can’t help but to notice the symmetry between the way we defined 
the initial object and the terminal object. The only difference 
between the two was the direction of morphisms. It turns out that for 
any category C we can define the opposite category C^op just by 
reversing all the arrows. The opposite category automatically 
satisfies all the requirements of a category, as long as 
we simultaneously redefine composition.

It follows then that a terminal object is the initial object in 
the opposite category.

**** Isomorphism

The intuition is that isomorphic objects look the same — they have 
the same shape. An isomorphism is an invertible morphism, or a pair 
of morphisms, one being the inverse of the other.

Morphism g is the inverse of morphism f if their composition is 
the identity morphism:

f . g = id
g . f = id

**** Products and Coproducts - Definitions

Let's define a product of two objects in any category using the 
same universal construction. Such product doesn’t always exist, 
but when it does, it is unique up to a unique isomorphism.

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 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 coproduct is the disjoint union of 
two sets. An element of the disjoint union of a and b is 
either an element of a or an element of b.

The canonical implementation of the coproduct is a data type 
called Either, which is defined in the standard Prelude as:

Either a b = Left a | Right b

A product behaves like multiplication, with the terminal object 
playing the role of one; whereas coproduct behaves more like 
the sum, with the initial object playing the role of zero. In 
particular, for finite sets, the size of the product is the 
product of the sizes of individual sets, and the size of the 
coproduct is the sum of the sizes.
<commit_msg>Notes from 'Category Theory for Programmers'.<commit_after>* Category Theory for Programmers

** Definitions

*** Category

A category consists of objects and arrows (morphisms). Arrows can be composed,
and the composition is associative. Every object has an identity arrow that serves
as a unit under composition.

*** Bottom as a representation of non-terminating computation

We can't just ban non-terminating functions because distinguishing between
terminating and non-terminating functions is undecidable - the famous halting
problem.

That's why computer scientists came up with an idea, to extend every type
by one more special value called the bottom (denoted by _|_ in Haskell).

This *value* corresponds to a non-terminating computation. In practice, when
proving correctness of the program, it is easier to drop out Bottom and
treat all functions as always terminating.

*** Denotational Semantics

Testing is a poor substitution of proof.

Consider following Haskell program, which calculates factorial:

fact n = product [1..n]

It has straightforward definition, which is nice and clean, almost equal
with the math book. 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.

However considering more pragmatic and actual problems (which are more
related with programming than with math) usage of *denotational semantics*
is much more harder.

The breakthrough came from category theory. <NAME> discovered that
any computational effect can be mapped to monads.

*** Monoid

A monoid is defined as a set with a binary operation. All that’s required
from this operation is that it’s associative, and that there is one special
element that behaves like a unit with respect to it.

In Haskell we would define a Monoid like this:

class Monoid m where
  mempty  :: m
  mappend :: m -> m -> m

You have to make sure that two properties are enforced - a neutrality of
`mempty` element and that `mappend` is associative. Commutativity is not
part of the definition so thanks to that a `String` or `Array` can be a
Monoid.

*** Kleisli Categories

Kleisli category has, as objects, the types of the underlying programming
language. Morphisms from type A to type B are functions that go from A to
a type derived from B using the particular embellishment. Each Kleisli
category defines its own way of composing such morphisms, as well as the
identity morphisms with respect to that composition.

*** Products and Coproducts

Every object is defined by its relationships - with itself and with 
the other objects. These relationships are defined by morphisms.

The initial object is the object that has one and only one morphism 
going to any object in the category. It guarantees the next best 
thing: uniqueness up to isomorphism.

Example: The initial object in a partially ordered set (often 
called a poset) is its least element. Some posets don’t have an 
initial object — like the set of all integers, positive and negative.

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

The terminal object is unique, up to isomorphism. In the category 
of sets, the terminal object is a singleton.

You can’t help but to notice the symmetry between the way we defined 
the initial object and the terminal object. The only difference 
between the two was the direction of morphisms. It turns out that for 
any category C we can define the opposite category C^op just by 
reversing all the arrows. The opposite category automatically 
satisfies all the requirements of a category, as long as 
we simultaneously redefine composition.

It follows then that a terminal object is the initial object in 
the opposite category.

**** Isomorphism

The intuition is that isomorphic objects look the same — they have 
the same shape. An isomorphism is an invertible morphism, or a pair 
of morphisms, one being the inverse of the other.

Morphism g is the inverse of morphism f if their composition is 
the identity morphism:

f . g = id
g . f = id

**** Products and Coproducts - Definitions

Let's define a product of two objects in any category using the 
same universal construction. Such product doesn’t always exist, 
but when it does, it is unique up to a unique isomorphism.

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 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 coproduct is the disjoint union of 
two sets. An element of the disjoint union of a and b is 
either an element of a or an element of b.

The canonical implementation of the coproduct is a data type 
called Either, which is defined in the standard Prelude as:

Either a b = Left a | Right b

A product behaves like multiplication, with the terminal object 
playing the role of one; whereas coproduct behaves more like 
the sum, with the initial object playing the role of zero. In 
particular, for finite sets, the size of the product is the 
product of the sizes of individual sets, and the size of the 
coproduct is the sum of the sizes.

*** Simple Algebraic Data Types

A lot of mechanisms can be built with use of basic types - products and coproducts.
This fact has important practical consequences. Many properties of data structures 
are composable - if you know how to compare values of basic types for equality, and 
you know how to generalize these comparisons to product / coproduct types you can 
automate the derivation of equality operators for composite types.

We have sum types with 'Void' as the neutral element, and the product types with
the unit type, '()' as the neutral element. We'd like to think of them as 
analogous to addition and multiplation. Using them separately can be used 
to define a variety of useful data structures, but the real power comes
from combining the two.

Mathematicians have a name for two intertwined monoids: it’s called a semiring. 
It’s not a full ring, because we can’t define subtraction of types.

Sample translation table with some entries of interest:

| Numbers   | Types                             |
|-----------+-----------------------------------|
| 0         | Void                              |
| 1         | ()                                |
| a + b     | Either a b = Left a \vert Right b |
| a * b     | (a, b) or Pair a b = Pair a b     |
| 2 = 1 + 1 | data Bool = True \vert False      |
| 1 + a     | data Maybe = Nothing \vert Just a |

Logical and and or also form a semiring, and it too can be mapped into type theory:

| Logic          | Types                             |
|----------------+-----------------------------------|
| false          | Void                              |
| true           | ()                                |
| a \vert\vert b | Either a b = Left a \vert Right b |
| a && b         | (a, b)                            | 
  
{'fraction_non_alphanumeric': 0.04372742973779243, 'fraction_numerical': 0.0006280420788192808, 'mean_word_length': 3.544773457010346, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 9, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 8, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4115455', 'n_tokens_mistral': 3232, 'n_tokens_neox': 3041, 'n_words': 2010}