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.