类型安全矩阵是一个长期存在的话题。他们争论着它们的相关性，并且编写了全部语言来实现长度在类型级别上的列表。令我惊讶的是，Haskell中仍然没有任何满足便利性和安全性理智标准的变体。是否有缺少现成库的原因，还是只是不必要？让我们弄清楚。

理解为什么某事（当然应该是！）不是的最可靠方法是尝试自己做。我们试试吧 ..

期望

首先想到的（至少对我来说）上的文章类型一级哈斯克尔的，在那里，用的帮助下DataKinds，GADTs，KindSignatures（在那里，为什么他们使用的简短描述-以下）引入的感应自然数，并把它们和载体背后参数长度：

data Nat = Zero | Succ Nat

data Vector (n :: Nat) a where
  (:|) :: a -> Vector n a -> Vector ('Succ n) a
  Nil :: Vector 'Zero a

infixr 3 :| 

KindSignatures用于表示它n可能不是具有类型的任何类型*（例如同一示例中的参数），而是Nat类型的值（提升到类型级别）。通过扩展可以做到这一点DataKinds。GADTs它们是必需的，以便构造函数可以影响值类型。在我们的例子中，构造函数将Nil精确地构造length的Vector Zero，并且构造函数将:|在第二个参数中的矢量上附加一个type元素，a并将大小增加一。有关更详细和正确的描述，您可以阅读我上面提到的文章或Haskell Wiki。

什么。这似乎是我们需要的。仅保留输入矩阵：

newtype Matrix (m :: Nat) (n :: Nat) a = Matrix (Vector m (Vector n a))

这甚至可以工作：

>>> :t Matrix $ (1 :| Nil) :| Nil
Matrix $ (1 :| Nil) :| Nil :: Num a => Matrix ('Succ 'Zero) ('Succ 'Zero) a

>>> :t Matrix $ (1 :| 2 :| Nil) :| (3 :| 4 :| Nil) :| Nil
Matrix $ (1 :| 2 :| Nil) :| (3 :| 4 :| Nil) :| Nil
  :: Num a => Matrix ('Succ ('Succ 'Zero)) ('Succ ('Succ 'Zero)) a

这种方法的问题已经从所有缝隙中浮现出来，但是您可以忍受它们，我们将继续。

, , , , , :

(*|) :: Num a => a -> Matrix m n a -> Matrix m n a
(*|) n = fmap (n *)

--        fmap
--       

instance Functor (Matrix m n) where
  fmap f (Matrix vs) = Matrix $ fmap f <$> vs

instance Functor (Vector n) where
  fmap f (v :| vs) = (f v) :| (fmap f vs)
  fmap _ Nil = Nil

, :

>>> :t fmap (+1) (1 :| 2 :| Nil)
fmap (+1) (1 :| 2 :| Nil)
  :: Num b => Vector ('Succ ('Succ 'Zero)) b

>>> fmap  (+1) (1 :| 2 :| Nil)
2 :| 3 :| Nil

λ > :t 5 *| Matrix ((1 :| 2 :| Nil) :| ( 3 :| 4 :| Nil) :| Nil)
5 *| Matrix ((1 :| 2 :| Nil) :| ( 3 :| 4 :| Nil) :| Nil)
  :: Num a => Matrix ('Succ ('Succ 'Zero)) ('Succ ('Succ 'Zero)) a

λ > 5 *| Matrix ((1 :| 2 :| Nil) :| ( 3 :| 4 :| Nil) :| Nil)
Matrix 5 :| 10 :| Nil :| 15 :| 20 :| Nil :| Nil

:

zipVectorWith :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
zipVectorWith f (l:|ls) (v:|vs) = f l v :| (zipVectorWith f ls vs)
zipVectorWith _ Nil Nil = Nil

(|+|) :: Num a => Matrix m n a -> Matrix m n a -> Matrix m n a
(|+|) (Matrix l) (Matrix r) = Matrix $ zipVectorWith (zipVectorWith (+)) l r

: , , . , :

-- transpose               :: [[a]] -> [[a]]
-- transpose []             = []
-- transpose ([]   : xss)   = transpose xss
-- transpose ((x:xs) : xss) = (x : [h | (h:_) <- xss]) : transpose (xs : [ t | (_:t) <- xss])

transposeMatrix :: Vector m (Vector n a) -> Vector n (Vector m a)
transposeMatrix Nil = Nil
transposeMatrix ((x:|xs):|xss) = (x :| (fmap headVec xss)) :| (transposeMatrix (xs :| fmap tailVec xss))

, GHC ( ).

    • Could not deduce: n ~ 'Zero
      from the context: m ~ 'Zero
        bound by a pattern with constructor:
                   Nil :: forall a. Vector 'Zero a,
                 in an equation for ‘transposeMatrix’
        at Text.hs:42:17-19
      ‘n’ is a rigid type variable bound by
        the type signature for:
          transposeMatrix :: forall (m :: Nat) (n :: Nat) a.
                             Vector m (Vector n a) -> Vector n (Vector m a)
        at Text.hs:41:1-79
      Expected type: Vector n (Vector m a)
        Actual type: Vector 'Zero (Vector m a)
    • In the expression: Nil
      In an equation for ‘transposeMatrix’: transposeMatrix Nil = Nil
    • Relevant bindings include
        transposeMatrix :: Vector m (Vector n a) -> Vector n (Vector m a)
          (bound at Text.hs:42:1)
   |
   | transposeMatrix Nil = Nil
   |

? , m Zero n Zero.

, , e Nil, Nil' n. n , , n .

, , - , . Haskell , .

- . . ?

Haskell : linear laop, :

• linear
• laop

linear laop. ? , , : , Succ Zero:

Matrix $ (1 :| 2 :| 3 :| 4 :| Nil) :| (5 :| 6 :| 7 :| 8 :| Nil) :| (9 :| 10 :| 11 :| Nil) :| Nil

    • Couldn't match type ‘'Zero’ with ‘'Succ 'Zero’
      Expected type: Vector
                       ('Succ 'Zero) (Vector ('Succ ('Succ ('Succ ('Succ 'Zero)))) a)
        Actual type: Vector
                       ('Succ 'Zero) (Vector ('Succ ('Succ ('Succ 'Zero))) a)
    • In the second argument of ‘(:|)’, namely
        ‘(9 :| 10 :| 11 :| Nil) :| Nil’
      In the second argument of ‘(:|)’, namely
        ‘(5 :| 6 :| 7 :| 8 :| Nil) :| (9 :| 10 :| 11 :| Nil) :| Nil’
      In the second argument of ‘($)’, namely
        ‘(1 :| 2 :| 3 :| 4 :| Nil)
           :| (5 :| 6 :| 7 :| 8 :| Nil) :| (9 :| 10 :| 11 :| Nil) :| Nil’

, GHC, - . ?

Template Haskell

TemplateHaskell (TH) — , -, , . .

matlab:

v = [1 2 3]
m = [1 2 3; 4 5 6; 7 8 10]

:

matrix := line; line | line
line := unit units
units := unit | ε
unit := var | num | inside_brackets

• var —
• num — ( )
• inside_brackets — Haskell ( ). Haskell haskell-src-exts haskell-src-meta

( , !). :

matrix :: Parser [[Exp]]
matrix = (line `sepBy` char ';') <* eof

line :: Parser [Exp]
line = spaces >> unit `endBy1` spaces

unit :: Parser Exp
unit = (var <|> num <|> inBrackets) >>= toExpr

Exp — AST Haskell, , ( AST ).

c , ,

data Matrix (m :: Nat) (n :: Nat) a where
  Matrix :: forall m n a. (Int, Int) -> ![[a]] -> Matrix m n a

, AST

expr :: Parser.Parser [[Exp]] -> String -> Q Exp
expr parser source = do -- parser    matrix   
  --      
  let (matrix, (m, n)) = unwrap $ parse source parser 
  --  AST
  let sizeType = LitT . NumTyLit
  --  TypeApplication  ,       ,        
  let constructor = foldl AppTypeE (ConE 'Matrix) [sizeType m, sizeType n, WildCardT]
  let size = TupE $ map (LitE . IntegerL) [m, n]
  let value = ListE $ map ListE $ matrix
  pure $ foldl AppE constructor [size, value]

parse :: String -> Parser.Parser [[a]] -> Either [String] ([[a]], (Integer, Integer))
parse source parser = do
  matrix <- Parser.parse parser "QLinear" source --   
  size <- checkSize matrix --  
  pure (matrix, size)

: QuasiQuoter

matrix :: QuasiQuoter
matrix =
  QuasiQuoter
    { quoteExp = expr Parser.matrix,
      quotePat = notDefined "Pattern",
      quoteType = notDefined "Type",
      quoteDec = notDefined "Declaration"
    }

! :

>>> :set -XTemplateHaskell -XDataKinds -XQuasiQuotes -XTypeApplications
>>> :t [matrix| 1 2; 3 4 |]
[matrix| 1 2; 3 4 |] :: Num _ => Matrix 2 2 _

>>> :t [matrix| 1 2; 3 4 5 |]
<interactive>:1:1: error:
    • Exception when trying to run compile-time code:
        All lines must be the same length
CallStack (from HasCallStack):
  error, called at src/Internal/Quasi/Quasi.hs:9:19 in qlnr-0.1.2.0-82f1f55c:Internal.Quasi.Quasi
      Code: template-haskell-2.15.0.0:Language.Haskell.TH.Quote.quoteExp
              matrix " 1 2; 3 4 5 "
    • In the quasi-quotation: [matrix| 1 2; 3 4 5 |]

>>> :t [matrix| (length . show); (+1) |]
[matrix| (length . show); (+1) |] :: Matrix 2 1 (Int -> Int)

TH , c . , hackage

>>> [operator| (x, y) => (y, x) |]
[0,1]
[1,0]
>>> [operator| (x, y) => (2 * x, y + x) |] ~*~ [vector| 3 4 |]
[6]
[7]

Haskell , . ? . , ( ), .

, . : .

复制到存储库和黑客的链接

欢迎提出意见，建议和请求。