Типобезопасные матрицы на Haskell

?v=1

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

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

© Habrahabr.ru