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?
Vect n a
can't be a monoid, sincen
needs to be doubled in the result. You need a customconcat : Vect n (Vect m a) -> Vect (n*m) a
, which probably needs a_++_ : Vect n a -> Vect m a -> Vect (n+m) a
and some arithmetic lemmas such asn*m + m = (succ n)*m
. – chiconcat
function in the stdlib of idris. – Bakuriu