fix +> Category instance

[crclark]

@mikeizbicki,

While working through the linear algebra example, I found and fixed a bug in the (+>) Category instance that caused (a.b) $ x to not equal a $ b $ x. The problem is that the instance of Concrete assumes that the type SVector 3 Double +> SVector 2 Double describes a matrix with 3 columns and 2 rows, while the instance for Category assumes that it means 3 rows and 2 columns (the other way around!). The linear algebra example file was using the latter convention exclusively, but it wasn't causing problems because ($) was only used with square matrices, which masked the problem.

Here's a minimal example of the problem for GHCI (adapted from the linear algebra example code):

let x = unsafeToModule [2,1,0] :: SVector 3 Double
let a = unsafeMkSMatrix 2 3 [1..6] :: SVector 2 Double +> SVector 3 Double
let b = unsafeMkSMatrix 3 2 [1..6] :: SVector 3 Double +> SVector 2 Double

Then this will give the correct answer of [30,64,98](I verified with Numpy as a sanity check):

(a.b) $ x 

While this will result in an exception:

a $ b $ x

This problem can also lead to type errors if we follow the row,column convention in the examples. a is actually the right shape to right-multiply by x, but a $ x is a type error.

After this fix, we will need to type our matrices the other way around:

let a' = unsafeMkSMatrix 2 3 [1..6] :: SVector 3 Double +> SVector 2 Double

let b' = unsafeMkSMatrix 3 2 [1..6] :: SVector 2 Double +> SVector 3 Double

And then (a'.b') $ x and a' $ b' $ x will both give correct results.

The underlying problem is that the implementation of (.) for matrices was flipped matrix multiplication, but it should be unflipped. That is, (a . b) should denote AB, not BA. This is the only way to get consistent behavior for (.) and ($). It also makes matrix multiplication in SubHask a lot less confusing :)

This PR also fixes the example and adds a note about how to read matrix type signatures w.r.t. numbers of rows and columns.

Unfortunately I wasn't able to figure out how to write a test for this. It looks like the Template Haskell test system only works for unary type classes. If you have any pointers, I can try to add a test to the PR. I wanted to write a test like this:

law_Concrete_application_composition ::
    (subcat <: (->)
     , Category subcat
     , Eq_ c) => subcat b c -> subcat a b -> a -> Logic c
law_Concrete_application_composition f g x
    = ((f.g) $ x) == (f $ g $ x)

[mikeizbicki]

Thanks for catching this very important bug! All your changes look great.

I like the additional law you propose as well. Currently, there's no way to check these higher order laws, and this is mostly due to engineering related limitations in template haskell. GHC 8.0 is fixing a bunch of type system issues that will make subhask nicer, but I haven't been following the template haskell improvements closely enough to know if it'll allow for these higher order laws. Maybe.

[mikeizbicki]

The failed build was due to a travis misconfiguration. I've reconfigured and it passes.