Matriks tipe-aman adalah topik abadi. Mereka berdebat tentang relevansinya, dan seluruh bahasa ditulis untuk mengimplementasikan daftar dengan panjang di tingkat jenis . Saya merasa aneh bahwa masih belum ada varian di Haskell yang memenuhi kriteria kenyamanan dan keamanan yang wajar. Apakah ada alasan untuk kurangnya perpustakaan yang sudah jadi, atau apakah itu tidak diperlukan? Mari kita cari tahu.

Cara paling pasti untuk memahami mengapa sesuatu (yang memang seharusnya begitu!) Tidak - adalah mencoba melakukannya sendiri. Mari mencoba ..

Harapan

Hal pertama yang datang ke pikiran (setidaknya untuk saya) artikel tentang dari Haskell tingkat jenis , di mana, dengan bantuan DataKinds, GADTs, KindSignatures(deskripsi singkat dari mana dan mengapa mereka digunakan - di bawah ini) diperkenalkan bilangan induktif, dan di belakang mereka dan vektor parameterized panjang:

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 :|

KindSignaturesdigunakan untuk menunjukkan bahwa itu nmungkin bukan tipe apapun dengan jenis *(seperti parameter dalam contoh yang sama), tetapi nilai tipe Nat, dinaikkan ke tingkat tipe. Ini dimungkinkan dengan ekstensi DataKinds. GADTsmereka diperlukan agar pembangun dapat mempengaruhi jenis nilai. Dalam kasus kami, konstruktor akan Nilmembuat Vektor dengan panjang Zero, dan konstruktor akan :|melampirkan elemen tipe ke vektor dalam argumen kedua adan meningkatkan ukurannya satu per satu. Untuk penjelasan yang lebih detail dan benar, Anda bisa membaca artikel yang saya rujuk di atas atau di Haskell Wiki.

Apa. Ini sepertinya yang kita butuhkan. Tetap hanya untuk memasukkan matriks:

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

Dan ini bahkan akan berhasil:

>>> :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

Masalah dari pendekatan ini sudah muncul dari semua celah, tetapi Anda dapat menerimanya, kami akan melanjutkan.

, , , , , :

(*|) :: 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 , . ? . , ( ), .

, . : .

Tautan duplikat ke repositori dan peretasan

Komentar, saran dan permintaan tarik dipersilakan.

Matriks jenis-aman di Haskell

Harapan

Template Haskell

More articles: