Clever Geek Handbook

Matrices de type sécurisé dans Haskell

Les matrices de type sécurisé sont un sujet éternel. Ils discutent de leur pertinence et des langages entiers sont écrits pour implémenter des listes avec une longueur au niveau du type . Il m'a semblé étrange qu'il n'y ait toujours aucune variante dans Haskell qui réponde aux critères sains de commodité et de sécurité. Y a-t-il des raisons au manque de bibliothèques prêtes à l'emploi, ou ne sont-elles tout simplement pas nécessaires? Découvrons-le.



Le moyen le plus sûr de comprendre pourquoi quelque chose (qui devrait certainement l'être!) N'est pas - est d'essayer de le faire vous-même. Essayons ..



Attente



La première chose vient à l' esprit (au moins pour moi) article sur le niveau de type haskell , où, à l'aide de DataKinds, GADTs, KindSignatures(une brève description de l' endroit où et pourquoi ils sont utilisés - ci - dessous) sont introduits nombres naturels inductives, et derrière eux et des vecteurs longueur paramétrées:



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


KindSignaturesest utilisé pour indiquer qu'il ne npeut s'agir d'aucun type avec un genre *(comme un paramètre dans le même exemple), mais d'une valeur du type Nat, élevée au niveau des types. Ceci est possible par extension DataKinds. GADTsils sont nécessaires pour que le constructeur puisse influencer le type de valeur. Dans notre cas, le constructeur Nilconstruira exactement le vecteur de longueur Zero, et le constructeur :|attachera un élément de type au vecteur dans le deuxième argument aet augmentera la taille de un. Pour une description plus détaillée et correcte, vous pouvez lire l'article auquel j'ai fait référence ci-dessus ou le Wiki Haskell.



Quoi. Cela semble être ce dont nous avons besoin. Il ne reste plus qu'à entrer dans la matrice:



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


Et cela fonctionnera même:



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


Les problèmes de cette approche émergent déjà de toutes les fissures, mais vous pouvez vivre avec eux, nous continuerons.



, , , , , :



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



, . : .



Dupliquer les liens vers le référentiel et le piratage



Les commentaires, suggestions et pull requests sont les bienvenus.



More articles:


All Articles