Grothendieck Completion

> {-# OPTIONS -XNoMonomorphismRestriction -XExistentialQuantification #-}
> import Data.Monoid
> import Data.Set

One of the experiences of learning mathematics is climbing the ladder
of numbers from natural numbers to complex numbers:

    N < Z < Q < R < C

Here I'll review how Z may be constructed from N by a general algebraic
method and then see what that same method yields when applied to more
arbitrary data types.

We define natural numbers as Peano numerals.

> data N = Zero | Succ N deriving (Eq, Show)

A mathematician would say that we have made a free monoid on one
generator (the Succ constructor).

Addition is a simple matter of combining all the generators.

> addN Zero     n = n
> addN (Succ m) n = Succ (addN m n)

This makes N into a monoid.

> instance Monoid N where
>     mempty = Zero
>     mappend = addN

As a matter of syntactic convenience, we'll use an infix operator for
the monoid operation and use a shorthand for the unit.

> e = mempty
> (>>>) = mappend

The left-to-right bias of >>> is intended. Later we will be working with
non-commutative monoids.

The e is shorthand for Einheit, meaning unit, and is a common abbreviation
in the literature. If you don't like it, tough! Blame Germany for producing
so many influential algebraists and settling countless conventional one-letter
abbreviations like K for fields (K for K�rper).

We'd like for N to be an instance of Num so we can use fromInteger. We don't
care about the rest, so we leave them undefined.

> instance Num N where
>     fromInteger n = iterate Succ Zero !! fromInteger n
>
>     (+) = undefined
>     (*) = undefined
>     abs = undefined
>     signum = undefined

Most of us are used to thinking of the integers Z as natural numbers with a
sign prefixed. To construct Z from N, your first instinct is probably to define

  data Sign = Minus | Plus
  data Z = Z Sign N

Indeed, that is one possible way to go. The only hitch is that you have to
ensure that Z Plus Zero and Z Minus Zero are considered equal. The easiest
way to achieve that is to use some consistent normalization:

  normalizeZ (Z Minus Zero) = Z Plus Zero
  normalizeZ n              = n

All functions that construct new integers must then call normalizeZ.

However, there is also an alternative construction of Z from N. The idea is
this: Rather than view the sign (plus or minus) as a prefix, we can view it
as an infix between two numbers. That is, we know that every integer can be
expressed as the difference of two naturals, so we should be able to represent
integers as pairs of naturals (m, n), corresponding to the integer m - n.

The mathematician Grothendieck invented a more general version of this
construction to define the K_0 groups of K theory, and therefore it generally
bears his name. You see variations on "Grothendieck construction", "Grothendieck
completion" and "K-completion" thrown around. Here I'll refer to it as the
Grothendieck completion as best describes its purpose of completing (in the
sense of filling or perfecting) a monoid by adjoining formal inverses.

> data Z = Z N N deriving Show

With the sign-based representation, the only redundantly represented number
was zero, expressible as either plus or minus zero. With this pair-based
representation, there are far more redundancies. For example, 2 - 3 and
1 - 2 both represent the same number. More generally,

    m - n = m' - n'

if and only if

    m + n' = m' + n

As an aside, note how this looks like the rule for comparing fractions
if you replace + and - by * and /. The only difference is that we allow
our "denominators" to be zero.

> instance Eq Z where
>     (Z m n) == (Z m' n') = (m >>> n') == (m' >>> n)

Addition is now defined by simply adding entrywise, much like how fractions
are multiplied by multiplying numerators and denominators separately.

> addZ (Z m n) (Z m' n') = Z (m >>> m') (n >>> n')

If no for other reason, this simple implementation of integer addition should
make us appreciate this pair-based construction.

Addition for sign-based integers is less symmetric and messier. It corresponds
to addition in the pair-based representation, where Plus n and Minus n are
interpreted as (n, Zero) and (Zero, n), followed by a normalization step that
shifts all the Succ occurrences to one side or the other, depending on which is
larger.

> instance Monoid Z where
>     mempty = Z Zero Zero
>     mappend = addZ

Everything should far should have been pretty simple. I hope you're convinced
that this pair-based representation indeed produces a structure isomorphic to
integers. However, let's review what we did in more general terms in an attempt
to identify the assumptions that made it work out so well.

We started with N, a free monoid on one generator. Because it only has a single
generator, N is automatically commutative. While the monoidal operation (addition)
is not generally invertible, N's freeness as a monoid does have a related
property: If a >> b = a >> c then a = b. This makes N a cancelative monoid.

Let's say we want to extend or complete N to make its operation invertible.
That is, we want to make N a group. A group is just a monoid with a way of
computing inverses for every element.

> class Monoid g => Group g where
>     inverse :: g -> g

For a Group instance to represent an actual group, the defining property
of inverses must hold:

  x >>> inverse x = e
  inverse x >>> x = e

This is easily implemented for our integer type Z. It's just a matter of
swapping the entries in a pair.

> instance Group Z where
>     inverse (Z m n) = (Z n m)

As an aside, it's curious to see that the involution property of inverses
follows from the fact that swapping pair entries twice does nothing!

The group completion of N is a new algebraic object K N with a map

  inject :: N -> K N

It is injective and therefore paired with a projection:

  project :: K N -> Maybe K

Projection is the left inverse of injection:

  project . inject = Just

Whatever else its properties, a basic requirement is that the injective image
of N inside of K N should behave identically to N on its own. That is, if
we zoom in on the part of K N that is the injective image of N then the
dynamics should be indistinguishable from N's own dynamics. This is another
way of saying that the injection is a monoid homomorphism:

  inject (x >>> y) = inject x >>> inject y

The >>> on the left side is in N and the one on the right side is in K N.

Let's return to the cancelation property and consider a general monoid M.
We saw earlier that in the case of N, a cancelative monoid, we successfully
got Z, a group, as the completion. What would happen if M were not cancelative?

One case would be the natural numbers, this time with multiplication instead of
addition. We can cancel most of the time but not when the multiplier is zero.
Certainly 0 * 1 = 0 * 3 does not imply 1 = 3. In attempting to complete this M to
K M the requirement that 'inject' is a homomorphism means that n * 0 = 0 for all n
must also hold true in K M as well. But since every element, including 0, must have
an inverse, we can take the equality like 0 * n = 0 and multiply both sides by the
inverse of 0 to get n = 0. That is, the image of M inside K M is 0, so 'inject'
certainly cannot be injective!

Thus we see that a monoid must be cancelative to have a group completion.

The other special fact about N is that it is a free monoid, and in particular it
is a free monoid on one generator ("one-dimensional") and therefore commutative.
What about free monoids on more generators, which would be non-commutative?

For any type X we can consider the free monoid F X with a generator for every element
in X. An element of F X is a word (possibly empty) drawn from the alphabet X and
the monoid operation is concatenation. The free monoid construction is a functor,
meaning every map X -> Y can be lifted to a map F X -> F Y on the free monoids.

This F is of course none other than the type constructor for lists! The monoid operation
is list concatenation and the identity element is the empty list. The lifting is our
familiar friend map :: (a -> b) -> ([a] -> [b]).

We have said multiple times that N is a free monoid on one generator. With this
identification of the free monoid construction F with the type constructor for lists,
this is simply a way of saying that N is isomorphic to [()] since () is the canonical
type inhabited by a single value, also denoted ().

What happens when we transfer our pairing construction to arbitrary free monoids?
It's a straightforward matter of taking our code from Z and replacing every occurrence
of N with an abstract type parameter:

> data K m = K m m deriving Show
>
> instance Monoid m => Monoid (K m) where
>     mempty = K e e
>     mappend (K x y) (K x' y') = K (x >>> x') (y >>> y')
>
> instance Monoid m => Group (K m) where
>     inverse (K x y) = (K y x)
>
> instance (Monoid m, Eq m) => Eq (K m) where
>     (K x y) == (K x' y') = (x >>> y') == (x' >>> y)

Injection and projection is now a simple matter:

> inject x = (K x e)
>
> project (K x e) = Just x
> project _       = Nothing

It's easy to see that project . inject = Just. What about the homomorphism property?
Can you prove that?

We defined an instance of Group for K m but is it actually a group? So far we've only
verified that directly for the type N, or equivalently [()]. Let's tackle the next
simplest case, where the value type has two elements. We might as well pick the standard
type Bool.

*Main> let x = inject [True]
*Main> x
K [True] []
*Main> inverse x
K [] True
*Main> x >>> inverse x
K [True] [True]
*Main> x >>> inverse x == e
True

Cool! But so far we have only used lists of one kind of value. Let's try more.

*Main> let x = inject [True, False]
*Main> x
K [True,False] []
*Main> inverse x
K [] [True,False]
*Main> x >>> inverse x == e
True

It seems to work alright. Let's try some experiments with an infinite value type. We'll
use the integers.

*Main> let a = inject [1]
*Main> let b = inject [2]
*Main> let c = inject [3]
*Main> a >>> (b >>> inverse b)
K [1,2] [2]
*Main> a >>> (b >>> inverse b) >>> c
K [1,2,3] [2]

We would expect (b >>> inverse b) to be not only equal to e in the sense of the (==)
equality function we defined but to be interchangeable with all e in all contexts,

*Main> a >>> e >>> c
K [1,3] []
*Main> a >>> (b >>> inverse b) >>> c == a >>> e >>> c
False

Damn! That's definitely not right!

The problem stems from the lack of commutativity, so it seem that the commutativity of N
that may have seemed incidental to our success in constructing Z is not so incidental
after all.

To verify that the construction indeed works for commutative monoids other than N, let's
explore some related examples. It turned out that lists (free mononoids) did not work due
to the non-commutativity of list concatenation. What are the closest thing to lists
while having a commutative kind of concatenation? Sets of course! The Set type constructor
in fact corresponds to the free commutative monoid construction. Given a type X that acts
as a generating set, Set X is the freest possible commutative monoid with X as generators.

Let's replay the failing example with sets instead of lists.

*Main> let a = inject (singleton 1)
*Main> let b = inject (singleton 2)
*Main> let c = inject (singleton 3)
*Main> a >>> (b >>> inverse b) >>> c == a >>> e >>> c
True

Yay! It worked!

If K N were the integers then what is K (Set X)? Because of the commutativity, the different
generators don't really interact, so you'd expect it to be a product of integers, one copy
for each value in X. That is, K (Set X) is isomorphic to the function type X -> Z.