How to make Vect n Int an instance of Monoid

Question

In Idris, Vect n a is a datatype representing a vector of n length containing items of type a. Imagine I have a function:

foo : Int -> Vect 4 Int
foo n = [n-1, n, n+1, n*4]

The body of the function is not important, it could be anything that returns a vector of 4 Ints. Now, I want to use this function with concatMap as follows:

bar : Vect n Int -> Vect (4*n) Int
bar vals = concatMap foo vals

Bar is a function that takes an Int vector of length n and returns ones of length 4*n.

The type signature of concatMap is:

Prelude.Foldable.concatMap : Foldable t => Monoid m => (a -> m) -> t a -> m

And hence if I try to compile bar, I get the error:

 When elaborating right hand side of bar:
     Can't resolve type class Monoid (Vect (plus n (plus n (plus n (plus n 0)))) Int)

This means Vect n Int isn't an instance of monoid. To make it an instance of monoid, I need to implement:

Prelude.Algebra.neutral : Monoid a => a

Unfortunately however I'm not sure how to do this. List implements monoid, as follows:

instance Monoid (List a) where
    neutral = []

But if I try to implement monoid with neutral = [] for Vect n Int, I receive the error:

 When elaborating right hand side of Prelude.Algebra.Vect n Int instance of Prelude.Algebra.Monoid, method neutral:
 |   Can't unify
 |           Vect 0 Int
 |   with
 |           Vect n Int
 |   
 |   Specifically:
 |           Can't unify
 |                   0
 |           with
 |                   n

So I was wondering, how would I go about implementing monoid for Vect?

Answer 1

You can't implement a monoid such that you are able to write down that expression using concatMap. Think about the signature of concatMap:

(Foldable t, Monoid m) => (a -> m) -> t a -> m

Note that the m must be the same Monoid in the both the return type of the functional argument (a -> m) and the return type of the whole function. However this is not the case for Vect n a. Consider the expression:

concatMap foo vals

Here foo will have a type of a -> Vect 4 a, and the result of concatMap that you want is of type Vect (4*n) a where n is the length of the original vector. But this cannot fit the concatMap type because you have an application of concatMap that requires a type like:

(Foldable t, Monoid m, Monoid m1) => (a -> m) -> t a -> m1

where the result monoid and the value returned by the function can be different types, while concatMap imposes you to use the same type.

[a] and Vect n a are completely different because [] does not include the length in the type, and this allows you to write a concatMap function. In fact this allows you to make a Monoid instance for [] and concatenation as binary operator.

When you start attaching the length to a type this possibility vanishes because you cannot mix different lengths anymore and thus Vect n a do not form a monoid for concatenation. The concatenation operator becomes of type a -> b -> c in the general case, and in particular it's type for Vects is Vect n a -> Vect m a -> Vect (n+m) a, which is clearly different from its type for lists: [a] -> [a] ->[a].

---

This said, the error you reported is due to the fact that when writing an instance for the Monoid class of Vect n a the value of neutral must be of type Vect n a but [] is of type Vect 0 a.

However you can create a different instance for the Monoid type class over Vect n a. If the elements of such a vector are monoids then you can create the monoid of such vectors.

In this case he neutral vector must be of length n, and the only sensible value that you can give to its elements is the neutral of the elements Monoid. Basically you want the neutral of Vect n a to be replicate n neutral.

The binary operation for the Monoid would then be the element-wise application of the operation between the elements.

So the instance would look something like:

instance Monoid a => Monoid (Vect n a) where
    neutral = replicate n neutral

instance Semigroup a => Semigroup (Vect n a) where
    Nil <+> Nil = Nil
    (x :: xs) <+> (y :: ys) = (x <+> y) :: (xs <+> ys)

Unfortunately I'm not an Idris user/programmer so I can't tell you exactly how to correctly write such code. The above is just an Haskell-like pseudocode to give an idea of the concepts.