The universal space

Take (or imagine) a blank sheet of paper. This is a plane. You can put points and vectors on it. A vector connects two points, but it is "movable": if you can translate one vector into another, they are deemed equal. A vector doesn't really have a beginning - you can position it wherever you want.

In this setting, some operations make sense, like

• vector + point = point:
  Position the vector at a point, and its end will be the result.


• point - point = vector:
  Join the points to get a vector from A to B. (It's inverse of vector + point = point.)


• vector + vector = vector:
  Put the beginning of one vector to the end of the second.

But some don't, like adding two points, or subtracting vector - point. With added origin, you can do anything using coordinates, as in (2,1) + (3,0) = (5,1). In fact, with given origin you can consider every point as a vector from the origin. But without it, it's like physical motion - you cannot tell if something is moving without a frame of reference.

Although addition point + point doesn't make sense, (point + point) / 2 should - it's middle between the points. 0.2 point + 0.8 point is somewhere in the 4/5 of the segment. This is known as "affine combination".

An expression like vector + point - point can be computed in two different ways: (vector + point) - point and vector + (point - point) and it turns out the result will be the same. There must be some structure here.

Define mass of a vector as 0, and mass of point as 1. Then,

• vector + point = point: 0 + 1 = 1


• point - point = vector: 1 - 1 = 0


• vector + vector = vector: 0 + 0 = 0


• (point + point) / 2 = point: (1+1) / 2 = 1

In fact you can enlarge the space. Define an object to be either a vector with mass 0, or a pair (p,m) which is a point p with a nonzero mass m. I'll write a point as m*p. Then multiplication streches a vector, or changes a point's mass: a*(m*p) = (a*m)*p. Addition is done with:

m p + v = m (p + \frac{v}{m})

- translation

m_{1}p_{1} + m_{2}p_{2} = (m_{1}+m_{2}) (\frac{m_{1}}{m_{1}+m_{2}} p_{1} + \frac{m_{2}}{m_{1}+m_{2}} p_{2})

- weighted mean of points

m_{1}p_{1} - m_{1} p_{2} = m_{1} (p_{1} - p_2})

- a vector joining two points

In this space, points and vectors are equal partners, and anything can be added and multiplied by a number. It's a vector space with dimension one more than the original.

In the original space, you assign a meaning to a sum like 0.2a + 0.8b, but not to the summands. In this space, summands make sense and 0.2a + 0.8b is really a sum of 0.2a and 0.8b.

In mathematical terms, this is an assignment of a vector space to every affine space. This construction is known as the universal space. Now, vector spaces and affine spaces have their own meaning of functions. A linear map respects linear combinations: f(cx+dy) = c f(x)+d f(y). An affine map is something that respects affine combinations: f(cx+dy) = cf(x)+ df(y), where c+d=1. It's easy to present a linear map using a matrix. How to present an affine map? The answer is, given affine map, you can extend it to a linear map between universal spaces by f(m*p)=m*f(p) for all m. And that gives a matrix.

For category theory lovers, this construction is the left adjoint of a functor that assigns an affine space to a vector space by forgetting the origin.

Kind polymorphism in action

Ultrecht Haskell Compiler is an experimental Haskell compiler that supports polymorphism on the kind level. This means that in

data Eq a b = Eq (forall f. f a -> f b)

Eq is given kind

Eq :: forall a . a -> a -> *

and both Eq Integer Char and Eq [] Maybe are valid types.

Using kind polymorphism, it is possible to write sigfpe's From monoids to monads using a single type class.

To talk about monoids, you need a category (mor), multiplication (mul) and a unit.

class Monoid mor mul unit m where
  one :: mor unit m
  mult :: mor (mul m m) m

With mor being (->), mul being (,), unit being () this is a normal monoid (one :: () -> m and mult :: (m,m) -> m.). For example:

instance Monoid (->) (,) () Integer where
  one () = 1
  mult = uncurry (*)

Now, instead of functions, there will be natural transformations; instead of (,) there will be functor composition; instead of unit there will be identity functor.

data Nat f g = Nat (forall x. f x -> g x)
data Comp f g x = Comp (f (g x))
data Id x = Id x
Nat :: (* -> *) -> (* -> *) -> *
Comp :: (* -> *) -> (* -> *) -> * -> *
Id :: * -> *

And here is the list monad. Notice kinds are different than in the previous case, but it is still an instance of the same type class.

instance Monoid Nat Comp Id [] where
  one = Nat $ \(Id x) -> [x]              -- one :: Nat Id []
  mult = Nat $ \(Comp x) -> concat x      -- mult :: Nat (Comp [] []) []

So, monads are really monoids in category of endofunctors.

If you invert the arrows, you get a comonad. Here's the product comonad.

data CoNat f g = CoNat (forall x. g x -> f x)
data CoComp f g x = CoComp (g (f x))
CoNat :: (* -> *) -> (* -> *) -> *
CoComp :: (* -> *) -> (* -> *) -> * -> *

data Product w a = Product w a

instance Monoid CoNat CoComp Id (Product w) where
  one = CoNat $ \(Product a b) -> Id b
  mult = CoNat $ \(Product a b) -> CoComp $ Product a (Product a b)

Question: what are kinds of mor, mul, unit and m in the Monoid type class definition?

There's a small lie here: monads require also a liftM/fmap function. Not all Haskell types of * -> * are functors, and I used that as a poor replacement.

I didn't write monoid laws, which if translated happen to be monad laws. You're welcome to read sigfpe's original post. It's hard to write them generically since there's no access to fmap.

The code is available on hpaste and can be run in UHC.