TRANSPOSITION FOR FIXED-SIZED MATRICES, TAKE TWO

Bruno Oliveira and Jeremy Gibbons
5th December 2005


Bruno was rightly dissatisfied with my approach, as outlined in
"Transposition for Fixed-Sized Matrices". He showed me a better way,
which I write up here. The programs are his (though I understand that
they owe something to Conor's lecture notes on Epigram from AFP2005);
the explanation is mine.


Again, we use GADTs from GHC 6.4+

> {-# OPTIONS -fglasgow-exts #-}

and again, we make use of type-level naturals as length indexes for
vectors:

> data Z
> data S n

> data Vector n a where
>   VNil  :: Vector Z a
>   VCons :: a -> Vector n a -> Vector (S n) a

> toList :: Vector n a -> [a]
> toList VNil = []
> toList (VCons a x) = a : toList x

> instance Show a => Show (Vector n a) where
>   show = show . toList


Type-level naturals have value-level representatives:

> data Nat n where
>   Z :: Nat Z
>   S :: Nat n -> Nat (S n)

> len :: Vector n a -> Nat n
> len VNil = Z
> len (VCons a x) = S (len x)


Here are two simple combinators on vectors: "rep" makes a constant
vector of a given length, and "zap" is "zip with apply". Note that the
two arguments of zap are forced at the type level to be of the same
length.

> vrep :: Nat n -> a -> Vector n a
> vrep Z      x = VNil
> vrep (S n)  x = VCons x (vrep n x)

> zap :: Vector n (a -> b) -> Vector n a -> Vector n b
> zap VNil          VNil          = VNil
> zap (VCons f fs)  (VCons x xs)  = VCons (f x) (zap fs xs)

With vrep and zap, we can build vmap and vfork as before (although they
aren't used in this script):

> vmap :: (a->b) -> Vector n a -> Vector n b
> vmap f x = zap (vrep (len x) f) x

> vfork :: Vector n (a->b) -> a -> Vector n b
> vfork fs a = zap fs (vrep (len fs) a)

Transposition is much easier to write if we explicitly pass the sizes
as parameters, rather than deducing them from the given matrix. In
particular, there is no longer a problem in computing the width of an
empty matrix.

> tr :: Nat n -> Nat m -> Vector n (Vector m a) -> Vector m (Vector n a)
> tr Z      m  VNil          = vrep m VNil
> tr (S n)  m  (VCons x xs)  = zap (zap (vrep m VCons) x) (tr n m xs)

Now we expect that 

  tr n m . tr m n = id

> v1 = VCons 1 (VCons 2 (VCons 3 VNil))
> v2 = VCons 4 (VCons 5 (VCons 6 VNil))
> v3 = VCons 7 (VCons 8 (VCons 9 VNil))
> three = S (S (S Z))

> m1 = VCons v1 (VCons v2 (VCons v3 VNil))

> proofTest n m = tr n m . tr m n
> proofTest' = proofTest three three m1


More interesting, perhaps, is the observation that fixed-length
vectors form what Conor McBride calls an "idiom" (or, to use the
revised name, an "applicative functor").

> class Functor f => Applicative f where
>   pure   :: a -> f a
>   (<*>)  :: f (a -> b) -> f a -> f b

Applicative functors are partway between functors and monads; every
monad is an applicative functor (with return for pure, and ap for
<*>), and every applicative functor is a functor. McBride and Paterson
motivate an applicative functor f as a type constructor that embeds
the usual notion of value, but has "its own peculiar way of giving
meaning to the usual applicative language - its idiom".

As well those of functors, applicative functors must satisfy the
following laws:

  pure id <*> u = u
  pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
  pure f <*> pure x = pure (f x)
  u <*> pure x = pure ($ x) <*> u

Conor and Ross's paper shows that the ordinary list functor is an
applicative functor:

> instance Applicative [] where
>   pure = repeat
>   (<*>) = zipWith ($)

It turns out that so is the functor Vector n, for arbitrary size
n. (In fact, Vector n is a monad, too, as are infinite lists; whereas
lists with repeat and zipWith ($) are not a monad - ragged lists
break the law.) 

To install Vector n as an instance of Applicative, however, we cannot
just use the operations vrep and zap defined above, because vrep has the
wrong type: the length is passed explicitly. Instead, we need to infer
that length by type, for which we need type classes.

> class Size n where
>   rep :: a -> Vector n a

> instance Size Z where
>   rep x = VNil

> instance Size n => Size (S n) where
>   rep x = VCons x (rep x)

> instance Functor (Vector n) where 
>   fmap = vmap

> instance Size n => Applicative (Vector n) where
>   pure   = rep
>   (<*>)  = zap

This doesn't help us much with our transposition. However, note that
the definition given above is constructed entirely out of applicative
functor widgets, so we can now write instead:

> tr2 :: Size m => Vector n (Vector m a) -> Vector m (Vector n a)
> tr2 VNil          = pure VNil
> tr2 (VCons x xs)  = pure VCons <*> x <*> tr2 xs

This suggests that there is more to transposition than what we've seen
about vectors: the same definition works for any applicative
functor. So here is a more generic version of tr:

> gtr :: Applicative f => Vector n (f a) -> f (Vector n a)
> gtr VNil          = pure VNil
> gtr (VCons x xs)  = pure VCons <*> x <*> gtr xs

Conor and Ross take this further. You might see that both equations
for gtr simply replicate the vector structure, reinterpreting
constructor applications in the idiom. This same idea works for any
datatype functor (certainly, regular functors; probably, anything that
corresponds to a relator). Moreover, it fuses with map; so the
construction can be generalized a little further, by applying some
function idiomatically to the elements of the data structure.

> class Traversable t where
>   traverse :: Applicative f => (a -> f b) -> t a -> f (t b)

> instance Traversable (Vector n) where
>   traverse f VNil          = pure VNil
>   traverse f (VCons x xs)  = pure VCons <*> f x <*> traverse f xs

If we specialize so that the function applied everywhere is just the
identity function, we get what Conor and Ross call an "applicative
distributor" (I believe this is what Lambert Meertens called "functor
pulling"):

> dist :: (Applicative f, Traversable t) => t (f b) -> f (t b)
> dist = traverse id

Applicative distribution is a generic zip or commuter for datatypes;
specialized to vectors, it is of course our transposition.

> tr3 :: Size m => Vector n (Vector m a) -> Vector m (Vector n a)
> tr3 = dist

I still haven't tried out the proof that tr is its own inverse,
though.