Since Haskell is independent of the type of input, it cannot raise the length of the list at the type level, which it can only receive at run time. With that said, the goal of n
is that you can make code that is polymorphic in the size of the vectors (for example, you can make sure that you do not accept the point product of a vector that has a different length). But you still need to explicitly specify the length of your actual vectors at compile time if you want to use this information.
Which linear
gives you fromVector
, which at runtime checks that the vector you specify matches the type you specify, 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 do 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 vw 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 mistake (if someone does not see something that I am missing). The Trace (V 5)
variant must be executed, although the Dim n => Trace (V n)
instance, but for some reason this is not so.
EDIT
As @ user2407038 pointed out, the problem is that the Dim n => Trace (V n)
mentioned above is not multilined - it only works for n :: *
, although we would like it to work for any type (in particular n :: Nat
in this case). There is really no reason for this limitation, so we can continue and define our own version of the instance
ghci> :set -XPolyKinds ghci> instance Dim n => Trace (V n) ghci> trace m 106.0
I opened the issue .
EDIT 2
Now the problem is fixed. I believe this is likely to happen in the next linear
release.
As a side note, I use -XDataKinds
, so I'm allowed to write type level literals (which have the kind GHC.TypeLits.Nat
- they are special and tightly bound to GHC) and -XOverloadedLists
, so I can write [1..5] :: Vector Int
>.