Right now I'm going through Type-Driven Development, and I'm on the exercises for part 3.3, question 2.

I'm trying to implement:

total addMatrix : Num a => Vect n (Vect m a) -> Vect n (Vect m a) -> Vect n (Vect m a)

to add two two-dimensional matrices.

I had as my implementation:

addMatrix : Num a => Vect n (Vect m a) -> Vect n (Vect m a) -> Vect n (Vect m a)

addMatrix [] [] = []

addMatrix ((w :: x) :: xs) ((z :: y) :: ys) = ((w + z) :: (zipWith (+) x y)) :: addMatrix xs ys

this ran, and produced the correct output from the example input, but it was not total.

Using the keyboard shortcuts I ended up producing automatically two more matches:

addMatrix : Num a => Vect n (Vect m a) -> Vect n (Vect m a) -> Vect n (Vect m a)

addMatrix [] [] = []

addMatrix ([] :: xs) y = [] :: xs

addMatrix x ([] :: ys) = [] :: ys

addMatrix ((w :: x) :: xs) ((z :: y) :: ys) = ((w + z) :: (zipWith (+) x y)) :: addMatrix xs ys

This is total, this produces the right output, but I can't help but think those two cases aren't right.

I'm still very new to functional programming, so I'm a bit confused sometimes on the match syntax, but I do think that's not what I want to do, but I'm not actually sure what say addMatrix ([] :: xs) y means exactly.

Could someone help me sort this out?

Post has attachment
Post has attachment
Dependent types will take over the word! To help with it, my book "Beginning Haskell" [http://www.apress.com/9781430262503] shows the beginning steps of using Idris :)
Post has attachment
In dependently typed languages, it is possible to write generic versions of n-adic functions. For example, here's zipWith/zipWith3/... in Idris:

http://gist.github.com/timjb/6259455

Now, this isn't quite generic. I would like to be able to write 'zipWithN 3 f as bs cs' or 'zipWithN 4 g as bs cs ds'. Unfortunately, Idris apparently can't figure out the contents of the vector of types given as an implicit argument in these cases, which is the reason of existence for the functions zipWith3 and so on. Now, is there a better way to write generalized zips that doesn't need these specialized functions?
Wait while more posts are being loaded