[Agda] Agda2 beginner's question

[Nicolas Pouillard]

Excerpts from Andreas Abel's message of Thu Nov 26 01:00:58 +0100 2009:
> 
> Dear Wolfram,
> 
> welcome to Agda!  We help you suffer through the first steps... ;-)
> 
> kahl at cas.mcmaster.ca wrote:
> > Dear Agda list,
> > 
> >   I know Haskell, including GADTs, and have used Isabelle before;
> > now I am just starting to try to get going with Agda2
> > and hit a serious roadblock in trying to unwrap a Data.Vec.Group
> > from the standard library (lib-0.2) to get at the enclosed Vec (Vec ...).
> > 
> > Since my ``group'' application appears to type check,
> > I would not have expected to be asked to prove
> > 
> >   concat xss = allFin (n * m)
> > 
> > before I can bind ``xss'' in the concat' pattern.
> > And even if I really have to do it, I have no idea how to start...
> 
> Yeah, I think that is an over-eagerly typing of "group" in the standard 
> library.  To use it, you have to first prove that your vector is 
> splittable into a vector of vectors who concat together to your original 
> vector.  But group is supposed to do the splitting for you...  Da beisst 
> sich die Katze in den Schwanz!
> 
> I can implement your example with the following, not so ambitiously 
> typed version of group.
> 
> group : ∀ {a} n k (xs : Vec a (n * k)) → Vec (Vec a k) n
> group zero    k []                  = []
> group (suc n) k xs                  with splitAt k xs
> group (suc n) k .(ys ++ zs)         | ys ++' zs with group n k zs
> group (suc n) k .(ys ++ concat zss) | ys ++' zs | zss = ys ∷ zss
> 
> Btw. your mat1 contained some bug as well (m and n switched).
> 
> mat1 : (m : ℕ) → (n : ℕ) → Matrix ℕ m n
> mat1 m n with group m n (allFin (m * n))
> mat1 m n | xss  = map (map toℕ) xss
> 
> Maybe I am missing something at 1 a.m. in the night, but the parts of my 
> brain that are still working tell me that the group function of the 
> stdlib needs to be rewritten, or at least there needs to be a comment 
> how on earth you are supposed to use it!

The original group function *is* usable, however having a convenient function
to remove the concat' constructor would help:

unconcat' : ∀ {a n k} {xs : Vec  a (n * k)} → Group n k xs → Vec (Vec a k) n
unconcat' (concat' xss) = xss

group' : ∀ {a} n k (xs : Vec a (n * k)) → Vec (Vec a k) n
group' n k xs = unconcat' (group n k xs)

Of course the function names could be improved.

-- 
Nicolas Pouillard
http://nicolaspouillard.fr