Programming with Quotients

# Rationals

We can represent fractions by a pair of an integer numerator and positive denominator. Then rationals can be the quotient of fractions equating all representations of the same rational:

1
2
3
4

data Rat : Type where
  _/_ : Int -> Pos -> Rat
  Eq : (n/m : Rat) -> (n'/m' : Rat) -> (n * m' = n' * m) 
        -> (n/m = n'/m')

Then to define a function (f) on this type we define it at the points as usual and the paths (equalities): (ap_f\ (p : a = b) : f(p) = f(q)). I have made up a notation where you pattern match each path constructor and overload function name f:

1
2
3

f : (p : x = y) -> f x = f y
f (PathConstr1(?fields) : x = y) = ?prove : f x = f y
f (PathConstr2(?fields) : x = y) = ?prove : f x = f y

For example, negation:⁵

1
2
3
4
5
6
7

-_ : Rat -> Rat
-(n/m) = (-n)/m
{- We must also provide a case for the path constructor -}
{- Remember (Eq q q' p) : q = q', so -(Eq q q' p) : -q = -q' -}
{- Remember that p : n * m' = n' * m -}
{- Assume a lemma that L {n,m} = (-n) * m = -(n * m) -}
-(Eq q q' p) = Eq (-q -q' (L >> -p >> flip L))

Here >> represents path composition and flip path inversion. I.e. for $p : a = b$ and $q : b = c$ then $p \texttt{>>} q : a = c$ and $flip\ p : b = a$ . Applying a function $f : A \to B$ to a path $p : a =_A a'$ gives $f(p) : f(a) =_B f(a')$ ; in the above case $-p : -(n*m') = -(n'*m)$ .

The ideas extend to multiple-argument functions:

1
2
3
4
5
6
7
8
9

_*_ : Rat -> Rat -> Rat
(n/m) * (n'/m') = (n * n')/(m * m')
{- Assume associativity lemma A {a,b,c} : (a*b)*c = a*(b*c) and commutativity lemma C {a,b} : a * b = b * c -}
{- This proof could be simplified via stronger lemmas -}
(Eq q r p) * (Eq q' r' p') =
  let rearrange = A >> (refl * flip A) >> (refl * (C * refl)) 
                  >> (refl * A) >> flip A in
  let e =  rearrange >> (p * p') >> rearrange in
  Eq ((q * q') (r * r') e)

# Unordered Pairs

Similarly, we can represent unordered pairs:

1
2
3

data UPair : Type -> Type -> Type where
  (,) : UPair a b
  Swap : ((x, y) : UPair a b) -> (x, y) = (y, x)

Whose functions f : UPair a b -> T must have a case for Swap, which amounts to proving commutativity!

1

f (Swap (x,y)) = ?commutativity : f (x, y) = f (y, x)

# Multisets

Now we get onto examples from some papers. In the motivation for Epigram (McKinna 2006) a merge sort is formalised. Their final sorting function has the following type:⁶

1
2
3
4
5
6
7

data OList Nat where
  [] : OList 0
  (::) : (x : Nat) -> {y : Nat} -> {auto lt : x <= y} 
         -> OList y -> OList x
‎
‎
<p>sort : List Nat -> OList 0</p>

Where OList is a locally sorted list with an (open) lower bound on all its elements. The locally-sorted property is ensured by the requirement that to cons a list we must provide a proof lt : x <= y. However, this of course does not require the resulting list to have the same elements as before, just that it is sorted.⁷ We could just always return the empty list!

But how could this invariant be enforced? Well, there are many ways: you could explicitly include a permutation proof Permutation : List Nat -> List Nat -> Type on lists and a toList function from OList 0 to List Nat, require that sort also returns a proof:

1

sort : (xs : List Nat) -> (ys : OList 0 ** Permutation(xs, toList ys))

We then have to pass and manipulate the proof explicitly through each recursive call of the sort function.

But, I found an interesting way to do this differently with quotients. We simply say that sort takes multisets (whose underlying inductive type is List Nat) to sort. Then any lists that differ only by ordering are identified by the same multiset and must return equivalent OLists. However, there is still no link between the input and output, and it seems a dependent pair is unavoidable: here we require that the input multiset is equal to the output. That is, that sort is an identity function on multisets. What makes this method easier is that the quotients have already enforced that all permutations map to the same output; we should only need to prove the equality for the case when the input is already sorted!

The easiest way to define multisets is by asserting that if you union (append) two multisets in any order, then they are still equal. It is easy to see that this creates an equivalence relation relating all permutations together.

1
2
3
4
5
6
7

data Multiset : Type -> Type where
  List a {- extending lists with a quotient 
            (like in polymorphic variants) -}
  Commute : (xs : Multiset a) -> (ys : Multiset a) 
            -> xs ++ ys = ys ++ xs
 ‎ ‎ 
sort : (xs : Multiset Nat) -> (ys : OList 0 ** xs = ys)

By the subtyping ideas mentioned earlier, a list is automatically a multiset. Interestingly, we can use sorted lists as a canonical form for multisets, meaning any function f : OList 0 -> T precomposes with sort to give rise to a function out of the quotient f ∘ sort : Multiset \mathbb{N} -> T with no proof obligations. Equally, multisets could have been defined by quotienting with sort (i.e. identifying lists whose sorted representations are equal).

# Equational Algebras

Every inductive type generates a free algebra (Burris and Sankappanavar 1981), while quotients allow further non-trivial identifications between terms to be made. This allows us to impose an equational theory upon the inductive type.

For example, we can consider a Packet DSL implemented in agda by Brady (2011). They start with a basic type to describe primitive data chunks of length-indexed bits, null-terminated strings, length-indexed strings, and propositions about the chunks:⁸

1
2
3
4
5

data Chunk : Set where
  bit : (width: Int) -> so (width>0) -> Chunk
  Cstring : Chunk
  Lstring : Int -> Chunk
  prop : (P:Prop) -> Chunk

Since these are purely markers, we cannot do any meaningful quotients here. However, the propositions with and and or constructors could be equated via de Morgan's laws.

More importantly, they define a PacketLang DSL, where we can add some useful equational laws:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21

data PacketLang : Set where
  CHUNK : (c:Chunk) -> PacketLang
  IF : Bool -> PacketLang -> PacketLang -> PacketLang
  (//) : PacketLang -> PacketLang -> PacketLang
  LIST : PacketLang -> PacketLang
  LISTN : (n:Nat) -> PacketLang -> PacketLang
  BIND : (p:PacketLang) ->
           (mkTy p -> PacketLang) -> PacketLang
  {- Path Constructors -}
  IFTrue : If true p q = p
  IfFalse : If false p q = q
  IfSame : {p = q} -> If b p q = p
  OrAssoc : (p // q) // r = p // (q // r)
  OrComm : p // q = q // r
  OrSame : {p = q} -> p // q = p
  BindRet : {p : PacketLang} -> {f : mkTy p -> PacketLang} 
              -> BIND (CHUNK x) f = f (mkTy x)
  BindAssoc  : {p : PacketLang} {f : mkTy p -> PacketLang} 
               -> {g : mkTy (BIND p f) -> PacketLang} 
               -> BIND (BIND p f) g = BIND p (\x => BIND (f x) g)
  ... {- etc. (note, not all the obvious laws work due to weirdness of mkTy) -}

However, since everything decodes via mkTy and chunkTy to (different, built-in) idris types, we can only get isomorphisms, not equalities between these results, which is incompatible with our quotients that require equivalence. Although this would be fine in a homotopy setting by the Univalence axiom (Univalent Foundations Program 2013). Similarly, it would be nice to have laws saying that the equational theory is algebraic w.r.t. BIND (that IF and // distribute through BIND) but these do not type check. Creating a unified inductive data type instead of decoding various different generic agda types, then mkTy would effectively be a normalisation (eval) function on the DSL, performed before marshalling in order to extract the data consistently without violating the quotients. In this situation, the type system would need to normalise the PacketLang terms before being passed into C code as the laws cannot be verified within C code.

Quotients can represent much more complex equational theories, as can be seen in Altenkirch and Kaposi (2016).