haskell - 如何在 Haskell 中实现与维度无关的矩阵向量乘法？

Question

我定义了一个存在隐藏维度的矩阵类型，所以我可以形成任意大小的矩阵列表：

import qualified Data.Vector.Sized as VS
import           Data.Vector.Sized (Vector)

-- | A matrix with existentially hidden dimensions.
data Mat :: * -> * where
  Mat :: (Vector m :.: Vector n) a -> Mat a

但是，现在，我不知道如何以类型检查的方式定义我的矩阵向量乘法函数。试试这个：

| Matrix-vector multiplication for existentially typed matrices.
(^*^)
  :: (KnownNat m, KnownNat n, Num a)
  => Mat a       -- ^ transform matrix
  -> Vector n a  -- ^ input vector
  -> Vector m a
Mat (Comp1 mat) ^*^ v = VS.map (dot v) mat

dot :: (KnownNat n, Num a) => Vector n a -> Vector n a -> a
u `dot` v = VS.sum $ VS.zipWith (*) u v

结果是：

• Couldn't match type ‘m1’ with ‘m’
  ‘m1’ is a rigid type variable bound by
    a pattern with constructor:
      Mat :: forall a (m :: Nat) (n :: Nat).
             (:.:) (Vector m) (Vector n) a -> Mat a,
    in an equation for ‘^*^’
    at src/RL/MulES.hs:89:1-15
  ‘m’ is a rigid type variable bound by
    the type signature for:
      (^*^) :: forall (m :: Nat) (n :: Nat) a.
               (KnownNat m, KnownNat n) =>
               Mat a -> Vector n a -> Vector m a
    at src/RL/MulES.hs:(84,1)-(88,15)
  Expected type: Vector m a
    Actual type: Vector m1 a
• In the expression: VS.map (dot v) mat
  In an equation for ‘^*^’:
      Mat (Comp1 mat) ^*^ v = VS.map (dot v) mat
• Relevant bindings include
    mat :: Vector m1 (Vector n8 a) (bound at src/RL/MulES.hs:89:12)
    (^*^) :: Mat a -> Vector n a -> Vector m a
      (bound at src/RL/MulES.hs:89:17)
   |
89 | Mat (Comp1 mat) ^*^ v = VS.map (dot v) mat
   |                         ^^^^^^^^^^^^^^^^^^

标签： haskellmatrix-multiplicationtypecheckingexistential-type

Answer 1

First let me remark that I find this whole idea quite dubious: why do you bother fixing dimensions through the type system if you then throw it away again with the existential wrapper?

Since you don't know the domain dimension of that linear mapping, the only vector you can apply it to is one that can have any dimension on demand. That's pretty crazy, but it can be expressed in Haskell using -XRank2Types. Also you don't know the codomain dimension, so the result must again be existentially wrapped. The existential wrappers must contain a KnownNat constraint, else you won't be able to do anything with the vectors at all. Like

{-# LANGUAGE GADTs, Rank2Types, UnicodeSyntax #-}

-- | This is really just a pretentious replacement for Data.Vector.Vector
data Array :: * -> * where
  Array :: KnownNat n => Vector n a -> Mat a

data Mat :: * -> * where
  Mat :: (KnownNat n, KnownNat m) => (Vector m :.: Vector n) a -> Mat a

lapply :: Num a => Mat a -> (∀ n . KnownNat n => Vector n a) -> Array a
lapply (Mat m) v = Array $ VS.map (dot v) mat

Will this be useful for anything? Not sure. You could actually create such a length-agnostic vector if what you really want to express is a continuous function that's PCM-sampled on a uniform grid (what the Matlab folks use all day, instead of having proper function types...). The sampling would automatically be adjusted to whatever resolution the matrix demands.

But, at runtime this just means your input “vector” is actually a function that takes a resolution-argument. There's not much the whole type-level-number foo buys you here.

IMO, when you find yourself dealing with such “variable length vectors” it's usually a sign that you're really working in an infinite-dimensional vector space, like usually such a function space. (The most widely-used such space is the L² Hilbert space.) This can't really be expressed with any array-based approach, but it can be expressed if you ditch the dimension/element decomposition and instead use vector spaces as a typeclass. Conal Elliott's package for this has been around for a long time now; it may seem a bit dated but is actually quite practically useful still. I spend some effort building upon it a proper category of linear maps, haven't really gotten to the point of making it fully usable for infinite-dimensional spaces though.