What exactly is algebraic about algebraic effects or algebraic data
types? Which module/object signatures are actually algebraic? What is
algebra anyway? Where is freedom in free algebra? What is the initial
algebra, what good does it do, and how does one actually prove the
initiality? Can we say something precise about the correctness of
a tagless-final DSL embedding and its interpreters? How do we
substantiate the correctness claims?

This web page, written in the form of lecture notes, is (being) built in response to such questions. It presents the standard introductory material from the field of Universal Algebra -- however, selected and arranged specifically for programmers, especially those interested in the tagless-final approach. We only use programming examples, and, as far as possible, a concrete programming language notation rather than mathematical notation.

- Introduction
- Signatures and Sigma-Algebras
- Algebra Homomorphism
- Initial Algebra
- Syntax and Semantics
- Algebraic Data Types
- Free Algebra
- Equalities (identities), equational laws, equational theories
- Case-study: a DSL of AB grammars and its tagless-final embedding

- What is Algebra? Garett Birkhoff, the founder of the field now called
Universal Algebra, said:
``By an `abstract algebra' is meant, loosely speaking, any system of elements and operations such as a ring, a field, a group, or a Boolean algebra'' (Birkhoff, 1935).
Universal Algebra is a field of Mathematics. A significant part of a Universal Algebra course and textbooks is devoted to lattices and combinatorics. There is not much connection, it seems, to common programming tasks. And yet it is. The automata theory (finite state machines, Kleene Algebra, regular expressions, etc.) was one of the first applications of algebras in Computer Science. According to Goguen et al. (1977), Burstall and Landin's ``Programs and their proofs: An algebraic approach'' (1969) was the first use of universal algebra and (implicitly) initiality in programming language semantics. F.L.Morris (``Correctness of translations of programming languages'', Ph.D. Thesis, Stanford, 1972) brought in many-sorted algebras, most commonly of interest in programming languages. The ADJ collaboration (J.A. Goguen, J.W. Thatcher, E.G. Wagner, and J.B. Wright) was responsible for the all-out introduction of algebraic and categorical methods in Computer Science -- and the subsequent development of algebraic data types, module systems and algebraic specifications. In particular, Goguen et al. (1977) demonstrated how the initial algebra semantics unifies a great number of semantic formalisms, and elegantly answers the questions of what is syntax and what is semantics. Recently, algebraic effects put algebras into spotlight once again. The tagless-final approach is another application of algebras, very closely related to the initial algebra semantics.

The present web page in intended as a reference, to collect the definitions and standard results from universal algebra that are of most interest to computer scientists and especially tagless-final programmers. The overarching goal of being relevant to programming dictates the selection of the material and the choice of notation. We use only programming examples and a concrete programming language notation (namely, OCaml). The standard mathematical practice relies on a multitude of superscripts and subscripts and the extensive, sometimes confusing, overloading to avoid writing even more deeply nested subscripts. A programming-language notation is more regular, less ambiguous -- and can be `mechanically checked', by a compiler.

The fact that the OCaml module notation turns out adequate is not all surprising: Joseph Goguen has been a major influence in the design of the ML module system.

**References**- Martin Wirsing: Algebraic specifications

Handbook of Theoretical Computer Science B, 1990, J. van Leeuwen, Ed. Elsevier. pp 675-788

Comprehensive, but fairly mathematical and categorical. We borrow most definitions from it, changing the notation.Stanley Burris and H. P. Sankappanavar: A Course in Universal Algebra

Graduate Texts in Mathematics, 1981, v. 78 10.1007/978-1-4613-8130-3

Available online <http://www.math.uwaterloo.ca/~snburris/htdocs/UALG/univ-algebra2012.pdf>

The standard, detailed graduate text, for Math graduate students. Initial algebra is mentioned only as a remark, as a special case of free algebra with the empty set of generators.J.A. Goguen, J.W. Thatcher, E.G. Wagner, and J.B. Wright: Initial Algebra Semantics and Continuous Algebras

Journal of the ACM, Vol 24, No 1, January 1977, pp 68-95

This is the paper that properly introduced initial algebras in Computer Science, see particularly Sections 1-4.Bart Jacobs and Jan Rutten: A Tutorial on (Co)Algebras and (Co)Induction

EATCS Bulletin, 1997, 62, pp. 222--259

The tutorial, for computer scientists, explains algebras and initiality in detail and at a good slow pace. It demonstrates proofs by initiality as an alternative to inductive proofs -- often a simpler and clearer alternative. The tutorial uses a different presentation of Sigma-algebras: so-called F-algebras, relying on polynomial functors to represent signatures.Garrett Birkhoff: On the structure of abstract algebras

Proceedings of the Cambridge Philosophical Society, 1935, v31, 433-454

<http://math.hawaii.edu/~ralph/Classes/619/birkhoff1935.pdf>

The foundational paper of the field of Universal Algebraalgebra.ml [5K]

The complete OCaml code accompanying the article: the executable specification

- Birkhoff formally defined an (abstract) algebra as a class
`A`

, now called the carrier set, with a class of operations on it: each operation is associated with a set of sequences of elements of`A`

and maps each sequence from its associated set to some element of`A`

. We shall see what it means in concrete, programming terms in a moment.We will be working with so-called many-sorted algebras, with not one but several carrier sets. To tell them apart and conveniently refer to, each carrier set is associated with its own `sort'. One may think of the `sort' as a symbol that names a carrier set. For many-sorted algebras, it is customary to first define a signature -- the `type' of an algebra. Here is the formal definition, to be illustrated below. ``Formally, a (many-sorted algebraic) signature Sigma is a pair

`<S,F>`

where`S`

is a set (of sorts) and`F`

is a set (of function symbols) such that`F`

is equipped with the mapping`F \mapsto S^n \times S`

for some`n >=0`

. The mapping, for a particular`f`

of`F`

is often denoted as`f: s_1 ... s_n -> s`

where`{s,s_1,...,s_n} \subset S`

'' (Wirsing, 1990). The number`n`

is called the*arity*of`f`

. The operations of zero arity are called constants.Wirsing's definition is the straightforward generalization of Birkhoff's original definition to the many-sorted case (it is also a restriction: Birkhoff's definition admitted operations of infinite arity, and algebras whose carriers and operations are not just infinite sets but proper classes).

In programming terms, a many-sorted algebraic signature is a module signature. For example,

module type NAT = sig type nat val zero : nat val succ : nat -> nat val plus : nat * nat -> nat end

Here, the set of sorts`S`

is the singleton set`{nat}`

. The set`F`

has three elements:`{zero, succ, plus}`

and is equipped with the mappingzero \mapsto nat succ \mapsto nat \times nat plus \mapsto (nat \times nat) \times nat

That mapping is (more perspicuously) represented by the OCaml declarations:val zero : nat val succ : nat -> nat val plus : nat * nat -> nat

Thus `sort' is what in programming may be called `type'. (Joseph Goguen has remarked that `type' is too ambiguous a word and so `sort' has been chosen instead.) We shall continue to use the term `sort', however odd it may sound to an (OCaml) programmer.*Exercise:*give several examples of OCaml module signatures that are not algebraic signatures.With the signature Sigma thus defined, ``A Sigma-Algebra consists of an

`S`

-sorted family of non-empty (carrier) sets`{A_s}_{s\in S}`

and a*total*function`f^A: A_{s_1},\ldots,A_{s_n} -> A_s`

for each`f: s_1,\ldots,s_n -> s`

in`F`

.'' (Wirsing, 1990).Here is an example of a

`NAT`

-algebra:module NatUL = struct type nat = unit list let zero = [] let succ x = () :: x let plus (x,y) = x @ y end

Since`NAT`

has only one sort, the`NatUL`

algebra has only one carrier set, which is the set`{[], [()], [();()], ...}`

of`unit list`

s. The constant`zero`

is the empty list,`succ`

maps a list to a longer, by one`()`

, list; and`plus`

maps a pair of lists to the concatenated list. All these operations are total as required:`succ`

and`plus`

can handle any lists supplied as arguments, with no exceptions.Here is another

`NAT`

algebra:module NatBool : (NAT with type nat = bool) = struct type nat = bool let zero = false let succ x = not x let plus (x,y) = not (x = y) (* exclusive or *) end

Its carrier is the set of Booleans. We added the signature ascription to the`NatBool`

module so that the OCaml compiler could check that all operations required by the`Nat`

signature are defined. We have exposed the particular type of the carrier set (that is, the association between the abstract sort`nat`

and the concrete carrier type).From now on, we shall use the OCaml notation: OCaml signatures for Sigma signatures, and OCaml modules implementing the signature for the corresponding algebra.

- An algebra homomorphism is a mapping between two algebras
of the same signature: specifically, a mapping of the carriers of one
algebra to the corresponding carriers of the other algebra that is said
to `preserve operations'. Here what it means formally: let
`S`

be an algebraic signature (with sorts`s1`

,`s2`

, ...`sk`

and the operations`f1`

,`f2`

, ...`fm`

). Let`M1: S`

and`M2: S`

be two`S`

-algebras: two OCaml modules of that signature. A homomorphism`H12`

from`M1`

to`M2`

(notated as`H12: M1 ~> M2`

) is a collection of functions`h_s1,...,h_sk`

, one for each sort, which can be represented by the following OCaml signature:module H12 : sig val h_s1: M1.s1 -> M2.s1 val h_s2: M1.s2 -> M2.s2 ... val h_sk: M1.sk -> M2.sk end

The functions`h_si`

(`i=1..k`

) are non necessarily injective or `onto' -- but have to be total:`h_si : M1.si -> M2.si`

should be able to handle any value from the set`M1.si`

received as the argument. The functions`h_si`

must also `preserve the operations': that is, for every operation`f : s_1 ... s_n -> s`

of arity`n`

,h_s (M1.f (a_1, ..., a_n)) = M2.f (h_s1 a_1, ..., h_sn a_n)

for every`a_1 \in M1.s1, ... a_n \in M1.sn`

.There is always a homomorphism from any algebra to itself: the identity homomorphism, to be written as

`Id`

. It is the identity mapping on the carriers (which clearly preserves the operations).A bit more interesting is the homomorphism from

`NatUL`

to`NatBool`

:module HULtoBool : sig val h : NatUL.nat -> NatBool.nat end = struct let rec h = function | [] -> false | _::t -> not (h t) end

The operation preservation conditionsh NatUL.zero = NatBool.zero h (NatUL.succ x) = NatBool.succ (h x) h (NatUL.plus (x,y)) = NatBool.plus (h x,h y)

are clearly satisfied, for any`unit list`

values`x`

and`y`

, as one can easily see by unrolling the definitions of`h`

and the operations. The reader may want to see it for themself.*Exercise:*show that there is*no*homomorphism from`NatBool`

to`NatUL`

.*Exercise:*Consider yet another`NAT`

-algebra:module NatStr : (NAT with type nat = string) = struct type nat = string let zero = "Z" let succ x = "S" ^ x let plus (x,y) = "(" ^ x ^ "+" ^ y ^ ")" end

Are there any homomorphisms involving`NatStr`

and the earlier introduced algebras? Note that`NatStr`

's carrier is the set of all OCaml strings (which includes not only`"SZ"`

but also`"foo"`

). Is there any way to adjust`NatStr`

so that there is a homomorphism to`NatUL`

?Homomorphism is just a collection of functions mapping carriers of one algebra to the corresponding carriers of the other algebra. As functions, they may be composed. We use the symbol

`\cdot`

of functional composition also for the composition of homomorphisms.*Theorem:*if`H1: M1 ~> M2`

and`H2: M2 ~> M3`

are two homomorphisms, then their composition`H2 \cdot H1`

is also a homomorphism, from`M1`

to`M3`

.

Proof: clearly,`H2 \cdot H1`

maps the carriers of`M1`

to the carriers of`M3`

. As for operation preservation, for any`f : s_1,...,s_n -> s`

,(H2.hs \cdot H1.hs) M1.f(x_1,...,x_n) = H2.hs (H1.hs (M1.f(x_1,...,x_n))) = H2.hs (M2.f(H1.hs1 x_1,...,H1.hsn x_n)) = M3.f(H2.hs1 (H1.hs1 x_1),...,H2.hsn (H1.hsn x_n)) = M3.f((H2.hs1 \cdot H1.hs1) x_1,...,(H2.hsn \cdot H1.hsn) x_n)

If a homomorphism`H: M1~>M2`

is `onto' -- that is, every element of every carrier set of`M2`

is an image by`H`

of some element of an`M1`

carrier -- the algebra`M2`

is called a homomorphic image of`M1`

. For example, the homomorphism`HULtoBool`

is onto and`NatBool`

is hence a homomorphic image of`NatUL`

.If all carrier-mapping functions in a homomorphism

`H: M1 ~> M2`

are one-to-one (that is, injective and onto), the homomorphism is called isomorphism, and`M1`

and`M2`

isomorphic. The identity homomorphism`Id`

is in fact the isomorphism.*Theorem:*A homomorphism`H: M1 ~> M2`

is isomorphism if and only if there is also a homomorphism`H': M2 ~> M1`

such that`H \cdot H' = Id`

and`H' \cdot H = Id`

. (`H'`

is also isomorphism). The proof is left as an exercise.

- We have seen that an algebra homomorphism does not always exist. We
now construct an algebra from which there is always a homomorphism
to any other algebra of the same signature. Moreover, the homomorphism
is unique. We show the construction on the running example of the
`NAT`

signature. Let`TFc`

be the set of OCaml functors:module type TF = functor(N:NAT) -> sig val e : N.nat end

constructed as follows. The functormodule TFzero(N:NAT) = struct let e = N.zero end

is in`TFc`

. If a functor`T1`

is in`TFc`

, so ismodule TS(N:NAT) = struct let e = let module M1 = T1(N) in N.succ M1.e end

To lighten the notation, we shall write the above asmodule TS(N:NAT) = struct let e = N.succ T1(N).e end

(In the current version of OCaml, it is necessary to code`T(N).e`

as`let module M = T(N) in M.e`

; see the accompanying code for details.) If functors`T1`

and`T2`

are in`TFc`

, so ismodule TP(N:NAT) = struct let e = N.plus (T1(N).e, T2(N).e) end

Finally, nothing else is in`TFc`

.A different way to write an element of

`TFc`

is illustrated by the following sample:module TFN(N:NAT) = struct open N (* A term constructed using only the operations succ, zero and plus *) let e = plus (succ zero, succ (succ zero)) end

which should look very familiar to the readers who have encountered the tagless-final style.We turn

`TFc`

into a`NAT`

algebra by adding the operations in the obvious way:module TFC : (NAT with type nat = (module TF)) = struct type nat = (module TF) let zero = (module TFzero : TF) let succ (module T1:TF) : nat = (module (functor (N:NAT) -> struct let e = N.succ T1(N).e end)) let plus ((module T1:TF), (module T2:TF)) : nat = (module (functor (N:NAT) -> struct let e = N.plus (T1(N).e, T2(N).e) end)) end

The sample element`TFN`

shown earlier can now be written asmodule TFCsample : TF = (val let open TFC in plus (succ zero, succ (succ zero)))

For any`NAT`

algebra`N`

there exists a homomorphism from`TFC`

to that algebra:module HTFC(N:NAT) = struct let h : TFC.nat -> N.nat = fun (module T:TF) -> T(N).e end

In the following demonstration, let`N`

be an arbitrary`NAT`

algebra and let`h`

be`HTFC(N).h`

, that is,`fun (module T:TF) -> T(N).e`

. Clearly`h`

maps every element of the carrier`TFc`

(that is, every functor`TF`

) to some element of`N.nat`

. For example, the result of mapping`TFN`

is`TFN(N).e`

, which is the`N.nat`

value computed as follows, using the operations`zero`

,`succ`

and`plus`

of`N`

:let open N in let e = plus (succ zero, succ (succ zero))

Now that we have seen that`h`

is the total mapping, we verify that it preserves the operations:h TFC.zero = N.zero h (TFC.succ x) = N.succ (h x) h (TFC.plus (x,y)) = N.plus (h x, h y)

for every`x`

and`y`

in`TFc`

. Indeed, unrolling the definitionsh TFC.zero = h (module TFzero) = TFzero(N).e = N.zero h (TFC.succ x) = let (module T1:TF) = x in h (module (functor (N:NAT) -> struct let e = N.succ T1(N).e end)) = let (module T1:TF) = x in N.succ T1(N).e = N.succ (h x)

(the verification of the`plus`

preservation is left to the reader.) The banality of the proof is an indication that`TFC`

preserves the operations by its very construction.We now demonstrate that

`h`

is a unique homomorphism from`TFC`

to`N`

. Suppose there is another mapping, called`g`

, from`TFc`

to`N.nat`

that preserves operations. Since both`h`

and`g`

must preserve the`zero`

operation,h TFC.zero = N.zero = g TFC.zero

That is,`h`

and`g`

coincide on`TFC.zero`

. If`h`

and`g`

map some`t`

of`TFc`

to the same element of`NAT.nat`

, thenh (TFC.succ t) = N.succ (h t) = N.succ (g t) = g (TFC.succ t)

That is, they also have to agree on`TFC.succ t`

. The case of`TFC.plus`

is similar. By structural induction`h`

and`g`

coincide on all elements of`TFc`

. Thus,`h`

is unique.A Sigma-algebra with a unique homomorphism to any other algebra of the same signature is called

*initial algebra*.The

`TFc`

construction is standard, used already by Birkhoff to show the existence of initial algebras (actually, he talked about free algebras, of which initial algebras are a particular case.) The carrier constructed like`TFc`

is called `Herbrand universe' for the signature Sigma (cf. Herbrand universe and Herbrand basis in Logic Programming). The`TFC`

algebra itself is called word-algebra or ground-term algebra. The construction easily generalizes to the many-sorted case, giving:*Theorem:*For any signature Sigma whose Herbrand universe has a term of every sort, there exists an initial Sigma-algebra*Exercise:*`NatBool`

is not an initial`NAT`

-algebra (why?). Show that`NatUL`

is not an initial`NAT`

-algebra either. (Hint: show that there is no homomorphism from`NatUL`

to`TFC`

).*Exercise*(not entirely straightforward): Although`NatUL`

fails to be an initial`NAT`

-algebra, there is still an initial`NAT`

-algebra with the same carrier set, viz.`unit list`

. Construct it.*Exercise:*Carry out the initial`NAT`

algebra construction using functions instead of functors (the functions may take modules as arguments)*Theorem:*two initial algebras of the same signature are isomorphic

Proof: Let`M1`

and`M2`

be two initial algebras. Then there exist (the unique) homomorphisms`H12: M1 ~> M2`

and`H21: M2 ~> M1`

. Their composition`H21 \cdot H12: M1 ~> M1`

must be a homomorphism too. There is also the identity homomorphism`Id: M1 ~> M1`

. Since`M1`

is initial, there is only one homomorphism from it to another algebra, including itself. Therefore, the two previously mentioned homomorphisms from`M1`

to itself must be the same:`H21 \cdot H12 = Id`

. Likewise, we find that`H12 \cdot H21 = Id`

. Hence`H12`

(and`H21`

) are in fact isomorphisms. The proof relies on the uniqueness of homomorphisms from an initial algebra -- the so-called `universality property'. The tutorial by Jacobs and Rutten shows more proofs by initiality, which, they argue, are often more perspicuous than the corresponding proofs by induction.*Theorem:*An algebra isomorphic to an initial algebra is initial as well

Proof: a simple application of the homomorphism composition theorem.

- The word-algebra construction feels like a mindless shuffling of
function symbols, very `syntactic' -- which is exactly the point,
according to Goguen et al. (1977). They invited to think of a
signature Sigma as the grammar of a language, an initial Sigma-algebra
`S`

as the abstract syntax, and the other Sigma algebras`A`

as semantics of the language. ``The semantic function is the uniquely determined homomorphism`hA : S ~> A`

, assigning a meaning`hA(s)`

in`A`

to each syntactic structure`s in S`

'' -- that is, to each term in the language. That initial algebras of the same signature are isomorphic strengthens their claim to be the `abstract syntax': there may be multiple presentations of abstract syntax, but they are `essentially the same'.In our running example,

`NAT`

is the grammar of the tiny language for adding natural numbers;`TFc`

is the set of its terms (`TFN`

or`TFCsample`

being sample terms); the other`NAT`

algebras provide interpretations, or semantics:`NatUL`

is the unary number semantics,`NatBool`

is the parity semantics.``From this viewpoint it becomes clear that a major aspect of formal semantics (both practical and theoretical) is constructing intended semantic algebras for particular programming languages.'' (Goguen et al., (1977))

Tagless-final takes this to heart, and to the letter. Once the signature is decided, one can write sample terms like

`TFN`

right away. Implementations of the signature provide interpreters: semantics. Applying the`TFN`

functor to, say, the`NatUL`

module, amounts to interpreting the`TFN`

term, or computing its`NatUL`

-semantics.In fact, the very module that defines a

`NAT`

algebra (its carrier and operations), such as`NatUL`

, is also the module that implements an interpreter of tagless-final terms like`TFN`

-- that is, implements the homomorphism from`TFC`

. An algebra is hence literally defined by its homomorphism from the word-algebra.*Writing a tagless-final interpreter is defining an algebra, and vice versa.*

- Consider yet another algebra
module ADT = struct type nat = Z | S of nat | P of nat * nat let zero = Z let succ x = S x let plus (x,y) = P (x,y) end

As we saw in the tagless-final approach,`ADT`

is the homomorphism from`TFC`

. Moreover, its mapping from the`TFc`

to the data type`ADT.nat`

is injective and onto. Hence it is an isomorphism and`ADT`

is also an initial algebra.*Exercise:*show the homomorphism from`ADT`

to`TFC`

, which must exist.Although

`TFC`

and`ADT`

are isomorphic and hence `essentially the same', there may still be useful presentation differences between them. After all, two programs that produce the same outputs for all the same inputs are also `essentially the same'. Yet there may be many reasons to prefer one over the other: one program may be faster, smaller, written in a familiar language, easier to maintain and extend, etc.