Comment utiliser des vecteurs de taille variable dans la bibliothèque "Linear" d'Edward Kmett?

Question

J'essaie d'utiliser la bibliothèque linéaire d'ekmett, et j'ai quelques problèmes avec les vecteurs de longueur variable, dans Linear.V. Comment puis-je utiliser la fonction dim pour obtenir la taille d'un vecteur? Comment puis-je utiliser trace sur une grande matrice carrée faite de V s imbriqués? J'ai des erreurs dans ces deux cas.

Code minimal:

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 

Il donne à ces erreurs que je ne comprends pas:

• 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

Parce que Haskell n'est pas dépendamment typé, il ne peut pas soulever au niveau de la longueur de type d'une liste, il pourrait être obtenu seulement à l'exécution. Cela dit, le but du n est que vous pouvez faire du code polymorphe sur la taille des vecteurs (par exemple vous pouvez vous assurer que vous ne prenez pas le produit scalaire de vecteur qui a des longueurs différentes). Mais vous devez toujours spécifier explicitement la longueur de vos vecteurs réels au moment de la compilation, si vous souhaitez utiliser cette information.

Qu'est-ce linearfait vous donner est fromVector qui effectue lors de l'exécution d'un contrôle que le vecteur que vous avez donné correspond au type spécifié. Par exemple,

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) 

Ainsi, dans votre cas, vous devriez probablement faire quelque chose comme ce qui suit:

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 ouais - Je pense que la dernière interaction est un bug (à moins que quelqu'un peut voir quelque chose que je manque). La variante Trace (V 5) doit être satisfiable par l'instance Dim n => Trace (V n) mais, pour une raison quelconque, elle ne l'est pas.

EDIT

Comme @ user2407038 l'a souligné, le problème est que le Dim n => Trace (V n) je l'ai mentionné ci-dessus ne polykinded - il ne fonctionne que pour n :: * pendant que nous voudrions que cela fonctionne pour tout type (en particulier n :: Nat dans ce cas). Il n'y a pas vraiment de raison de cette restriction, afin que nous puissions aller de l'avant et de définir notre propre version de l'instance

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

J'ai ouvert un issue.

EDIT 2

Le problème est maintenant résolu. Je pense qu'il devrait probablement le faire dans la prochaine version de linear.

---

Comme une note de côté, j'utilise -XDataKinds pour que je suis autorisé à écrire de type niveau littéraux (qui ont GHC.TypeLits.Nat genre - ils sont en GHC spéciales et avec fil) et -XOverloadedLists je peux écrire [1..5] :: Vector Int.