Типобезопасные матрицы — извечная тема. О нужности их спорят, а для реализации списков с длинной на уровне типов пишут целые языки. Мне показалось странным, что на Haskell до сих пор нет ни одного варианта, который удовлетворял бы вменяемым критериям удобства и безопасности. Есть какие-то причины отсутствия готовых библиотек или они просто не_нужны? Давайте разбираться.

Верный способ понять, почему чего-то (что непременно должно быть!) нет — это попробовать сделать это самому. Попробуем..

Ожидание

Первым же делом вспоминается (по крайней мере мне) статья о type level 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 может быть не любым типом с kind’ом * (как например параметр а в этом же примере), а значением типа Nat, поднятым на уровень типов. Возможность этого обеспечивается расширением DataKinds. GADTs же нужны для того, чтобы конструктор мог влиять на тип значения. В нашем случае конструктор Nil построит именно Vector длины Zero, а конструктор :| присоединит к вектору во втором аргументе элемент типа 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 не то, что бы тривиальная задача. Получились ли мои матрицы типобезопасными? Скорее нет. Они имеют типобезопасный и гибкий интерфейс, но реализация функционала отдана на откуп разработчику (то есть мне), корректность которого компилятор гарантировать не может.

Хорошо это или плохо, но в зоопарке матриц на хаскеле прибавление. А вы решайте: нужны или нинужны.

Дублирую ссылки на репозиторий и hackage

Замечания, предложения, а также пуллреквесты, приветствуются.