This implements, in Agda, a framework of composable datatype refinements and relational algebraic ornamentation based on McBride's work on ornaments, and forms the basis of the author's DPhil dissertation.

All files have been typechecked with Agda 2.5.2 and Standard Library 0.13.

See the author's (old) homepage for more information, including published papers.

Basic definitions of categories, functors, and natural transformations. The collection of objects in a category is an Agda set, i.e., equality on objects is definitional equality, whereas the collection of arrows is a setoid, i.e., a set equipped with an equivalence relation. All operations on morphisms must respect the equivalence relation, including the morphism maps of functors.

Categorical definition of isomorphisms, parametrised by an underlying category. Isomorphic objects form a setoid and are amenable to equational reasoning. It is proved here that terminal objects are isomorphic. A predicate saying that a morphism is part of an isomorphism is also provided.

Isomorphisms are preserved by functors.

If each of the components of a natural transformation from F to G is part of an isomorphism, then F and G are naturally isomorphic.

A pullback is defined to be a terminal object in the category of spans over a slice category. Any two pullback objects are isomorphic. Pullback preservation and reflection of functors are also defined. A functor preserves pullback if it preserves a particular pullback.

The Midpoint Lemma: Let X, Y, Z be objects of a category C, and X × Y, X × Z, Y × Z, and (X × Y) × Z be products. Then (X × Y) × Z is a pullback of the projections X × Z → Z and Y × Z → Z.

Definition of slice categories.

The forgetful functor from a slice category to its underlying category is pullback-preserving.

Definition of span categories. Products and product preservation are also defined here.

A "weak" category of categories, in which morphisms (i.e., functors) are considered equal if they are naturally isomorphic. An equivalence of categories is an isomorphism in this weak category of categories.

This module defines the J rule for propositional equality, a generalised K rule for heterogeneous equality, and a predicate specifying when an element of a setoid is the unique inhabitant of the setoid.

This module defines pointwise equality of functions, which forms a setoid, and pointwise heterogeneous equality of functions. The category Fun of sets and functions is also defined here. The unit type is proved to be terminal in Fun.

The category Fam of families of sets. An isomorphism between two families of sets in Fam can be broken into isomorphisms between corresponding sets in the two families. There is a canonical way of forming pullbacks in Fam, namely taking the set-theoretical pullbacks of the index set and corresponding sets in the families. The forgetful functor from Fam to Fun preserves this pullback, and is hence pullback-preserving.

Various ways to construct isomorphisms in Fun.

Definition of inverse images of a function, and definitions of set-theoretic pullbacks in terms of inverse images and quotients.

Converse of preorders, setoids derived from preorders, implication as a preorder, and indirect reasoning combinators.

Auxiliary operations for dependent pairs.

Definition of refinements, swaps, and upgrades.

Families of refinements form a category FRef.

Definition of datatype descriptions, i.e., a universe for functors on families of sets. Datatype-generic fold and induction are defined on top of descriptions.

Horizontal data, which can be separated into "shape" and "core" (cf. containers), and shape equivalence.

Definition of ornaments, i.e., a universe for simple, structural natural transformations between functors decoded from descriptions. Ornamental descriptions are provided for constructing new descriptions from old ones such that ornaments can be automatically derived. Singleton ornaments are also defined, which create as many singleton types as there are elements of the base type.

Definition of (relational) algebraic ornaments and classifying algebras. The optimised predicate of an algebraic ornament can be swapped for a relational fold with the algebra of the ornament.

Let D : Desc I be a description. The category of relational D-algebras and the slice category of ornaments over D are equivalent.

The category of descriptions and ornaments. The functor Ind (for "induction") takes the least fixed points of descriptions and extends ornaments to forgetful maps on those least fixed points.

An extensional equivalence relation on ornaments, which extends to extensional equivalence on ornamental forgetful maps.

Horizontal transformations, i.e., shape-altering morphisms between horizontal data (cf. container morphisms). Ornaments can be derived from horizontal transformations.

The category of descriptions and families of horizontal transformations, and the equivalence between this category and the category Ōrn of descriptions and ornaments.

Ornamental equivalences about horizontal ornaments.

Shape : Functor ḞḢTrans Fam and Erase : Functor Ōrn ḞḢTrans reflect pullbacks. This file can take a long time to typecheck.

Parallel composition of ornaments.

Parallel composition of ornaments gives rise to a pullback square in Ōrn, which is also a pullback when mapped to Fam by the functor Ind. This file can take a long time to typecheck.

The optimised predicate for the parallel composition of two ornaments can be swapped for the pointwise conjunction of the optimised predicates for the two component ornaments. This file can take a long time to typecheck and may require a larger stack size.

Definition of an optimised predicate for an ornament as the parallel composition of the ornament and the singleton ornament. This construction gives a functor from Orn to FRef which produces more representation-efficient promotion predicates.

Sequential composition of ornaments.

Basic definitions of subsets and relations, combinators for specifying nondeterministic computation, relational inclusion wrapped up as preorder and setoid, combinators for reasoning with relations, componentwise relations between families of sets, and definition and properties of relators.

Let D : Desc I be a description. The category RAlg D is the wide subcategory of the category of relational D-algebras where the morphisms are restricted to be functions and are proof-relevant. This module also defines the banana-split algebras and proves that they are products in RAlg D.

Combinators that help avoiding explicit applications of monotonicity and associativity of relational composition and preservation of composition by relators and converse.

Definition of right-division of componentwise relations.

Definition and properties of relational fold.

A variant of the Greedy Theorem and its embedding into inductive families.

Definition of hylomorphisms and the Hylomorphism Theorem.

Definition and properties of binary join and its componentwise version, and definition of summing join (kept for future work).

Definition of meet and its componentwise version.

Definition of the relation that takes a minimum from a set generated by a relation, and its componentwise version.

Okasaki's idea of numerical representations are nicely captured by the coherence property of upgrades; insertion into binomial heaps is used as an example.

Finite numbers, i.e., natural numbers bounded above by a given natural number.

Fold fusion theorems for algebraic ornamentation.

The insert function used in insertion sort upgraded to work with vectors, ordered lists, and ordered vectors.

The ordering property and balancing properties of leftist heaps are treated separately when needed.

Cons-lists as an ornamentation of natural numbers.

Ordered lists indexed with a lower bound as an ornamentation of lists.

Vectors, i.e., length-indexed lists, defined as the optimised predicate for the ornament from natural numbers to lists.

Implementing the streaming theorem for list metamorphisms by algebraic ornamentation.

Solving the minimum coin change problem with the Greedy Theorem and algebraic ornamentation.

Peano-style natural numbers.

Decidable total ordering on natural numbers and minimum.