Типобезопасные матрицы на Haskell
Типобезопасные матрицы — извечная тема. О нужности их спорят, а для реализации списков с длинной на уровне типов пишут целые языки. Мне показалось странным, что на 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 |]
: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
Замечания, предложения, а также пуллреквесты, приветствуются.
