1 Introduction↩︎

Consider a puzzle about sorting, inspired by Dijkstra’s Dutch National Flag problem [1]. Suppose there are balls of three colours, corresponding to the colours of the Dutch flag: red, white, and blue. Given an unordered list (bag) of such balls, how many ways can you sort them into the Dutch flag? \[\bag{ \tikz[anchor=base, baseline]{ \foreach \x/\color in {1/red,2/red,3/blue,4/white,5/blue,6/red,7/white,8/blue} { \node[circle,draw,fill=\color,line width=1pt] at (\x,0) {\phantom{\tiny\x}}; \ifthenelse{\NOT 1 = \x}{\node at ({\x-0.5},0) {,};}{} } } }\] Obviously there is only one way, decided by the order the colours appear in the Dutch flag: \(\term{red} < \term{white} < \term{blue}\). \[[ \tikz[anchor=base, baseline]{ \foreach \x/\color in {1/red,2/red,3/red,4/white,5/white,6/blue,7/blue,8/blue} { \node[circle,draw,fill=\color,line width=1pt] at (\x,0) {\phantom{\tiny\x}}; \ifthenelse{\NOT 1 = \x}{\node at ({\x-0.5},0) {,};}{} } } ]\] What if we are avid enjoyers of vexillology who also want to consider other flags? How many ways can we sort our unordered list? To answer this, we distinguish between a sorting algorithm (a computational procedure) and a sorting function (a mathematical mapping). Since we sort the elements of a carrier set \(A\) directly (so stability and metadata are not concerns), a sorting function must produce a unique, deterministic output list for each input bag. Thus, “how many ways to sort” means how many extensionally distinct sorting functions can be defined. Because there are \(3! = 6\) permutations of \(\{\term{red}, \term{white}, \term{blue}\}\), there are 6 possible orderings, corresponding to 6 categories of tricolour flags (see Wikipedia):

For a carrier set with 3 elements, the 6 possible total orderings yield exactly 6 extensionally correct sorting functions. Intuitively, a correct sorting function takes a bag and returns a unique, sorted list of the same elements. Extensional correctness therefore requires the output list to be a permutation of the input elements, and sorted according to a fixed total order. Formally, there is a bijection between total orderings on a carrier set \(A\) and correct sorting functions on lists over \(A\). Our main contribution is showing how a sorting function can be correctly axiomatised and formalised from this point of view.

Outline and Contributions

The paper is organised as follows:

These sections are largely independent. Readers interested in universal algebra can start at 2; those focused on free (commutative) monoids can skip to [sec:monoids] [sec:commutative-monoids]; and those interested primarily in sorting can proceed directly to 5. All results are formalised in Cubical Agda, available online at [2]. We use informal mathematical language in the paper to keep it accessible. An extended version with additional details is on arXiv [3].

No prior exposure to Homotopy Type Theory (HoTT) or Univalence is required. We assume only basic familiarity with dependent type theory and functional programming (such as Agda, Coq, or Haskell). While the formalisation is written in Cubical Agda and uses higher inductive types and univalence for quotient constructions, the paper’s text is presented in informal mathematical language.

2 Universal Algebra↩︎

We develop some basic notions from universal algebra and equational logic [4], which gives us a vocabulary and framework to express our results in. The point of view we take is the standard category-theoretic approach to universal algebra [5], which is an alternative perspective to the Lawvere theory or abstract clone point of view [6], lawvereFunctorialSemanticsAlgebraic1963?. We keep a running example of monoids in mind, while explaining and defining the abstract concepts.

2.1 Algebras↩︎

Every signature \(\sig\) induces a signature functor \(\Sig\) on \(\Set\).

A \(\sig\)-structure is given by a carrier set, with functions interpreting each operation symbol. The signature functor applied to a carrier set gives the inputs to each operation, and the output is simply a map back to the carrier set. These two pieces of data constitute an algebra for the \(\Sig\) functor. We write \(\str{X}\) for a \(\sig\)-structure with carrier set \(X\), following the model-theoretic notational convention.

For a fixed signature \(\sig\), the category of \(\Sig\)-algebras and their morphisms form a category of algebras, written \(\SigAlg\), or simply, \(\sigAlg\), given by the obvious definitions of identity and composition for the underlying functions.

2.2 Free Algebras↩︎

The concrete category \(\sigAlg\) of structured sets and structure-preserving maps admits a forgetful functor \(U : \sigAlg \to \Set\). In our notation, \(U(\str{X})\) is simply \(X\), a fact we exploit to simplify our notation and formalisation. The left adjoint to this forgetful functor is the free algebra construction, also known as the term algebra or the absolutely free algebra without equations [7]. We rephrase this in more concrete terms.

In other words, we ask for a bijection between the set of homomorphisms out of the free algebra to any other algebra, and the set of functions from the carrier set of the free algebra to the carrier set of the other algebra. There should be no more data in homomorphisms out of the free algebra than there is in functions out of the carrier set, which is the property of freeness. The inverse operation to post-composing with \(\eta_X\) extends a function to a homomorphism.

Free algebra constructions are canonically equivalent.

We have discussed specifications of free algebras, but not actually given a construction. In type theory, free constructions are often given by inductive types, where the constructors are the pieces of data that freely generate the structure, and the type-theoretic induction principle enforces the category-theoretic universal property.

The constructors and are the generators for the universal map, and the algebra map, respectively. Together, they describe the type of abstract syntax trees for terms in the signature \(\sig\) – the leaves are the free variables, and the nodes are the branching operations of the tree, marked by the operations in \(\sig\).

2.3 Equations↩︎

The algebraic framework described so far only captures operations, not equations. These algebras are lawless (or wild or absolutely free) – \(\SigMon\)-algebras are premonoids rather than monoids, and \(\str{F}_{\sigMon}\)-algebras are free premonoids, not free monoids, since they are missing the unit and associativity laws.

To impose equations on the generated abstract syntax trees, we adopt the point of view of equational logic.

This will be used to define a system of equations (10).

Similar to the term signature functor in 2, this produces a term arity functor on \(\Set\).

To build equations out of this, we use the \(\sig\)-operations and construct trees for the left and right-hand sides of each equation using the free variables available.

Finally, we say how a given \(\sig\)-structure \(\str{X}\) satisfies the system of equations \(T_{(\sig,\eqsig)}\). We need to assign a value to each free variable in the equation in the carrier set, using a valuation function \(\rho : V \to X\). Given such an assignment, we evaluate the left and right trees of the equation, by extending \(\rho\,\) with 6, that is by construction, a homomorphism from \(\str{F}(V)\) to \(\str{X}\). To satisfy an equation, these two evaluations should agree.

Given a signature \((\sig,\eqsig)\) with a system of equations \(T_{(\sig,\eqsig)}\), the \(\sig\)-algebras satisfying \(T_{(\sig,\eqsig)}\), or varieties, form a full subcategory of \(\sigAlg\). While free algebras exist for any signature \(\sig\) as in [def:free-algebra-construction], constructions of free varieties for arbitrary systems of equations require non-constructive principles [8], in particular, the arity sets need to be projective – we do not pursue this matter further. We have a rudimentary framework for universal algebra and equational logic, which gives us enough tools to develop the next sections.

3 Constructions of Free Monoids↩︎

In this section, we consider various constructions of free monoids in type theory, with proofs of their universal property. Since each construction satisfies the same categorical universal property, by [lem:free-algebras-unique], these are canonically equivalent (hence equal, by univalence) as types (and as monoids), allowing us to transport proofs between them. There are countably many such representations of free monoids, allowing us to choose the most convenient one for a given task. Using the universal property allows us to define and prove our programs correct in one go, which we use in 5.

3.1 Lists↩︎

Cons-lists are simple inductive datatypes, well-known to functional programmers, and are a common representation of free monoids in programming languages. More generally, they correspond to list objects [9], [10] and algebraically-free monoids [11] in category theory.

The (universal) generators map is the singleton: \(\eta_A(a) \defeq [a] \jdgeq a \cons \nil\), the identity element is the empty list , and the monoid multiplication \(\mult\) is given by list concatenation.

3.2 Arrays↩︎

An alternate (non-inductive) representation of the free monoid on a carrier set, or alphabet \(A\), is \(A^{\ast}\), the set of all finite strings or sequences of characters drawn from \(A\), as in [12]. We call this an array, which is a pair of a natural number \(n\), denoting the length of the array, and a lookup (or index) function \(\Fin[n] \to A\), mapping indices to elements of \(A\). In type theory, this is also understood as an extension of a container [13], where the type of shapes is a \(n\colon\Nat\), and the type of positions for each shape is \(\Fin[n]\), where the array elements are stored.

For example, \((3, \lambda\{ 0 \mapsto 3, 1 \mapsto 1, 2 \mapsto 2 \})\) represents the same list as \([3, 1, 2]\). The (universal) generators map is the singleton: \(\eta_A(a) = (1, \lambda\{ 0 \mapsto a \})\), the identity element is \((0, \lambda\{\})\) and the monoid operation \(\mult\) is given by array concatenation.

We need two auxiliary lemmas about array concatenation to do induction on arrays.

An alternative proof of the universal property for \(\Array\) can be given by directly constructing an equivalence (of types, and monoid structures) between \(\Array(A)\) and \(\List(A)\) (using \(\term{tabulate}\) and \(\term{lookup}\)), and then applying univalence and transport (see formalisation).

4 Constructions of Free Commutative Monoids↩︎

The next step is to add commutativity to the monoid multiplication in each construction of free monoids. Informally, adding commutativity to free monoids turns “ordered lists” to “unordered lists”, where the ordering is the one imposed by the position or index of the elements in the list. This is crucial to our goal of studying sorting, as we will study sorting as a function mapping back unordered lists to ordered lists, later in 5.3.

It is known that finite multisets are (free) commutative monoids, under the operation of multiset union: \(\xs \cup \ys = \ys \cup \xs\). The order is “forgotten” in the sense that it doesn’t matter how two multisets are union-ed together, such as, \(\bag{a, a, b, c}\) and \(\bag{b, a, c, a}\) are equal as finite multisets (justifying the bag notation). Formally, \(\bag{x,y,\dots}\) denotes \(\eta_A(x) \mult \eta_A(y) \mult \dots : \MM(A)\).

This is unlike free monoids, where \([a, a, b, c] \neq [b, a, c, a]\) (justifying the list notation). Formally, \([x, y, \dots]\) denotes \(\eta_A(x) \mult \eta_A(y) \mult \dots : \LL(A)\), and \(x \cons xs\) denotes \(\eta_A(x) \mult xs : \LL(A)\).

4.1 Free monoids quotiented by permutation relations↩︎

Instead of constructing free commutative monoids directly, the first construction we study is to take any free monoid and quotient by symmetries. The constructions in 4.2 and 4.4 are specific instances of this recipe.

From the perspective of universal algebra and equational logic developed in 2, we work in the signature of monoids, but extend the equational theory of monoids with commutativity. If \((\str{F}(A), \eta)\) is a free monoid construction satisfying its universal property, then we quotient \(F(A)\) by an appropriate symmetry relation \(\approx\). This is precisely a permutation relation.

Note that being a permutation relation is a proposition. We write \(\quot{F(A)}{\approx}\) for the quotient of \(F(A)\) by \(\approx\), with the inclusion map \(q: F(A) \twoheadrightarrow \quot{F(A)}{\approx}\). The generators map into \(\quot{F(A)}{\approx}\) is given by \(q \comp \eta_A\), the identity element is \(\qlift{e} = q(e)\), and the multiplication operation \(\mult\) is lifted to \(\qlift{\mult}\) in the quotient by congruence.

The monoid extension operation of \(F(A)\), denoted \(\ext{(\blank)}\), lifts to an extension operation for commutative monoids, for \(\quot{F(A)}{\approx}\), which we denote by \(\exthat{(\blank)}\).

4.2 Lists quotiented by permutation relations↩︎

A specific instance of this construction is \(\List\) quotiented by a concrete permutation relation to get commutativity. Of course, there are many permutation relations in the literature, we consider a simple one which swaps any two adjacent elements anywhere in the middle of the list. This \(\PList\) construction has also been considered in [14], who prove that \(\PList\) is equivalent to the free commutative monoid (constructed as a HIT). We give a direct proof of its universal property using our generalisation.

By 4.1, to obtain that \(\PList(A)\) is the free commutative monoid on \(A\), it suffices to prove the property of \(\Perm(A)\) being a permutation relation.

\(\PList\) being a quotient of \(\List\) makes it easy to lift functions and properties defined on \(\List\) along the quotient map. The inductive nature of \(\Perm\) makes it easy to define algorithms that inductively rearrange elements in a list, such as insertion sort. This property also makes it possible to normalize inductively constructed list elements in \(\PList\) to their simplest forms, e.g. \(q([ x ]) \mult q([y, z])\) normalizes to \(q([x,y,z])\) by definition, saving the efforts of defining auxiliary lemmas to prove their equality.

This inductive nature, however, makes it difficult to define efficient operations on \(\PList\). Consider a divide-and-conquer algorithm such as merge sort, which involves partitioning a \(\PList\) of length \(n+m\) into two smaller \(\PList\) of length \(n\) and length \(m\). We must iterate all \(n\) elements before we can make such a partition, thus making \(\PList\) unintuitive to work with when we want to reason with operations that involve arbitrary partitioning.

4.3 Swap Lists↩︎

Informally, quotients are defined by generating all the points, then quotienting out into equivalence classes by the congruence relation. Alternately, HITs use generators (points) and higher generators (paths) (and higher higher generators and so on…). We can also define free commutative monoids using HITs where adjacent swaps generate all symmetries, for example swap-lists taken from [15], and in the Cubical library [16].

We refer the reader to [15] or the Cubical Agda library [16] for further details. Much like \(\List\), \(\SList\) is inductively defined, therefore making it intuitive to reason with when defining inductive operations or proofs on \(\SList\), but difficult to reason with when defining operations that involve arbitrary partitioning, for reasons similar to those given in 4.2.

4.4 Bag↩︎

Alternatively, we can also quotient the \(\Array\) type by symmetries to get commutativity. This construction has been considered in [17] and [18], partially considered in [15], and in [14], who give a similar construction, where only the index function is quotiented, instead of the entire array. [19] also considered \(\Bag\) as a setoid relation on \(\List\) in an intensional MLTT setting. [14] prove that their version of \(\Bag\) is the free commutative monoid by equivalence to the other HIT constructions. We give a direct proof of its universal property instead, using our general recipe.

Note that by a pigeonhole argument, \(\sigma\) may only be constructed when \(n = m\). In other words, we are quotienting by an automorphism on the indices, and its action on the elements. We have already shown \(\Array\) to be the free monoid in 3.2. By [prop:qfreemon], to obtain that \(\Bag(A)\) is the free commutative monoid on \(A\), it suffices to prove the property of \(\approx\) being a permutation relation.

To show that \(\ext{f}\) is invariant under permutation: for all \(\phi\colon \Fin[n]\xto{\sim}\Fin[n]\), \(\ext{f}(n, i) \id \ext{f}(n, i \circ \phi)\), we need some formal combinators for punching in and punching out indices. These operations are borrowed from [21] and developed further in [20] for studying permutation codes.

Unlike \(\PList\) and \(\SList\), \(\Bag\) and its underlying construction \(\Array\) are not inductively defined, making it difficult to do induction on them. For example, in the proof of [array:univ], both [array:eta-suc] [array:split] are needed to do induction on \(\Array\), as opposed to \(\List\) and its quotients, where we can do induction simply by pattern matching. Much like \(\PList\), when defining functions on \(\Bag\), we need to show they respect \(\approx\), i.e. \(\as \approx \bs \to f(\as) = f(\bs)\). Notably, this is much more difficult than \(\PList\) or \(\SList\) – with \(\PList\) and \(\SList\) we only need to consider swapping adjacent elements, while with \(\Bag\) we need to consider all possible permutations. For example, in the proof of 2, we need to first construct a \(\tau\) which satisfies \(\tau(0) = 0\) and prove \(\ext{f}(n, i \comp \sigma) = \ext{f}(n, i \comp \tau)\) before we can apply induction.

5 Sorting Functions↩︎

We will now put to work the universal properties of our types of (ordered) lists and unordered lists, to define operations on them systematically, which are mathematically sound, and then reason about them. First, we explore definitions of various operations on both free monoids and free commutative monoids. By univalence (and the structure identity principle [23], [24]), everything henceforth holds for any presentation of free monoids and free commutative monoids. We use \(\FF(A)\) to denote the free monoid or free commutative monoid on \(A\), \(\LL(A)\) to exclusively denote the free monoid construction, and \(\MM(A)\) to exclusively denote the free commutative monoid construction.

For example \(\term{length}\) is a common operation defined inductively for \(\List\), but usually, properties about \(\term{length}\), such as, \(\term{length}(\xs \mult \ys) = \term{length}(\xs) + \term{length}(\ys)\), are proven separately after defining it. In our framework of free algebras, where the \(\ext{(\blank)}\) operation is a correct-by-construction homomorphism, we can define operations like \(\term{length}\) directly by universal extension, which also gives us a proof that they are homomorphisms for free. A further application of the universal property is to prove that two different types (such as lists and arrays) are equal, by showing they both satisfy the same universal property as in [lem:free-algebras-unique], which is desirable especially when proving a direct equivalence between the two types turns out to be a difficult exercise in combinatorics.

5.1 Prelude↩︎

Any presentation of free monoids or free commutative monoids has a \(\term{length} : \FF(A) \to \Nat\) function, where \(\Nat\) carries the additive monoid structure \((0,+)\), which is also a commutative monoid structure since addition is commutative.

Further, any presentation of free monoids or free commutative monoids has an element membership predicate \({\blank\in\blank} : A \to \FF(A) \to \hProp\), for any set \(A\). Here, we use the fact that \(\hProp\) forms a (commutative) monoid under disjunction and falsehood \((\bot, \vee)\).

\(\yo\) is formally the Yoneda map under the “types are groupoids” correspondence, where \(x:A\) is being sent to its representable in the Hom-groupoid (formed by the identity type), of type \(\hProp\). Note that the proofs of (commutative) monoid laws for \(\hProp\) use equality, which requires the use of univalence (or at least, propositional extensionality). By construction, this membership predicate satisfies its homomorphic properties, which are colloquially the properties of inductively defined de Bruijn indices.

We note that \(\hProp\) is actually one type level higher than \(A\). To make the type levels explicit, \(A\) is of type level \(\ell\), and since \(\hProp_\ell\) is the type of all types \(X : \Set_\ell\) that are mere propositions, \(\hProp_\ell\) has type level \(\ell + 1\). We do not assume any propositional resizing axioms [25], and instead use Agda’s universe polymorphism in our formalisation to accommodate this.

Any presentation of free (commutative) monoids \(\FF(A)\) also supports the \(\term{Any}\) and \(\term{All}\) predicates, which allow lifting a predicate \(A \to \hProp\) (on \(A\)), to any or all elements of \(\xs : \FF(A)\), respectively. We note that \(\hProp\) forms a (commutative) monoid in two different ways: \((\bot,\vee)\) and \((\top,\wedge)\) (disjunction and conjunction), which are the two different ways of getting \(\term{Any}\) and \(\term{All}\), respectively, by extension.

Note that Cubical Agda has problems with indexing over HITs [26], [27], hence it is preferable to program with our universal properties, such as when defining \(\term{Any}\) and \(\term{All}\), because the indexed-inductive definitions of these predicates get stuck on \(\term{transp}\) terms.

There is a \(\term{head}\) function on lists, which is a function that returns the first element of a non-empty list. Formally, this is a monoid homomorphism from \(\LL(A)\) to \(1 + A\).

This monoid operation \(\oplus\) is not commutative, since swapping the input arguments to \(\oplus\) would return the leftmost or rightmost element. To make it commutative would require a canonical way to pick between a choice of two elements – this leads us to the next section.

5.2 Total orders↩︎

First, we recall the axioms of a total order or linear order \(\leq\) on a set \(A\).

Note that either-or means a (truncated) logical disjunction. In the context of this paper, we want to make a distinction between “decidable total order” and “total order”. The decidability axiom strengthens the totality axiom, where we have either \(x \leq y\) or \(y \leq x\) merely as a proposition, but decidability allows us to produce a witness if \(x \leq y\) is true.

We also recall the axioms of a strict total order \(<\) on \(A\).

We can show that giving a decidable strict total order structure on \(A\) is equivalent to giving a decidable total order structure on \(A\). In practice, however, this equivalence is thoroughly awful to work with in a proof assistant, leading to horrible goals when formalising proofs that shift between these representations.

An equivalent way of defining a total order is using a binary meet operation, without starting from an ordering relation.

Finally, tying this back to 27, we have the following for free commutative monoids.

5.3 Sorting functions↩︎

The free commutative monoid is also a monoid, hence, there is a canonical monoid homomorphism \(\quotient : \LL(A) \to \MM(A)\), which is given by \(\ext{\eta_A}\), the extension of the unit \(\eta_A : A \to \MM(A)\). Since \(\MM(A)\) is (upto equivalence), a quotient of \(\LL(A)\) by symmetries (or a permutation relation), it is a surjection (in particular, a regular epimorphism in \(\Set\) as constructed in type theory), the canonical inclusion into the quotient. Concretely, \(\quotient\) simply includes the elements of \(\LL(A)\) into equivalence classes of lists in \(\MM(A)\), which “forgets” the order that was imposed by the indexing of the list.

Classically, assuming the Axiom of Choice would allow us to construct a section (right-inverse, in \(\Set\)) to the surjection \(\quotient\), that is, a function \(\ssection : \MM(A) \to \LL(A)\) such that \(\forall x.\, \quotient(\ssection(x)) \id x\). Or in informal terms, given the surjective inclusion into the quotient, a section (uniformly) picks out a canonical representative for each equivalence class. The core question we want to study is the existence of \(\ssection\) in a constructive setting, or equivalently, whether the order factored out by the symmetry quotient can be constructively recovered.

Viewing the quotienting relation as a permutation relation (from 4.1), a section \(\ssection\) to \(\quotient\) has to pick out canonical representatives of equivalence classes generated by permutations. Using \(\SList\) as an example, \(\ssection(x \cons y \cons \xs) \id \ssection(y \cons x \cons \xs)\) for any \(x, y : A\) and \(\xs : \SList(A)\), by \(\term{swap}\). Since \(\forall \xs.\,\quotient(\ssection(\xs)) \id \xs\), \(\ssection\) must preserve all the elements of \(\xs\). It cannot be a trivial function such as \(\lambda\,\xs. []\) – it must produce a permutation of the elements of \(\xs\). But to place these elements side-by-side in the list, \(\ssection\) must somehow impose an order on \(A\) (invariant under permutation), turning unordered lists of \(A\) into ordered lists of \(A\). Axiom of Choice (AC) giving us a section \(\ssection\) to \(\quotient\) “for free” is analagous to how AC implies the well-ordering principle, which states every set can be well-ordered. Thus, if AC was assumed, we could easily recover an order on \(A\) from the section \(\ssection\). Instead we study how to constructively define such a section, and in fact, that is exactly the extensional view of a sorting algorithm, and the implications of its existence is that \(A\) can be ordered, or sorted.

5.3.1 Section from Order↩︎

5.3.2 Order from Section↩︎

The previous section allowed us to construct a section, but an arbitrary section may not be a sorting function. To show a section is indeed a sort function, we need to show the section imposes some total order on \(A\) which it sorts by. Indeed, just by the virtue of \(\ssection\) being a section, we can almost construct a total-order on the carrier set.

Recall that the head homomorphism \(\term{head} \defeq \ext{\inr} : \LL(A) \to 1 + A\) (as in 27) is defined by equipping \(1 + A\) with a monoid structure with unit \(e \defeq \inl(\ttt)\) and multiplication defined as \(\inl(\ttt) \oplus b \defeq b\) and \(\inr(a) \oplus b \defeq \inr(a)\), which picks out the first (leftmost) element of a list. Here, we take the two-element bag \(\bag{x, y}\), “sort” it by \(\ssection\), and test if the \(\term{head}\) element is \(x\). Note, this is equivalent to \(x \leqs y \defeq s\bag{x, y} = [x,y]\), because \(\ssection\) preserves length, and the second element is forced to be \(y\).

A crucial observation is that \(\ssection\) correctly orders 2-element bags, but it does not necessarily sort bags with 3 or more elements.

To make sure that \(\ssection\) is a well-behaved section that recovers a total order on \(A\), we will enforce additional constraints on the image of \(\ssection\).

If \(\ssection\) were a sort function, the image of \(\ssection\) would be the set of \(\ssection\)-“sorted” lists, therefore \(\inimage{\xs}\) would imply \(\xs\) is a correctly \(\ssection\)-“sorted” list. First, we note that the 2-element case is correct.

Then, we state the first axiom on \(\ssection\).

There are two different membership symbols in this axiom, where the first membership is list membership from 25, and the second membership is image membership from 33. The \(\in\) symbol is intentionally overloaded to make the axiom look like a logical “cut” rule, that pushes the (least) \(x\) element to the head of the list. Informally, the head of an \(\ssection\)-“sorted” list is always the least element of the list.

5.3.3 Embedding orders into sections↩︎

Following from [sort:almost-order] [sort:trans], and [prop:order-to-sort-head-least], we have shown that a section \(\ssection\) that satisfies \(\isheadleast\) produces a total order \(x \leqs y \defeq \term{least}(\bag{x, y}) \id \inr(x)\), and a total order \(\leq\) on the carrier set produces a section satisfying \(\isheadleast\), constructed by sorting with \(\leq\). This constitutes an embedding of decidable total orders into sections satisfying \(\isheadleast\).

5.3.4 Equivalence of order and sections↩︎

We want to improve the embedding to an isomorphism, and it remains to show that we can turn a section satisfying \(\isheadleast\) to a total order \(\leqs\), then reconstruct the same section from \(\leqs\). Unfortunately, \(\isheadleast\) is not enough to guarantee this.

Therefore, we need to introduce a second axiom of sorting.

This says that \(\ssection\)-“sorted” lists are downwards-closed under cons-ing, that is, the tail of an \(\ssection\)-“sorted” list is also \(\ssection\)-“sorted”. To prove the correctness of our axioms, first we need to show that a section \(\ssection\) satisfying \(\isheadleast\) and \(\istailsort\) is equal to insertion sort parameterized by the \(\leqs\) constructed from \(\ssection\). In fact, the axioms we have introduced are equivalent to the standard inductive characterisation of sorted lists, found in textbooks, such as in [28].

Note that \(\isSorted_{\leq}(\xs)\) is a proposition for every \(\xs\), and forces the list \(\xs\) to be permuted in a unique way. This predicate is equivalent to the standard \(\type{Sorted}\) relation in the Agda standard library [22], which is defined pairwise using the more general \(\type{Linked}\) relation (i.e., \(\type{Sorted}(\xs) \defeq \type{Linked}(\blank\leq\blank, \xs)\)). Indeed, many of these definitions are traditional constructions that are completely independent of univalence or cubical features.

Insertion sort by \(\leq\) always produces lists that satisfy \(\isSorted_{\leq}\). Sections that also produce lists satisfying \(\isSorted_{\leq}\) are equal to insertion sort by function extensionality.

Finally, this gives us the correctness property of our axioms.

We can now state and prove our main theorem.

The sorting axioms we have come up with are abstract properties of functions. As a sanity check, we can verify that the colloquial correctness specification of a sorting function (starting from a total order) matches our axioms. We use the correctness criterion developed in [27].

6 Discussion↩︎

We conclude by discussing some high-level observations, related work, and future directions.

The paper uses informal type theoretic language, and is accessible without understanding any details of the formalisation. However, the formalisation is done in Cubical Agda, which has a few differences and shortcomings, that cause certain details to be more verbose than they are in informal type theory.

For simplicity we omitted type levels in the paper, but our formalisation has many verbose uses of universe levels due to Agda’s universe polymorphism. Similarly, h-levels were restricted to sets in the paper, but the formalisation is parameterised in many places for any h-level (to facilitate future generalisations). The free algebra framework currently only works with sets. Due to issues of regularity, certain computations only hold propositionally, and the formalisation requires proving auxiliary \(\beta\) and \(\eta\) computation rules in some places.

One of the contributions of our work is a rudimentary framework for universal algebra in a more categorical style, which lends itself to an elegant formalisation in type theory. This framework may be improved and generalised from sets to groupoids, using a system of coherences on top of a system of equations, to talk about 2-algebraic structures on groupoids, such as monoidal groupoids, symmetric monoidal groupoids, and so on.

The construction of finite multisets and free commutative monoids in type theory has a long history, and various authors have different approaches to it. We refer the reader to the discussions in [14], [15] for a detailed survey of these constructions. Our work, in particular, was motivated by the colloquial observation that: “there is no way to represent free commutative monoids using inductive types”. From the categorical point of view, note that the free monoid functor on \(\Set\) is polynomial, but the free commutative monoid endofunctor is not polynomial, since it only weakly preserves pullbacks. Various authors have given clever encodings of free commutative monoids using inductive types by adding assumptions on the carrier set – in particular, the assumption of total ordering on the carrier set leads to the construction of “fresh-lists”, by [29], which forces the canonical sorted ordering on the elements of the finite multiset.

It is worth noting that in programming practice, it is usually the case that all user-defined types have some sort of total order enforced on them, either because they’re finite, or because they can be canonically enumerated. Under these assumptions, the construction of fresh lists is a very reasonable way to represent free commutative monoids, or finite multisets.

The free monoid and free commutative monoid constructions can be categorified to free monoidal categories and free symmetric monoidal categories, respectively. In type theory, these types can be groupoidified to free monoidal groupoids and free symmetric monoidal groupoids, using the groupoid structure of identity types. This is a natural next step, and its connections to assumptions about total orders on the type of objects would be an important direction to explore.

Sorting is a classic problem in computer science – the programming point of view of sorting and its correctness has been studied by various authors. The simplest view of sorting is a function \(\term{sort}: \LL(\Nat) \to \LL(\Nat)\), which permutes the list and outputs an ordered list, which is studied in [28]. Fundamentally, this is a very extrinsic view of program verification, which is commonly used in program verification and proof assistants, and further, a special case of a more general sorting algorithm.

Henglein [30] studies sorting functions abstractly, without requiring a total order on the underlying set. He considers sorting functions as functions on sequences (lists), and recovers the order by applying a “sorting function” on an \(n\)-element list, and looking up the position of the elements to be compared. Unlike our approach, he does not factorize sorting functions through free commutative monoids. Henglein also studies sorting on preorders where antisymmetry may not hold, whereas we have only considered total orders in this paper. We are able to give a more refined axiomatisation of sorting because we consider permutations explicitly, and work in a constructive setting (using explicit assumptions about decidability), and which is an improvement over previous work.

Another intrinsic view of correctness of sorting has been studied in [31] using bialgebras, which was further expanded in [27] with an accompanying formalisation in Cubical Agda, that matches our point of view, as explained in [prop:sort-correctness]. However, their work is not just about extensional correctness of sorting, but also deriving various sorting algorithms starting from bialgebraic semantics and distributive laws. Our work is complementary, in that we are not concerned with the computational content of sorting, but rather the abstract properties of sorting functions, which are independent of a given ordering. It is unclear whether the abstract property of sorting functions can be combined with the intrinsic complexity of sorting algorithms – and that is a direction for future work.

Although we only talk about sorting lists and bags, the same ideas can be applied to other inductive types (polynomial functors) such as trees. We speculate that this could lead to some interesting connections with sorting (binary) trees, and constructions of (binary) search trees, from classical computer science.

References↩︎