Functional correctness with the Haskell masters
Training to build quality code on scientific excellence
26 September 2018 6 mins read
At IOHK, we are proud of our scientific approach and close collaboration with academia. We publish in peer reviewed scientific journals and present our results at acclaimed international conferences to ensure that our protocols and algorithms are built on rock-solid foundations. Our software must reflect this scientific excellence and quality, which means that we need a process…
IOHK releases Icarus to the Cardano community
Developers can now build their own light wallets
15 August 2018 7 mins read
Today IOHK releases Icarus, a reference implementation for a lightweight wallet developed by the IOHK engineering team. We hope that this code base will be used as a point of reference to enable developers to create their own secure light and mobile wallets for Cardano. Icarus is a fully open source code base that will be the first step in a range of open source initiatives to…
How does Casper compare to Ouroboros?
Differences between the proposed Ethereum protocols and Cardano’s consensus algorithm
9 August 2018 13 mins read
TL;DR In response to recent discussions in social media, we give a brief comparison of the Ouroboros and Casper proof-of-stake protocols.
Ouroboros is a formally specified and analysed protocol with mathematically proven security guarantees based on clearly specified assumptions. The protocol description, models and proofs are all public. Hence, the underlying assumptions, the…
From free algebras to free monads
7 August 2018 29 mins read
In universal algebra freeness is a well defined algebraic property. We will explore equational theories which are tightly connected to free algebras. We will consider free monoids. Then we'll explain how monads can be brought into the picture in the context of monoidal categories. This will lead to a precise definition of a free monad as a free monoid.
This post requires familiarity with some very basic Category Theory and does not assume any knowledge on universal algebra. Most mathematical notions will be introduced but you might want to dig into literature for some more examples; though most of the books are quite lengthy and not suited for non-mathematicians - you've been warned ;). Knowing this I tried to bring all the required definitions, together with some very basic examples. As you read you may want to read about semigroups, monoids, groups, $G$-sets, lattices, Boolean or Heyting algebras from Wikipedia articles or try to find info on nCatLab (though this is is a heavy resource, with mostly with higher categorical approach, so probably better suited for more familiar readers).
Preliminaries
We will need some preliminary definitions. Let's begin with a definition of algebra. For a set $A$ we will denote $A^n$ the $n$th cartesian product of $A$, i.e. $A^2=A\times A$.
Definition Algebra
Examples includes many classical algebraic structures, like semigroups, where there is only a single operation of arity 2, monoids which in addition have one operation of arity $0$ - the unit element of multiplication. Other source of examples are Boolean algebras with two 2-ary operations $\wedge$ and $\vee$ or more generally lattices, Heyting algebras. Also rings, modules, fields, vector spaces and countless other structures. Universal algebra has a very general theory describing common concepts but also deals with very special cases of some of more esoteric algebras.
Definition Homomorphism
This means that homomorphism preserve operations. For example a homomorphism of monoids is a map that preserves the multiplication and unit. For boolean algebras, it means that a homomorphism preserves the $\vee$ (also called join) and $\wedge$ (usually called meet) operations, etc.
It is an easy observations that homomorphism are closed under composition and since the identity map is always a homomorphism this leads to well defined categories, e.g. category of monoids, category of boolean algebras, category of rings, ...
Free algebras and Equational theories
Free Algebra
As you can see the definition of a free algebra requires a context, this interesting in its own! There are free monoids in the class of all monoids and there are free commutative monoids in the class of commutative monoids (i.e. monoids in which $m\cdot n=n\cdot m$ for each elements $m,n$).
Many theories allow free algebras. Let's see some other examples:
-
The monoid of natural numbers $\mathbb{N}$ with addition and $0$ as its unit element is a free monoid generated by $\{1\}$. It is both free in the class of all monoids and in the class of commutative ones. The $n$-th cartesian product $\mathbb{N}^n$ is a free commutative monoid generated by the set $\{(1,0,\ldots,0),(0,1,0,\ldots,0),\ldots,(0,\ldots,0,1)\}$, but it's not a free monoid in the class of all monoids.
-
The additive group of integers $\mathbb{Z}$ is a free group with one generator, it is also free in the class of commutative groups. As in monoids: $\mathbb{Z}^n$ is a free commutative group with $n$ generators.
-
A free group with two generators can be pictured as the Cayley graph (which is a fractal) (note that its first quarter is the free monoid with two generators).
-
Every vector space is free, since every vector space admits a basis.
-
In the class of $G$-sets, free $G$ sets are exactly all the cartesian products of $G^n$.
-
In the class of rings, polynomial rings with integer coefficients, usually denoted by: $\mathbb{Z}[X]$ or $\mathbb{Z}[X_1,\dots,X_n]$ for polynomials with many variables) are free (you likely have learned quite a lot about them in school, you just haven't been told the really interesting part ;)). This example was the motivation for terms, their algebra and term functions which we will discover next.
This is also true for semi-rings. You might have used this fact when using purescript validation library. A free semiring generated by a type `a` has type `[[a]]`; for example `[[()]]` is isomorphic to $\mathbb{N}[X]$, since (please excuse mixing Haskell and mathematical notation): $$[[()]]\simeq[\mathbb{N}]\simeq\mathbb{N}[X]$$
Free algebras play an essential role in a proof of beautiful and outstanding Birkhoff theorem. It states that a class of algebras $\mathcal{C}$ is an equational theory if and only if the class is closed under cartesian products, homomorphic images and subalgebras. Equational theories are classes of algebras which satisfy a set of equations; examples includes: semigroups, monoids, groups or boolean or Heyting algebras but also commutative (abelian) semigroups / monoids / groups, and many other classical algebraic structures.
We need to be a little bit more precise language to speak about equational theories in the full generality of universal algebra, which we are going to introduce.
Terms, term functions and their algebra
Definition Term
Let’s consider an algebra type $(f_i)_{i=1,\ldots,n}$. Then the set of terms on a set $X$ (set of variables) is inductively defined as:
-
each $x\in X$ is a term (of arity $0$)
-
each $f_i(x_1,\dots ,x_{j_i})$ is a term of arity $j_i$ for $x_1,\dots ,x_{j_i}\in X$
-
if $g_1,\dots g_n$ are terms of arities $j_1$ to $j_n$ respectively, and $g$ is a term of arity $n$ then $g(g_1(x_{11},\dots,x_{1j_1}),\dots, g_n(x_{n1},\dots,x_{nj_n}))$ is a term of arity $j_1+\dots+j_n$ with $x_{kl}\in X$.
We will denote the set of terms on $X$ by $\mathsf{T}^{(f_i)_{i=1,\dots,n}}(X)$ or simply $\mathsf{T}(X)$.
For example in groups: $x^{-1}\cdot x$, $x\cdot y$ and $1$ (the unit of the group) are terms. Terms are just abstract expressions that one can build using algebraic operations that are supported by the algebra type. Each term $t$ defines a term function on every algebra of the given type. In groups the following terms are distinct but they define equal term function: $x^{-1}\cdot x$ and $1$; on the other hand the two (distinct) terms $(x\cdot y)\cdot z$ and $x\cdot (y\cdot z)$ define equal term functions. The two terms $x\cdot y$ and $y\cdot x$ define distinct term functions (on non commutative groups or commutative monoids). Another example comes from boolean algebras (or more broadly lattice theory) where the two terms $x\wedge (y\vee z)$ and $(x\wedge y)\vee(x\wedge z)$ define equal term functions on Boolean algebras (or more generally distributive lattices). If $t$ is a term then the associated term function on an algebra $\underline{A}$ we let denote by $\tilde{t}^{\underline{A}}$. Term functions are natural to express equalities within a theory. Now we are ready to formally define equational classes of algebras.
Definition Equational Theory
For example the class of monoids is an equational theory for $$\mathbf{E}=\bigl\{(1\cdot x,\, x),\; (x\cdot 1,\, x),\; \bigl((x\cdot y)\cdot z,\, x\cdot (y\cdot z)\bigr)\bigr\}$$ i.e. all the algebras with two operations: one of arity 0 (the unit) and one of arity 2 (the multiplication), such that the $1$ is the unit for multiplication $\cdot $ and multiplication is associative. The class of commutative monoids is also an equational theory with one additional equation $(x\cdot y,\, y\cdot x)$. Groups, Boolean or Heyting algebras, lattices are also equational theories.
Coming back to free algebras: it turns out that the set of terms $\mathsf{T}^{(f_i)}(X)$ on a given set of variables $X$ has an algebra structure of type $(f_i)_{i=1,\dots,n}$: it is given by the inductive step in the definition of terms: if $t_i\in \mathsf{T}^{(f_i)}(X)$ for $i=1,\dots,j_i$ then $$ f_j^{\underline{\mathsf{T}^{(f_i)}(X)}}(t_1,\ldots,t_{j_i}) := f_j(t_1,\ldots,t_{j_i})\in \mathsf{T}(X) $$ Furthermore $\underline{\mathsf{T}^{(f_i)}(X)}$ is a free algebra over $X$ in the class of all algebras of the given type $(f_i)_{i=1,\dots,n}$. An extension of a map $h:X\rightarrow\underline{A}=(A,(f_i^{\underline{A}})_{i=1,\ldots,n})$ can be build inductively following the definition of terms and using the homomorphism property: $$ h(f_i(t_1,\ldots,f_{i_j})) := f_i^{\underline{A}}(h(t_1),\ldots,h(t_{i_j})) $$ The map $h$ is indeed a homomorphism: $$ \begin{array}{ll} h\bigl(f_i^{\underline{\mathsf{T}(X)}}(t_1,\ldots,t_{i_j})\bigr) & = h(f_i(t_1,\ldots, t_{i_j}) \\\\ & = f_i^{\underline{A}}(h(t_1),\ldots, h(t_{i_j})) \\\\ \end{array} $$ Note that the class of algebras of the same type is usually very broad, but this is the first approximation to build free algebras in an equational theory. This is just the equational theory for the empty set $\mathbf{E}$.
Let’s see this on an example and let us consider algebras of the same type as a monoid: with one nullary operation (unit $1$ or `mempty` if you like) and one 2-ary operation (multiplication / `mappend`). Let $X$ be a set of variables. Then $1$ is a valid term, and also if $t_1$ and $t_2$ are terms on $X$ then also $t_1\cdot t_2$ is a term, but also $t_1\cdot 1$ and $1\cdot t_2$ are valid and distinct terms. $\mathsf{T}(X)$ resembles a monoid but it isn't. It is not associative and the unitality condition is not valid since $t\cdot 1\neq t\neq 1\cdot t$ as terms. We still need a way to enforce the laws. But note that if you have a map $f:X\rightarrow M$ to a monoid $M$ which you'd like to extend to a homomorphism $\mathsf{T}(X)\rightarrow M$ that preserves $1$ (which is not the unit, yet) and multiplication (even though it is not associative), you don’t have much choice: $\mathsf{T}(X)\rightarrow M$: $t_1\cdot t_2$ must be mapped to $f(t_1)\cdot f(t_2)\in M$.
We need a tool to enforce term equations. For that one can use
Definition Congruence relation
- reflexive: for each $a\in A$: $a\sim a$
- symmetric: for each $a,b\in A$: if $a\sim b$ then $b\sim a$
- transitive: for each $a,b,c\in A$: if $a\sim b$ and $b\sim c$ then $a\sim c$
Equivalence relations and congruences form complete lattices (partial ordered which have all suprema and minima, also infinite). If you have two equivalence relations (congruences) then their intersection (as subsets of $A^2$) is an equivalence relation (congruence).
The set of equations that defines the class of monoids generates a congruence relation on the term algebra $\underline{\mathsf{T}^{f_i}(X)}$ (i.e. an equivalence relation which is compatible with operations: $x_1\sim y_1$ and $x_2\sim y_2$ then $(x_1\cdot y_1) \sim (x_2\cdot y_2)$). One can define it as the smallest congruence relation which contains the set $\mathbf{E}$. Equivalence relation on a set $A$ is just a subset of the cartesian product $A\times A$ (which satisfy certain axioms), so it all fits together! One can describe this congruence more precisely, but we'll be happy with the fact that it exists. To show that, first one need to observe that intersection of congruences is a congruence, then the smallest congruence containing the set $\mathbf{E}$ is an intersection of all congruences that contain $\mathbf{E}$. This intersection is non empty since the set $A\times A$ is itself a congruence relation.
The key point now is that if we take the term algebra and take a quotient by the smallest congruence that contains all the pairs of terms which belong to the set $\mathbf{E}$ we will obtain a free algebra in the equational class defined by $\mathbf{E}$. We will leave the proof to a curious reader.
Free monoids
Let’s take a look on a free monoid that we can build this way. First let us consider the free algebra $\underline{\mathsf{T}(X)}$ for algebras of the same type as monoids (which include non associative monoids, which unit does not behave like a unit). And let $\sim$ be the smallest relation (congruence) that enforces $\mathsf{T}(X)/\sim$ to be a monoid.
Since monoids are associative every element in $\underline{\mathsf{T}(X)}/\sim$ can be represented as $x_1\cdot( x_2\cdot (x_3\cdot\ldots \cdot x_n))$ (where we group brackets to the right). Multiplication of $x_1\cdot( x_2\cdot (x_3\cdot\ldots \cdot x_n))$ and $y_1\cdot( y_2\cdot (y_3\cdot\ldots \cdot y_m))$ is just $x_1\cdot (x_2\cdot (x_3\cdot\ldots\cdot(x_n\cdot (y_1\cdot (y_2\cdot (y_3\cdot\ldots\;\cdot y_m)\ldots)$. In Haskell if you’d represent the set $X$ as a type $a$ then the free monoid is just the list type $[a]$ with multiplication: list concatenation and unit element: the empty list. Just think of
-- A set with `n` elements corresponds
-- to a type with `n` constructors:
data X = X_1|⋯|X_n
Free Monads
It turns out that monads in $\mathcal{Hask}$ are also an equational theory. Just the terms are higher kinded: $*\rightarrow*$ rather than $*$ as in monoids. The same construction of a free algebra works in the land of monads, but we need to look at them from another perspective. Let us first take a mathematical definition of view on monads.
Definition Monad
class Monad m where
return :: a -> m a
join :: m(m a) -> m a
which is unital and associative, i.e. the following law holds:
-- | associativity
join . join == join . fmap join
-- | unitality
join . return = id = join . fmap return
These axioms are easier to understand as diagrams:
It is a basic lemma that this definition a monad is equivalent to what we are used to in Haskell:
class Monad m where
return :: a -> m a
>>= :: m a -> (a -> m b) -> m b
Having `join` one defines `>>=` as
ma >>= f = join $ f <$> ma
and the other way, having `>>=` then
join = (>>= id)`
Not only these two constructions are reverse to each other, but also they translate the monad laws correctly.
Monoids in monoidal categories
To define a monoid $M$ in the category $\mathcal{Set}$ (of sets) one needs the product $M\times M$. Abstraction of this structure leads to…
Cardano smart contracts testnet IELE launches
Developers can run programs with increased confidence
30 July 2018 4 mins read
Today we launch the second Cardano testnet, which is for the IELE virtual machine (VM) and follows our recent launch of the KEVM testnet. The technology is not only an important step on the Cardano roadmap, but also for the industry – in offering robust and reliable financial infrastructure. Developers now have the opportunity to explore the smart contracts technology that will…
Recent posts
The 11 blockchain tenets: towards a blockchain bill of rights by Prof Aggelos Kiayias
11 October 2024
An unforgettable learning experience in Argentina by Ivan Irakoze
12 September 2024
Input | Output at Tokyo Tech: pushing the boundaries of blockchain technology by Olga Hryniuk
5 September 2024