haskell - 如何在 Edward Kmett 的 "Linear"库中使用可变大小向量？

Question

我正在尝试使用 ekmett 的线性库，但在 Linear.V 中的可变长度向量方面遇到了一些问题。如何使用 dim 函数获取向量的大小？如何在由嵌套 V 组成的大方阵上使用 trace ？在这两种情况下我都会遇到错误。

最少代码:

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

它给出了这些我不明白的错误:

• 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

因为 Haskell 不是依赖类型的，所以它无法将仅在运行时获取的列表的长度提升到类型级别。话虽如此，n 的目的是您可以编写在向量大小上具有多态性的代码(例如，您可以确保您没有采用具有以下特征的向量的点积):不同的长度)。 但是如果您想使用该信息，您仍然需要在编译时显式指定实际向量的长度。

线性为您提供的是fromVector它在运行时执行检查您提供的向量是否与您指定的类型匹配。例如，

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)

因此，就您而言，您可能应该执行以下操作:

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 是的 - 我认为最后的交互是一个错误(除非有人能看到我丢失的东西)。虽然 Dim n => Trace (V n) 实例应该可以满足 Trace (V 5) 变体，但由于某种原因却不能。

编辑

正如 @user2407038 所指出的，问题是我上面提到的 Dim n => Trace (V n) 不是多类的 - 它只适用于 n::* 而我们希望它适用于任何类型(特别是本例中的 n::Nat)。实际上没有任何理由进行此限制，因此我们可以继续定义我们自己的实例版本

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

我打开了一个 issue .

编辑2

该问题现已修复。我认为它可能会进入 线性 的下一个版本。

<小时/>

作为旁注，我使用 -XDataKinds 以便我可以编写类型级文字(具有类型 GHC.TypeLits.Nat - 它们很特殊并硬连线到 GHC)和 -XOverloadedLists，这样我就可以编写 [1..5]::Vector Int。