Structure Preserving Maps

Universal Algebra

Algebraic Data Types

(not in final form)

Part 2 of a short course on monads.

In the previous lecture, we discussed monoids as a paradigmatic example of an algebraic structure. The importance of paradigmatic examples is that they can be generalised in different ways. One important way to generalise monoids is to say that a monoid is made from operations and equations: Operations for neutral element (empty word) and mutiplication (concatenation) and equations for identity and associativity.

To capture more diverse structures, we should generalise to other kind of operations and equations. The area of mathematics that studies mathematical objects defined by operations and equations is known as Universal Algebra, or also General Algebra. The objects of study are called algebras.

An important application of algebra to programming are algebraic data types. We have seen examples in the previous lecture and will see more in this one.

In the lecture we went trough the Example, the Axioms, some More Examples and then discussed the program algebraic-data-types. At the beginning of the next lecture I explained the notion of termalgebra and that it makes mathematically precise on what domain we do induction when we program with algebraic data types. Finally, I briefly touched upon the remainig points made in these notes.

Programs: induction, algebraic-data-types, magma.

Example

The clock is a function

(We make various assumptions here such as that time can be measured in discrete units, stretches from negative infinity to infinity.)

A clock that is neither fast nor slow has the additional property of preserving the structure of time. We can model this mathematically, by equipping

$\mathbb{Z}$ with the structure

$(\mathbb{Z},0,+)$ of addition. Similarly, we introduce the notation of

$\mathbb{Z}/12\mathbb{Z}$ for the set

$\{0,\dots 11\}$ with addition as on the clock.

That the clock is preserving the structure of addition can now be expressed by saying that diagram

commutes. Algebraically, this is just an equation

$$clock(x+1)=clock(x)+1$$

where

$+1$ on the left refers to integer addition and

$+1$ on the right refers to addition modulo 12. Moreover, it seems reasonable to require

$$clock(0)=0$$

Let us call, just for the purposes of this example, a function that satisfies these equations a proper clock.

If we put these equations into words we can say that "one unit of time advances the clock by one unit". So the following should be more or less obvious, but one can also prove it by induction.

Exercise: There infinitely many functions

$\mathbb{Z}\to \mathbb{Z}/12$, but there is only one function satisfying the equations above. ^[1]

In many programming and mathematical problems, to determine the relevant structure can be a big step towards a solution. Even in the example of the clock, we can think of different structure that we may want to preserve.

For example, both

$\mathbb{Z}$ and

$\mathbb{Z}/12\mathbb{Z}$ are monoids under addition. So we could ask, in addition to

$clock(0)=0$, for the following diagram to commute.

Algebraically, that would be written as

$$clock(x+y)=clock(x)+clock(y)$$

The purpose of the exercise is to show that this defines a more permissive notion of structure preserving map. But let us first pause and recognise that we just met what is known as a monoid homomorphism. ^[2]

Definition: Let

$(M,e,\cdot )$ and

$(M^{\prime },e^{\prime },\ast )$ be two monoids. Then

$f:M\to M^{\prime }$ is a monoid homomorphism if

$$\begin{array}{c}f(e)=f(e^{\prime })\\ f(x\cdot y)=f(x)\ast f(y)\end{array}$$

Exercise: Find the 5 different monoid homomorphisms

$(\mathbb{Z},0,+)\to (\mathbb{Z}/12\mathbb{Z},0,+)$. ^[3]

We have introduced monoids as a paradigmatic example of an algebra. The importance of paradigmatic example is that they can be generalised in various different ways. A monoid is made from operations and equations: Operations for neutral element (empty word) and mutiplication (concatenation) and equations for identity and associativity.

The area of mathematics that studies mathematical objects defined by operations and equations is known as Universal Algebra, or also General Algebra. The objects of study are then just called algebras. This is what we will look at next.

Axioms: Universal Algebra

(essential)

The purpose of this section is to generalise the previous example to algebraic structures defined by arbitrary operations.

First, let us go back to automata-as-algebras, the introductory example of the first lecture. As we have seen, we can think of the alphabet

$\mathrm{\Sigma }$ as a set of unary operation symbols. An automaton interprets each input symbol as a function

$Q\to Q$. In other words, automata can be seen as algebras of unary operations. We now generalise this to operations which can take any number of arguments.

Definition: A signature is a set

$\mathrm{\Sigma }$ of operation symbols together with a function

$\mathsf{a}\mathsf{r}\mathsf{i}\mathsf{t}\mathsf{y}\mathsf{:}\mathsf{\Sigma }\to \mathbb{N}$.

Example: The signature of

• monoids is

  $\mathrm{\Sigma }=\{e,\cdot \}$ and
  $\mathsf{a}\mathsf{r}\mathsf{i}\mathsf{t}\mathsf{y}(e)=0$ and
  $\mathsf{a}\mathsf{r}\mathsf{i}\mathsf{t}\mathsf{y}(\cdot )=2$.

• lists is

  $$\mathrm{\Sigma }=\{\mathtt{N}\mathtt{i}\mathtt{l}\}\cup \{\mathtt{C}\mathtt{o}\mathtt{n}\mathtt{s}\mathtt{x}\mid \mathtt{x}\in \mathtt{a}\}$$

  where

  $\{\mathtt{N}\mathtt{i}\mathtt{l}\}$ is a constant (arity
  $0$) and the
  $\mathtt{C}\mathtt{o}\mathtt{n}\mathtt{s}\mathtt{x}$ are unary (arity
  $1$).

Remark: Once we have a signature we can form terms from operation symbols and variables.

Example: In the signature of

• monoids we have terms such as
  $e\cdot x$ and
  $x\cdot (y\cdot z)$.
• lists terms are lists.

Remark: An equation is a pair of terms.

Definition: An algebra for a signature

$\mathrm{\Sigma }$, or a

$\mathrm{\Sigma }$-algebra, consists of a set

$A$ together with an

$n$-ary function (=operation)

$A^n\to A$ for each

$n$-ary operation symbol of

$\mathrm{\Sigma }$.

We will see many examples of algebras and structure preserving maps (homomorphisms) in the next section. But first another definition.

Definition: Let

$\mathrm{\Sigma }$ be a signature,

$A$ and

$B$ two algebras and

$f:A\to B$ a function between between their underlying sets.

$f$ is called a homomorphism, if for all operations

$\sigma$ of arity

$n$, we have

$$f({\sigma }^A(x_1,\dots x_n)={\sigma }^B(f(x_1),\dots f(x_n))$$

where

${\sigma }^A$ is the interpretation of

$\sigma$ on

$A$ and

${\sigma }^B$ is the interpretation of

$\sigma$ on

$B$.

Definition:

$f:A\to B$ is an isomorphism if

$f$ has an inverse, that is, if there is a homomorphism

$g:B\to A$ such that

$g\circ f=id$ and

$f\circ g=id$.

Remark:

$f$ is an isomorphism iff

$f$ is a bijective homomorphism.

Remark on many-sorted universal algebra: For programming applications of universal algebra we want "heterogeneous" or "many-sorted" universal algebra. Indeed, we need algebras that do not have only on "carrier"

$A$ but a family

$(A_1,A_2,\dots )$ of carrier sets (or sorts or types). For example, the signature of the length function involves two sorts (types) and the signature of the member function three:

len :: List a -> Integer
member :: a -> List a -> Bool

Some mathematics texts go the extra mile and extend universal algebra to this more general setting. But all the maths we need can be more easily explained in the one-sorted setting. As a rule of thumb, all results extend to the many-sorted setting, so we are free to apply them to programming with many types.

More Examples: Induction

(essential)

The examples of this section explore the following important ideas.

• The notion of free monoid generalises to algebras for arbitray signatures.
• Free algebras come with a principle of induction that can be used for reasoning and computation.
• Free algebras are unique up to isomorphism.

Again, all of our inductive definitions are implemented in Haskell for you to experiment with in induction.

Natural Numbers via Zero and Successor

Choose the signature

$\mathrm{\Sigma }=\{\mathrm{O},\mathrm{S}\}$ with

$\mathrm{a}\mathrm{r}\mathrm{i}\mathrm{t}\mathrm{y}(\mathrm{O})=0$ and

$\mathrm{a}\mathrm{r}\mathrm{i}\mathrm{t}\mathrm{y}(\mathrm{S})=1$, that is,

$\mathrm{O}$ is a constant and S is a unary operation symbol.

The so-called

$\mathrm{\Sigma }$-termalgebra, or intial algebra (see next section for more on termalgebras, initial algebras and free algebras) consists of all terms one can form from the operations of the signature:

$\mathrm{O}$,

$\mathrm{S}\mathrm{O}$,

$\mathrm{S}\mathrm{S}\mathrm{O}$, etc. The operation

$\mathrm{S}$ takes a term

$\mathrm{S}\dots \mathrm{O}$ to

$\mathrm{S}\mathrm{S}\dots \mathrm{O}$. In Haskell, this intial algebra can be defined as

data NN = O | S NN

Maths Exercise: Show that the natural numbers

$\mathbb{N}$ with 0 and

$+1$ are isomorphic to the

$\mathrm{\Sigma }$-termalgebra.

Answer. ^[4]

Induction on natural numbers: The principle of definition by induction goes as follows. For any

$i\in \mathbb{N}$ and

$s:\mathbb{N}\to \mathbb{N}$ there is a unique funtion

$f:\mathbb{N}\to \mathbb{N}$

$$\begin{array}{rl}f(0)& =i\\ f(n+1)& =s(f(n))\end{array}$$

Maths Exercise: More generally, for any

$\mathrm{\Sigma }$-algebra

$(A,\mathrm{O},\mathrm{S})$, there is a unique

$\mathrm{\Sigma }$-homomorphism

$f:\mathbb{N}\to A$ defined by the same two equations above.

Answer. ^[5]

In pseudo Haskell, we can define this induction principle as (see also the code in induction)

induction :: a -> (a -> a) -> (Integer -> a)
induction i s 0 = i
induction i s (n+1) = s (induction i s n)

Note how lines 2 and 3 are exactly the same as the two equations above if we identify

$f$ with induction i s.

Natural Numbers as a Free Monoid

This example shows that we get a different induction principle for the natural numbers if we change the signature.

Maths Exercise: The natural numbers

$(\mathbb{N},0,+)$ are isomorphic to the free monoid over

$\mathrm{\Sigma }=\{s\}$.

Answer. ^[6]

The induction principle: For any monoid

$(M,e,\cdot )$ and any

$m\in M$ there is a unique monoid morphism

$f:\mathbb{N}\to M$ satisfying

$$\begin{array}{c}f(0)=e\\ f(n+1)=m\cdot f(n)\end{array}$$

$f(n)$ is more commonly written as

$m^n$. What the inductive definition explains is why this notation not only makes sense for numbers but generalises to any monoid.

Maths Exercise: Prove the uniqueness of

$f$.

Answer. ^[7]

In pseudo Haskell, the induction principle can be defined as (see also the code in induction)

induction2 :: m -> (m->m->m) -> m -> Int -> m
induction2 e mult m 0 = e
induction2 e mult m (n+1) = mult m (induction2 e mult m n)

Again, identifying

$f$ in the two equations above with induction2 e mult m we have a perfect match between code and maths.

Exercise: Adapt the definitions above to the situation where one does not have a neutral element. ^[8]

Induction over Words/Lists

Words (= lists) are algebras for two different signatures. First, we have the signature where each letter is a unary operation. Second, we have the signature of monoids. Induction over words usually refers to the first signature. Let us review an example.

If we write

data List a = Nil | Cons a (List a)

we define List a as a particular algebra (in fact the initial algebra or termalgebra, see below) for the signature ^[9]

$$\mathrm{\Sigma }=\{\mathtt{N}\mathtt{i}\mathtt{l}\}\cup \{\mathtt{C}\mathtt{o}\mathtt{n}\mathtt{s}\mathtt{x}\mid \mathtt{x}\in \mathtt{a}\}$$

where

$\{\mathtt{N}\mathtt{i}\mathtt{l}\}$ is a constant (arity

$0$) and the

$\mathtt{C}\mathtt{o}\mathtt{n}\mathtt{s}\mathtt{x}$ are unary (arity

$1$). When we define length of a list via

len :: List a -> Integer
len Nil = 0
len (Cons x xs) = 1 + len xs

we define len as a structure preserving map, in fact a

$\mathrm{\Sigma }$-algebra homomorphism.

Exercise: For which algebraic structure on Integer is len a

$\mathrm{\Sigma }$-algebra homomorphism?

Answer. ^[10]

We used the following induction principle to extend the transition function of an automaton from letters to words.

Let

$(M,e,\cdot )$ be a monoid. Any function

$f:\mathrm{\Sigma }\to M$ has a unique extension

$f^{\mathrm{♯}}:{\mathrm{\Sigma }}^{\ast }\to M$.

In more detail, for any

$f:\mathrm{\Sigma }\to M$ there is a unique monoid homomorphism

$$f^{\mathrm{♯}}:{\mathrm{\Sigma }}^{\ast }\to M$$

such that

$f^{\mathrm{♯}}([a])=f(a)$.

In Haskell, the induction principle can be defined as (see also the code in induction)

fold :: m -> (m->m->m) -> (a->m) -> List a -> m
fold e mult f Nil = e
fold e mult f (Cons x xs) = mult (f x) (fold e mult f xs)  

The first two arguments are the monoid

$M$ and the third argument is the function

$f:\mathrm{\Sigma }\to M$.

Programming Exercise: Implement the following functions using fold.

• a function List Int -> Int computing the sum of a list of integers.
• a function List Int -> Int computing the product of a list of integers.
• a function List a -> Int computing the length of a list.
• a function List (List a) -> List a that flattens a list (like concat does for Haskell's predefined lists).
• a function List (List a) -> Int that computes the sum of the lengths of the lists in a list.

Btw, instead of a programming exercise, this can also be seen as an exercise in writing down mathematical defintions.

Programming Exercise: Redo the exercises above with Haskell's predefined lists.

Recursion over Algebraic Data Type

Every signature gives rise to a recursion principle. We can take for example binary trees.

By the way, here we see again why for applications it is usually necessary/convenient to generalise our definitions so that they allow for many-sorted/typed algebras. For example, for binary trees over integers, we want to sorts/types, say,

$T$ for trees and

$\mathbb{Z}$ for integers and operations ^[11]

$$\begin{array}{rl}Nil& :1\to T\\ Node& :\mathbb{Z}\times T\times T\to T\end{array}$$
The first makes an empty tree and the second makes a bigger tree from a left subtree, a right subtree and an integer.

See the Homework on Algebraic Data Types below for more.

Theory

(initial and free algebras will play an essential role in the next two lectures)

We continue from the section on axioms and universal algebra.

The principle of induction we have seen at work in the previous examples is induction over the set of all terms formed from the operations of a signature. The set of all terms these terms forms again an algebra. For example, the set

$\{\mathrm{O},\mathrm{S}\mathrm{O},\mathrm{S}\mathrm{S}\mathrm{O},\dots \}$ is closed under taking successors.

Definition: Let

$\mathrm{\Sigma }$ be a signature and let

$X$ be a set of "variables". The set

${\mathsf{T}\mathsf{e}\mathsf{r}\mathsf{m}}_{\mathrm{\Sigma },X}$ of all "terms" is the smallest set closed under the rules

$$\frac{t_1,\dots t_n\in {\mathsf{T}\mathsf{e}\mathsf{r}\mathsf{m}}_{\mathrm{\Sigma },X}}{\sigma (t_1,\dots t_n)\in {\mathsf{T}\mathsf{e}\mathsf{r}\mathsf{m}}_{\mathrm{\Sigma },X}}\sigma \in \mathrm{\Sigma },\mathsf{a}\mathsf{r}\mathsf{i}\mathsf{t}\mathsf{y}(\sigma )=n\frac{}{x\in {\mathsf{T}\mathsf{e}\mathsf{r}\mathsf{m}}_{\mathrm{\Sigma },X}}x\in X$$

We write

${\mathsf{T}\mathsf{e}\mathsf{r}\mathsf{m}}_{\mathrm{\Sigma }}$ if

$X$ is empty.

${\mathsf{T}\mathsf{e}\mathsf{r}\mathsf{m}}_{\mathrm{\Sigma },X}$ is a

$\mathrm{\Sigma }$-algebra, the termalgebra over

$\mathrm{\Sigma }$ and

$X$, under the operations

$$\bar{\sigma }:({\mathsf{T}\mathsf{e}\mathsf{r}\mathsf{m}}_{\mathrm{\Sigma },X}{)}^n\to {\mathsf{T}\mathsf{e}\mathsf{r}\mathsf{m}}_{\mathrm{\Sigma },X}$$

defined by the rule on the left above.

Proposition: Fix a signature

$\mathrm{\Sigma }$.

1. For any algebra

   $A$ there is a unique homomorphism
   
   $${\mathsf{T}\mathsf{e}\mathsf{r}\mathsf{m}}_{\mathrm{\Sigma }}\to A$$

2. For any algebra

   $A$, set of variables
   $X$, and function
   $f:X\to A$, there is a unique homomorphism
   
   $$f^{\mathrm{♯}}:{\mathsf{T}\mathsf{e}\mathsf{r}\mathsf{m}}_{\mathrm{\Sigma },X}\to A$$

   such that

   $f^{\mathrm{♯}}(x)=f(x)$.

Maths Exercise: Prove the proposition by induction on the structure of the termalgebra.

Maths Exercise: In the section on examples on induction and the program induction, we saw the definition

fold :: m -> (m->m->m) -> (a->m) -> List a -> m
fold e mult f Nil = e
fold e mult f (Cons x xs) = mult (f x) (fold e mult f xs)  

Show that fold is the unique homomorphism from the free monoid List a over a to a monoid (m,e,mult) wrt f:a->m, that is,

$$\begin{array}{c}\mathtt{\text{fold e mult f}}={\mathtt{\text{f}}}^{\mathrm{♯}}\end{array}$$

Answer. ^[12]

The existence and uniqueness of the homomorphism is called the universal property of the termalgebra. An algebra with Property 1 is also called an initial algebra and an algebra with Property 2 a free algebra over

$X$.

Notice that the fact that the termalgebra has the universal property is proved by induction. Conversely, when we will study category theory in the next lecture, we will take the universal property of an initial algebra as an axiomatisation of induction.

Applications

(can be skipped if the importance of structure preserving maps is appreciated)

We will present two applications of the concept of structure preserving maps, one to mathematics and one to theoretical computer science. An application to programming will be presented as homework below.

1. The mathematical application uses the notion of structure preserving map to answer the question whether there are more fractions than integers in two different, seemingly contradictory ways. The apparent paradox will be solved by paying attention to the notion of struture implicit in the two answers.

2. The theoretical computer science application uses the notion of structure preserving map to give a mathematical answer to the following question. What is the meaning of a programming language?

3. The application to programming is to show that the unique homomorphism from the termalgebra can be programmed by recursion over an algebraic data type.

Are there more rational numbers than integers?

What do you think: Are there more fractions than integers?

(This is one of those questions where both yes and no can be a correct answer depending on how you justify it.)

Convention: I restrict my attention to positive rationals and positive integers and I denote them by

$\mathbb{Q}$ and

$\mathbb{N}$, respectively. The answers remain true if we extend to all rationals and integers.

Answer 1: There are strictly more rationals than integers

It seems obvious that there are more rationals than integers.

We can visualise this by looking at the numberline where there are gaps between integers, but the rationals are dense.

In symbolic notation, we look at the inclusion

$$\mathbb{N}\hookrightarrow \mathbb{Q}$$

which is injective but not surjective, hence not bijective: Every integer is a rational, but there are rationals that are not integers.

Answer 2: There are at least as many integers as rationals

Can we encode rationals by integers? After all, we know that rationals are stored in a computer as sequences of bits and that every sequence of bit is an integer in binary notation. This suggests that there is an injective function

$$\mathbb{Q}\to \mathbb{N}$$

showing that there are at least as many rationals as integers. Equivalently, and easier to explain, we can also look for a surjective function

$$\mathbb{N}\to \mathbb{Q}$$

We guess, from the fact that rationals can be represented on a digital computer, that such a map must exist.

But what is an easy way to describe such a map explicitely?

It was found by Cantor and is most easily given by a picture. You can derive from the picture an algorithm that computes the functions

$\mathbb{Q}\to \mathbb{N}$ and

$\mathbb{N}\to \mathbb{Q}$ via going through a while loop. You can also challenge your math-muscles and derive an explicit formula that does not need going through a loop.

Remark: The map

$\mathbb{N}\to \mathbb{Q}$ given by the picture assigns more than one code to each rational as eg

$1/2=2/4$. Thus the picture gives a surjective but not bijective

$\mathbb{N}\to \mathbb{Q}$. But we can define a bijective map from it by eliminating duplicate codes.

It seems that we reached a contradiction between Answer 1 and Answer 2.

Thinking about it, it looks like Answer 2 is winning. Because, by reaching Answer 1, we made a mistake. We argued that an map

$A\to B$ that is injective but not surjective proves that there are strictly more

$B$ than

$A$. This is true for finite sets, but wrong for infinite sets.

Nevertheless, Answer 1 looks intuitively correct. So can we restore our intuition and justify it by an explanation that stands up to scientific standards of scrutiny?

The answer is yes and what we need for the justification is the notion of structure preserving map.

Exercise/Activity: Can you lead the development we abandoned with the last sentence to a satisfying conclusion?

Denotational Semantics of Programming Languages

The abstract syntax of a programming language can be described in terms of universal algebra. For example, the abstract syntax of

$\lambda$-calculus

data Exp = Var String | App Exp Exp | Abs String Exp

corresponds to a two-sorted universal algebra, one sort String for variables and one sort for expressions, as well as two operations, one for application and one for abstraction.

Before we come back to

$\lambda$-calculus let us first look at the example of arithmetic. For example, if we take as abstract syntax of a simple language of arithmetic

data Exp = 1 | Add Exp Exp | Mult Exp Exp

this corresponds to a signature

$\mathrm{\Sigma }=\{1,+,\ast \}$. The meaning of this language can be described as the unique homomorphism

$$\mathsf{T}\mathsf{e}\mathsf{r}{\mathsf{m}}_{\mathsf{\Sigma }}\to (\mathbb{N},1,+,\cdot )$$

For more on this perspective see my lecture on operational and denotational semantics.

Now let us quickly come back to the question why we need to go beyond universal algebra, if we want to extend these techniques from arithmetic to

$\lambda$-calculus and other programming languages.

• Universal algebra only supports operations of type
  $A^n\to A$. To treat typed functional programming languages, we need to extend universal algebra with a more expressive type system, and this is one reason why category theory, to be introduced in the next lecture, is of such importance in programming language research.
• A more subtle point is that universal algebra does not provide us with tools to deal with variable binding, the distinction between free and bound variables,
  $\alpha$-equivalence, capture avoiding substitution. ^{[13] [14]} These issues are pursued in an area of theoretical computer science known as nominal sets or nominal techniques. ^[15]

For more on variables and binding see my lecture .

Homework

(Maths)

$X^{\ast }$ is the free monoid over

$X$

(prove that List a is the free monoid over a)

In the previous lecture we defined

$X^{\ast }$ (or List a) and called it the free monoid. In the next lecture we will see an independent definition of free algebra. To show that these two definitions agree, one has to show the following.

Let

$(M,e,\ast )$ be a monoid. For any map

$f:X\to M$ there is a unique monoid homomorphism

$f^{\mathrm{♯}}:X^{\ast }\to M$ such that

$$f^{\mathrm{♯}}([x])=f(x).$$

• Define multiplication (=concatenation) on lists inductively.
• Define
  $f^{\mathrm{♯}}$ inductively.
• Show that
  $f^{\mathrm{♯}}([x])=f(x)$.
• Show that
  $f^{\mathrm{♯}}([])=e$.
• Show that
  $f^{\mathrm{♯}}$ preserves multiplication.

Remark: We will see in Lecture 4 that all free algebras correspond to monads, and vice versa. But there is something special about the example of lists:

• $X^{\ast }$ is the free algebra over the empty set for the signature
  $\mathrm{\Sigma }=\{[]\}\cup X$ where the arity of
  $[]$ is 0 and the arity of the elements
  $x\in X$ is
  $1$.
• $X^{\ast }$ is the free monoid over
  $X$.

It may be interesting to think about the analogy List a and BTree a, see the below, and to try to turn BTree into a monad/free algebra over a.

(Programming) Recursion over Algebraic Data Types

(if you want to do some programming, this homework illustrates that inductively-defined structure-preserving maps on termalgebras can be run on a computer)

As an application I will show that we can program with the univeral property of initial algebras, at least if no equations are involved. I will use Haskell, but everything is entirely general and can be made to work in any programming language (possibly in a more cumbersome notation).

Head over to algebraic-data-types to run and implement some Haskell functions defined by the univeral property of initial algebras.

Type :load main.hs into the console on the right to call individual functions and use "run" to execute the test defined in main.

We have seen that the natural numbers come with at least two induction principles, one for the signature of zero and successor and one for the natural numbers as monoids. The first one has the advantage that definition of natural numbers via zero and successor does not involve any equations. For such structures Haskell can run definitions by induction automatically.

The first line defines the natural numbers as an intial algebra (algebraic data type) in Haskell:

data NN = Zero | Succ NN

Mathematically, we would write this as two functions

$$\begin{array}{r}Zero:1\to \mathbb{N}\\ Succ:\mathbb{N}\to \mathbb{N}\end{array}$$

If you already know about addition on

$\mathbb{N}$ you want

$Succ(n)=1+n$. But the perspective we are taking here is that we define the natural numbers, from scratch.

So we go the other way round and define addition by induction on the structure that defines

$\mathbb{N}$, namely zero and successor:

$$\begin{array}{rl}Zero+y& =y\\ Succ(n)+y& =Succ(n+y)\end{array}$$

Exercise: Show, by induction on

$n$, that

$Succ(n)=1+n$.

In Haskell, the definition of addition looks almost the same: ^[16]

add Zero y = y
add (Succ n) y = Succ (add n y)

One advantage of the Haskell syntax is that it actually runs. Enter in the console

add (Succ Zero) (Succ Zero)

to obtain the result

Succ (Succ Zero)

Next, we define in Haskell the free monoid over a type a

data List a = Nil | Cons a (List a)

Mathematically, replacing now a with

$X$, we would write this as two functions ^[17]

$$\begin{array}{rl}Nil& :1\to X^{\ast }\\ Cons& :X\times X^{\ast }\to X^{\ast }\end{array}$$

At this point, I slowly start to prefer Haskell to maths. Judge for yourself, but if you head over to adt.hs, dedinitions such as

len Nil = 0
len (Cons x xs) = 1 + len xs

are neat enough that I don't want to repeat them in mathematical notation. (But try it as an exercise, just to make sure you can translate between the two ways of writing.)

After we have done this, we will also be in a position to understand better the remark that these operations are generic. For example, replay what we did so far for the data type of binary trees

data BTree a = Nil | Node (BTree a) (BTree a) a 

and compare BTree and List.

With binary trees one can define heap sort. The idea is to transform a list into a heap and then to flatten the heap into a sorted list.

Here is a definition of a heap:

• Nil is a heap.
• Node t a n is a heap if all nodes in t are
  $\le n$ and all nodes in s are
  $\ge n$.

Define the following functions.

data BTree a = Nil | Node (BTree a) (BTree a) a 

member :: Eq a => BTree a -> a -> Bool

max_tree :: BTree Int -> Int

insert :: BTree Int -> Int -> BTree Int

heapify :: [Int] -> BTree Int

is_heap :: BTree Int -> Bool

flatten :: BTree Int -> [Int]

They should satisfy the property that

$\mathsf{f}\mathsf{l}\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{e}\mathsf{n}\circ \mathsf{h}\mathsf{e}\mathsf{a}\mathsf{p}\mathsf{i}\mathsf{f}\mathsf{y}(xs)$ is sorted as well as the equations

$$\begin{array}{rlr}\mathsf{f}\mathsf{l}\mathsf{a}\mathsf{t}\mathsf{t}\mathsf{e}\mathsf{n}\circ \mathsf{h}\mathsf{e}\mathsf{a}\mathsf{p}\mathsf{i}\mathsf{f}\mathsf{y}(xs)& =xs& \text{ if }xs\text{ is sorted}\\ \mathsf{i}\mathsf{s}\mathsf{\_}\mathsf{h}\mathsf{e}\mathsf{a}\mathsf{p}\circ \mathsf{h}\mathsf{e}\mathsf{a}\mathsf{p}\mathsf{i}\mathsf{f}\mathsf{y}(xs)& =\mathsf{T}\mathsf{r}\mathsf{u}\mathsf{e}\\ ...\end{array}$$

(Programming) A Binary Tree monad

For the bintary trees above there is no obvious way to define a mu :: BTree (BTree a) -> BTree. But if we store data only in the leaves that changes. At magma, you can implement a monad structure on

data Magma a = Leaf a | Node (Magma a) (Magma a)

From a programming point of view Magma a is a kind of binary tree. But Magma a is also the free magma over a. ^[18]

Summary and Outlook

In this lecture, we already have seen a lot of category theory, without calling it that. Indeed, by now, many of the main protagonsits have appeared: categories, functors, natural transformations, initial objects, free algebras and left adjoints, monads, univeral properties. So it is time to reveal this structure in the next lecture.

References and Further Reading

… ask me if you are interested …

---

1. Why is

   $x\mapsto 2x$ not a proper clock? Which function corresponds to the clock that run out of battery? ↩︎

2. Is constructed from two Greek words meaning "similar form". ↩︎

3. We use the same symbols

   $0$ and
   $+$ for two different operations. Both in mathematics and in programming is this kind of overloading widely used. ↩︎

4. The

   $\mathrm{\Sigma }$-termalgebra has elements
   $\mathrm{O}$,
   $\mathrm{S}\mathrm{O}$,
   $\mathrm{S}\mathrm{S}\mathrm{O}$, etc. Define a function from
   $\mathbb{N}$ to the termalgebra by induction:
   $f(0)=\mathrm{O}$ and
   $f(n+1)=\mathrm{S}f(n)$. This function is bijective, hence an isomorphism. ↩︎

5. By the property of a homomorphism, we must have

   $f(0)=\mathrm{O}$ and
   $f(n+1)=s(f(n))$. This determines
   $f$ uniquely. ↩︎

6. The free monoid

   $M$ over
   $\mathrm{\Sigma }=\{s\}$ has elements
   $ϵ,s,ss,sss,\dots$. Define
   $f:M\to \mathbb{N}$ as
   $f(w)=length(w)$.
   $f$ is a bijection (why?). And
   $f$ preserves the monoid structure. Indeed,
   $f(ϵ)=0$ and
   $f(wv)=length(wv)=length(w)+length(v)=f(w)+f(v)$. ↩︎

7. Consider

   $f^{\prime }$ with
   $f^{\prime }(1)=m$. We have to show
   $f^{\prime }=f$. We know $f(0)=f'(0). (Why?) Morevover, for
   $n=1+\dots 1$,
   $n>0$, we have
   $f^{\prime }(n)=f^{\prime }(1+\dots 1)=f^{\prime }(1)\cdot \dots f^{\prime }(1)=f(1)\cdot \dots f(1)=f(1+\dots 1)=f^{\prime }(n)$. ↩︎

8. The structure arising from dropping the neutral element and identity laws from the definition of monoids is known as semi-group. ↩︎

9. Instead of

   $\mathtt{x}\in \mathtt{a}$ we could also write
   $\mathtt{x}\mathtt{::}\mathtt{a}$, using Haskell's notation x :: a to indicate that x is an element of type a. ↩︎

10. To understand len as a

    $\mathrm{\Sigma }$-algebra homomorphism, we need to think of Integer as a
    $\mathrm{\Sigma }$-algebra, that is, we need an interpretation on Integer of the operation symbols
    $\{\mathtt{N}\mathtt{i}\mathtt{l}\}$ and
    $\mathtt{C}\mathtt{o}\mathtt{n}\mathtt{s}\mathtt{x}$. The Haskell definition of len does this implicitely: Nil is interpreted as 0 and all Conx x are interpreted as 1+. ↩︎

11. From a universal algebra point of view, there are two ways to treat

    $\mathbb{Z}$ in the example of binary trees. We can take
    $\mathbb{Z}$ as a parameter of the definition. Or we can take
    $\mathbb{Z}$ as a second sort and explicitely add the integer-operations with their equations to a 2-sorted algebra. There can be subtle differences between these two ways of modelling, but they do not need to concern us here. In case you want to know, for what we are doing here, I find it easier to consider
    $\mathbb{Z}$ as a parameter. ↩︎

12. We let

    $\mathrm{\Sigma }$ be the signature of monoids (one unary operation, one binary operation). Then List a is isomorphic to the termalgebra
    $${\mathsf{T}\mathsf{e}\mathsf{r}\mathsf{m}}_{\mathsf{\Sigma }\mathsf{,}\mathtt{\text{a}}}\mathsf{.}$$

    If e :: m and mult :: m->m->m satisfy the equations of a monoid, then

    $(\mathtt{m}\mathtt{,}\mathtt{e}\mathtt{,}\mathtt{m}\mathtt{u}\mathtt{l}\mathtt{t}\mathtt{)}$ is a monoid. Therefore, by the universal property of the termalgebra, any f::a->m induces a unique monoid homomorphism
    $${\mathtt{f}}^{\mathrm{♯}}\mathtt{::}{\mathsf{T}\mathsf{e}\mathsf{r}\mathsf{m}}_{\mathsf{\Sigma }\mathsf{,}\mathtt{\text{a}}}⟶\mathsf{(}\mathtt{m}\mathtt{,}\mathtt{e}\mathtt{,}\mathtt{m}\mathtt{u}\mathtt{l}\mathtt{t}\mathtt{)}\mathtt{.}$$

    It remains to show that

    ${\mathtt{f}}^{\mathrm{♯}}$ is indeed foldMon e mult f. This is similar to this exercise. ↩︎

13. For example, the capture avoiding substitution of

    $\lambda$-calculus is very different from the substitution into free variables one has in universal algebra. ↩︎

14. Nevertheless, universal algebraic techniques can be used to prove powerful results about

    $\lambda$-calculus, see eg the work of Antonino Salibra. ↩︎

15. See the work by Gabbay and Pitts. ↩︎

16. If you want to understand why Haskell syntax is different there are two (related) reasons. The first is historical: Haskell inherited its syntax from the

    $\lambda$-calculus. The second is that Haskell syntax is superior to the conventional maths syntax if one works with higher order functions. ↩︎

17. If you wonder why the Haskell notation and the mathematical notation are much closer for the functions like addition than for the definition of the data types: We will be able to remedy this in the next lecture when we introduce functors. In fact, a definition like data List a is best understood as defining a functor

    $List(X)$. ↩︎

18. Let

    $\mathrm{\Sigma }$ be a signature with one binary operation symbol. Then Magma a is
    ${\mathsf{T}\mathsf{e}\mathsf{r}\mathsf{m}}_{\mathrm{\Sigma },\mathtt{a}}$. ↩︎