How do I use variable size vectors in Edward Kmett's "Linear" library?

Question

I'm trying to use ekmett's linear library, and I'm having some trouble with variable length vectors, in Linear.V. How do I use the dim function to get the size of a vector? How do I use trace on a large square matrix made of nested Vs ? I get errors in both of these cases.

Minimal code:

import qualified Data.Vector as Vector
import Linear.V (V(V), dim)
import Linear.Vector (outer)
import Linear.Matrix (trace)

v, w :: V n Double -- What do I do here?
v = V $ Vector.fromList [1..5]
w = V $ Vector.fromList [2, 3, 5, 7, 11]

d = dim v
m = outer v w
t = trace m

It gives these errors which I don't understand:

• Ambiguous type variable ‘n0’ arising from a use of ‘dim’
  prevents the constraint ‘(Linear.V.Dim n0)’ from being solved.
  Probable fix: use a type annotation to specify what ‘n0’ should be.
  These potential instances exist:
    two instances involving out-of-scope types
    (use -fprint-potential-instances to see them all)
• In the expression: dim v
  In an equation for ‘d’: d = dim v

• Ambiguous type variable ‘n1’ arising from a use of ‘trace’
  prevents the constraint ‘(Linear.V.Dim n1)’ from being solved.
  Probable fix: use a type annotation to specify what ‘n1’ should be.
  These potential instances exist:
    two instances involving out-of-scope types
    (use -fprint-potential-instances to see them all)
• In the expression: trace m
  In an equation for ‘t’: t = trace m

Answer 1

Because Haskell is not dependently typed, it can't lift to the type level the length of a list it might be getting only at runtime. With that said, the purpose of the n is that you can make code that is polymorphic over the size of the vectors (for example you can make sure your aren't taking the dot product of vector that have different lengths). But you still need to explicitly specify the length of your actual vectors at compile time, if you want to use that information.

What linear does give you is fromVector which performs at runtime a check that the vector you gave matches the type you specified. For example,

ghci> :set +t -XDataKinds -XOverloadedLists
ghci> import Linear
ghci> import Linear.V
ghci> fromVector [1,2,3] :: Maybe (V 3 Int)
Just (V {toVector = [1,2,3]})
it :: Maybe (V 3 Int)
ghci> fromVector [1,2,3] :: Maybe (V 2 Int)
Nothing
it :: Maybe (V 3 Int)

So, in your case, you should probably be doing something like the following:

ghci> Just v = fromVector [1..5]           :: Maybe (V 5 Double)
v :: V 5 Double
ghci> Just w = fromVector [2, 3, 5, 7, 11] :: Maybe (V 5 Double)
w :: V 5 Double
ghci> dim v
5
it :: Int
ghci> m = outer v w
m :: V 5 (V 5 Double)
ghci> trace m
<interactive>:44:1: error:
   • No instance for (Trace (V 5)) arising from a use of ‘trace’
   • In the expression: trace m
     In an equation for ‘it’: it = trace m

...annnnd yeah - I think the last interaction is a bug (unless someone can see something I'm missing). The Trace (V 5) variant should be satisfiable though the Dim n => Trace (V n) instance but for some reason it isn't.

EDIT

As @user2407038 has pointed out, the problem is that the Dim n => Trace (V n) I mentioned above is not polykinded - it only works for n :: * while we would like it to work for any kind (specifically n :: Nat in this case). There isn't really any reason for this restriction, so we can go ahead and define our own version of the instance

ghci> :set -XPolyKinds
ghci> instance Dim n => Trace (V n)
ghci> trace m
106.0

I've opened an issue.

EDIT 2

The issue is now fixed. I reckon it should probably make it into the next release of linear.

---

As a side note, I use -XDataKinds so that I am allowed to write type-level literals (which have kind GHC.TypeLits.Nat - they are special and hardwired into GHC) and -XOverloadedLists so I can write [1..5] :: Vector Int.