类型安全矩阵乘法

Question

在Haskell中写这个Scala矩阵乘法的冗长讨论后,我想知道......类型安全矩阵乘法会是什么样的？所以这是你的挑战:要么链接到Haskell实现,要么自己实现,如下:

data Matrix ... = ...

matrixMult :: Matrix ... -> Matrix ... -> Matrix ...
matrixMult ... = ...

当matrixMult产生一个错误类型在编译的时候,如果你试图乘两个matricies不兼容的尺寸.布朗尼指出,如果你链接到讨论这个精确主题的论文或书籍,和/或讨论自己这个功能是多么有用/无用.

Answer 1

有许多包实现了这个:

• http://hackage.haskell.org/package/hmatrix-static
• http://hackage.haskell.org/packages/archive/repa-algorithms/2.2.0.1/doc/html/Data-Array-Repa-Algorithms-Matrix.html
• http://hackage.haskell.org/packages/archive/blas/0.7.6/doc/html/Data-Matrix-Dense.html#t:Matrix
• http://hackage.haskell.org/package/Vec

特别是维修论文对设计空间和选择进行了非常好的讨论:http://repa.ouroborus.net/

历史最感兴趣的是McBride的2001年的"Faking It",它描述了强类型向量.他采用的技术与上述包装中使用的技术非常相似.他们显然是在做出依赖类型编程的圈子里知道的,但我的印象是"Faking It"论文是在Haskell中使用它们的早期实例之一.Oleg的2005 Monad Reader关于数字参数化类型的文章也对这些技术的历史进行了一些很好的讨论.

Answer 2

您可以使用类型级自然数来对维度进行编码.您的矩阵类型变为

-- x, y: Dimensions
data Matrix x y n = ...

你必须定义两个附加ADTs和一个类TLN(Type Level Naturals):

data Zero
data Succ a
class    TLN a                 where fromTLN :: a -> Int
instance TLN Zero              where fromTLN = const Zero
instance TLN a => TLN (Succ a) where fromTLN = 1 + fromTLN (undefined :: a)

你的函数类型很简单:

matrixMult :: (TLN x, TLN y, TLN t, Num a) =>
  Matrix x t a -> Matrix t y a -> Matrix x y a

您可以通过生成undefined适当的类型和ScopedTypeVariables扩展名来提取数组维度.

此代码完全未经测试,GHC可能会在编译时停止.这只是一个关于如何做到的草图.

链接

• http://www.haskell.org/haskellwiki/Type_arithmetic

Answer 3

对不起,无法抗拒粘贴我很久以前掀起的东西.这是在类型族之前,所以我使用fundeps进行算术运算.我证实这仍然适用于GHC 7.

{-# LANGUAGE EmptyDataDecls,
  ScopedTypeVariables,
  MultiParamTypeClasses,
  FunctionalDependencies,
  FlexibleContexts,
  FlexibleInstances,
  UndecidableInstances #-}

import System.IO


-- Peano type numerals

data Z
data S a

type One = S Z
type Two = S One
type Three = S Two

class Nat a
instance Nat Z
instance Nat a => Nat (S a)

class Positive a
instance Nat a => Positive (S a)

class Pred a b | a -> b
instance Pred (S a) a


-- Vector type

newtype Vector n k = Vector {unVector :: [k]}
    deriving (Read, Show, Eq)

empty :: Vector Z k
empty = Vector []

vtail :: Pred s' s => Vector s' k -> Vector s k
vtail (Vector (a:as)) = Vector as
vhead :: Positive s => Vector s k -> k
vhead (Vector (a:as)) = a

liftV :: (a->b) -> Vector s a -> Vector s b
liftV f = Vector . map f . unVector

type Matrix m n k = Vector m (Vector n k)

infixr 6 |>
(|>) :: k -> Vector s k -> Vector (S s) k
k |> v = Vector . (k:) . unVector $ v


-- Arithmetic

instance (Num k) => Num (Vector n k) where
    (+) (Vector v) (Vector u) = Vector $ zipWith (+) v u
    (*) (Vector v) (Vector u) = Vector $ zipWith (*) v u
    abs = liftV abs
    signum = liftV signum

dot :: Num k => Vector n k -> Vector n k -> k
dot u v = sum . unVector $ v*u

class Transpose n m where
    transpose :: Matrix n m k -> Matrix m n k

instance (Transpose m a, Nat a, Nat m) => Transpose m (S a) where
    transpose v = liftV vhead v |>
                  transpose (liftV vtail v)

instance Transpose m Z where
    transpose v = empty

multiply :: (Nat n, Nat m, Nat n', Num k, Transpose m n) =>
            Matrix m n k -> Matrix n' m k -> Matrix n n' k
multiply a (Vector bs) = Vector [Vector [a `dot` b | a <- as] | b <- bs]
    where (Vector as) = transpose a

printMatrix :: Show k => Matrix m n k -> IO ()
printMatrix = mapM_ (putStrLn) . map (show.unVector) . unVector


-- Examples

m :: Matrix Three Three Integer
m =    (1 |> 2 |> 3 |> empty)
    |> (2 |> 3 |> 4 |> empty) 
    |> (3 |> 4 |> 5 |> empty) |> empty
n :: Matrix Three Two Integer
n =    (1 |> 0 |> empty)
    |> (0 |> 1 |> empty) 
    |> (1 |> 1 |> empty) |> empty
o = multiply n m
p = multiply n (transpose n)