Массивы и подъем класса типов (и зависимые типы?)

Обычный способ — обернуть не очень типизированное представление в более типизированное, например:

data Nat = Z | S Nat
newtype Vec (n :: Nat) a = Vec [a]
newtype Sized m (ns :: [Nat]) a = Sized { getArray :: Array (Vec m Int) a }

Здесь ns — это продвигаемый (см. Продвижение Haskell) фантом (см. Мотивация фантомных типов?) значение — список размеров измерений, а m — это длина этого списка (расширенного и фантомного). Таким образом, любой массив под оболочкой Sized считается многомерной матрицей, размеры которой представляют ns. Экземпляр Monoid выглядит следующим образом:

instance (SingI m, SingI ns, Monoid a) => Monoid (Sized m ns a) where
  mempty                      = listSized $ repeat mempty
  Sized as `mappend` Sized bs = listSized $ zipWith mappend (elems as) (elems bs)

Этот SingI материал взят из библиотеки singletons. Синглтоны позволяют поднимать значения на уровень типов, поэтому мы можем как бы эмулировать зависимые типы, а SingI позволяет возвращать поднятые значения обратно на уровень значений с помощью функции fromSing. listSized по сути является listArray, но для массивов со статически известными размерами и, следовательно, требует, чтобы все эти SingI находились в области видимости. Вот его определение:

toInt :: Nat -> Int
toInt = go 0 where
  go !a  Z    = a
  go  a (S n) = go (1 + a) n

vecBounds :: forall m (ns :: [Nat]). (SingI m) => Sing ns -> (Vec m Int, Vec m Int)
vecBounds singNs = (Vec $ replicate m 0, Vec ns') where
    m   = toInt $ fromSing (sing :: Sing m)
    ns' = map (pred . toInt) $ fromSing singNs

listSized :: forall m (ns :: [Nat]) a. (SingI m, SingI ns) => [a] -> Sized m ns a
listSized = Sized . listArray (vecBounds (sing :: Sing ns))

vecBounds вычисляет границы для заданного расширенного списка размеров измерений. Он возвращает кортеж, первый компонент которого является самым нижним индексом, который всегда имеет форму [0,0..0] (нулей столько, сколько размеров, т.е. m). Второй компонент является наибольшим индексом, поэтому, если вы, например. есть список размеров таких измерений, как [2, 1, 3] (представленный как [S (S Z), S Z, S (S (S Z))]), тогда максимальный индекс равен [1, 0, 2].

Остается только предоставить экземпляр Ix для Vec n a, который является прямым обобщением экземпляры продукта:

instance Ix a => Ix (Vec n a) where
  range   (Vec ns, Vec ms)          = map Vec . sequence $ zipWith (curry range) ns ms
  index   (Vec ns, Vec ms) (Vec ps) = foldr (\(i, r) a -> i + r * a) 0 $
    zipWith3 (\n m p -> (index (n, m) p, rangeSize (n, m))) ns ms ps
  inRange (Vec ns, Vec ms) (Vec ps) = and $ zipWith3 (curry inRange) ns ms ps

И мы можем написать несколько тестов:

type M  = S (S (S Z))
type Ns = [S (S Z), S Z, S (S (S Z))]

arr1 :: Sized M Ns (Sum Int)
arr1 = listSized $ map Sum [5,3,6,7,1,4]

arr2 :: Sized M Ns (Sum Int)
arr2 = listSized $ map Sum [8,2,9,7,3,6]

main = mapM_ (print . getArray) $ [arr1, arr2, arr1 `mappend` arr2 `mappend` mempty]

Это печатает

array (Vec [0,0,0],Vec [1,0,2]) [(Vec [0,0,0],Sum {getSum = 5}),(Vec [0,0,1],Sum {getSum = 6}),(Vec [0,0,2],Sum {getSum = 1}),(Vec [1,0,0],Sum {getSum = 3}),(Vec [1,0,1],Sum {getSum = 7}),(Vec [1,0,2],Sum {getSum = 4})]
array (Vec [0,0,0],Vec [1,0,2]) [(Vec [0,0,0],Sum {getSum = 8}),(Vec [0,0,1],Sum {getSum = 9}),(Vec [0,0,2],Sum {getSum = 3}),(Vec [1,0,0],Sum {getSum = 2}),(Vec [1,0,1],Sum {getSum = 7}),(Vec [1,0,2],Sum {getSum = 6})]
array (Vec [0,0,0],Vec [1,0,2]) [(Vec [0,0,0],Sum {getSum = 13}),(Vec [0,0,1],Sum {getSum = 15}),(Vec [0,0,2],Sum {getSum = 4}),(Vec [1,0,0],Sum {getSum = 5}),(Vec [1,0,1],Sum {getSum = 14}),(Vec [1,0,2],Sum {getSum = 10})]

т.е. элементы суммировались поточечно по мере необходимости. И если вы случайно попытаетесь суммировать массивы с разными размерностями, вы получите ошибку типа:

type Ns  = [S (S Z), S Z, S (S (S Z))]
type Ns' = [S (S (S Z)), S Z, S (S Z)]

arr1 :: Sized M Ns (Sum Int)
arr1 = listSized $ map Sum [5,3,6,7,1,4]

arr2 :: Sized M Ns' (Sum Int)
arr2 = listSized $ map Sum [8,2,9,7,3,6]

main = print . getArray $ arr1 `mappend` arr2

-- Couldn't match type 'S 'Z with 'Z …
-- Expected type: Sized M Ns (Sum Int)
--   Actual type: Sized M Ns' (Sum Int)
-- In the second argument of `mappend', namely `arr2'
-- In the first argument of `mappend', namely `arr1 `mappend` arr2'

Полный код.

@ user3237465 — это полный и прямой ответ на ваш вопрос о присоединении информации о статическом размере к Arrays. Но поскольку вы упомянули, что вы новичок в зависимых типах, я хотел привести более простой пример сложения матриц, который, как мне кажется, может послужить лучшим введением в тему. Многое из нижеприведенного можно найти (лучше объяснить!) в Хазохизм бумага.

Как обычно, у нас есть натуральные числа, которые GHC автоматически поднимет до уровня типа. Следующее объявление data не только определяет тип Nat и два конструктора значений Z и S, мы также получаем вид Nat и два конструктора типа Z и S.

data Nat = Z | S Nat

type One = S Z
type Two = S (S Z)
type Three = S (S (S Z))

Я собираюсь определить обычный вектор GADT, который функционально представляет собой связанный список со статическим знанием его длины.

infixr 5 :>
data Vec n a where
    VNil :: Vec Z a
    (:>) :: a -> Vec n a -> Vec (S n) a
deriving instance Show a => Show (Vec n a)

instance Functor (Vec n) where
    fmap f VNil = VNil
    fmap f (x :> xs) = f x :> fmap f xs

Вот несколько примеров векторов.

v1 :: Vec Two String
v1 = "foo" :> "bar" :> VNil
v2 :: Vec Two String
v2 = "baz" :> "quux" :> VNil
v3 :: Vec One String
v3 = "nabble" :> VNil

Нам потребуется выполнить анализ чисел на уровне типов во время выполнения. Например, мы хотим написать функцию vreplicate :: n -> a -> Vec n a, которая повторяет заданный элемент n раз. vreplicate должен знать во время выполнения, сколько копий значения необходимо сделать! Однако приведенная выше сигнатура типа недействительна, поскольку Haskell поддерживает разделение между значениями времени выполнения и типами времени компиляции. Типы, принадлежащие виду Nat, не могут передаваться во время выполнения. Введите одиночные значения.

data Natty n where
    Zy :: Natty Z
    Sy :: Natty n -> Natty (S n)

(Это более или менее код, который генерирует для вас библиотека singletons.) Для заданного (четко определенного) n вида Nat существует ровно одно (точно определенное) значение типа Natty n. Сопоставление с образцом на Natty говорит вам о его n. Квантификатор forall n. Natty n -> говорит вам, что n используется во время выполнения. Таким образом, наша функция vreplicate будет иметь тип Natty n -> a -> Vec n a с Natty n в качестве замены n во время выполнения. (Настоящий зависимо типизированный язык не заставит вас прыгать через такой обруч!)

Как я уже говорил, если вы знаете значение Natty, вы знаете его n. Мы можем дополнительно заставить информацию течь в другом направлении, от типов к значениям, используя следующий хакерский класс типов:

class NATTY n where
    natty :: Natty n
instance NATTY Z where
    natty = Zy
instance NATTY n => NATTY (S n) where
    natty = Sy natty

Словарь NATTY n является неявной копией одноэлементного словаря n Natty.

OK. Экземпляр Applicative для Vec объединяет два вектора вместе, точечно объединяя их содержимое.

vzip :: Vec n a -> Vec n b -> Vec n (a, b)
vzip VNil VNil = VNil
vzip (x :> xs) (y :> ys) = (x, y) :> vzip xs ys

vreplicate :: Natty n -> a -> Vec n a
vreplicate Zy _ = VNil
vreplicate (Sy n) x = x :> vreplicate n x

instance NATTY n => Applicative (Vec n) where
    pure = vreplicate natty
    fs <*> xs = fmap (uncurry ($)) (vzip fs xs)

Итак, мы можем преобразовать Monoid для as в Monoid для векторов a. Это стандартный трюк, чтобы превратить Applicative в Monoid.

instance Monoid a => Monoid (Vec n a) where
    mempty = pure mempty
    mappend = liftA2 mappend

Выигрыш: вы можете использовать только mappend векторов, длины которых совпадают. Сравните это со списком zip, который усекает более длинный из двух сжатых списков.

ghci> v1 `mappend` v2
"foobaz" :> ("barquux" :> VNil)

-- ┌       ┐     ┌        ┐     ┌           ┐
-- | "foo" |  +  | "baz"  |  =  | "foobar"  |
-- | "bar" |     | "quux" |     | "bazquux" |
-- └       ┘     └        ┘     └           ┘

ghci> v1 `mappend` v3
<interactive>:35:14: error:
    • Couldn't match type ‘'Z’ with ‘'S 'Z’
      Expected type: Vec Two String
        Actual type: Vec One String
    • In the second argument of ‘mappend’, namely ‘v3’
      In the expression: v1 `mappend` v3
      In an equation for ‘it’: it = v1 `mappend` v3

-- ┌       ┐     ┌          ┐
-- | "foo" |  +  | "nabble" |  =  ?
-- | "bar" |     └          ┘
-- └       ┘

Теперь давайте поработаем с 2D матрицами. Хитрость заключается в том, чтобы построить их из более мелких многоразовых битов. Матрица — это вектор векторов, композиция двух векторов на уровне типов.

newtype (f :.: g) a = Compose { getCompose :: f (g a) } deriving Show

type Mat n m = Vec n :.: Vec m

То есть Mat n m a изоморфно Vec n (Vec m a).

Функциональность и аппликативность сохраняются за счет композиции,

instance (Functor f, Functor g) => Functor (f :.: g) where
    fmap f = Compose . fmap (fmap f) . getCompose
instance (Applicative f, Applicative g) => Applicative (f :.: g) where
    pure = Compose . pure . pure
    Compose fgf <*> Compose fgx = Compose (liftA2 (<*>) fgf fgx)

и мы можем еще раз использовать стандартный трюк, чтобы поднять Monoid в Applicative из составленных Applicatives.

instance (Monoid a, Applicative f, Applicative g) => Monoid ((f :.: g) a) where
    mempty = pure mempty
    mappend = liftA2 mappend

Теперь мы получаем сложение матриц бесплатно!

m1 :: Mat Two Two String
m1 = Compose (v1 :> v2 :> VNil)
m2 :: Mat Two Two String
m2 = Compose (v2 :> v1 :> VNil)

ghci> m1 `mappend` m2
Compose {getCompose = ("foobaz" :> ("barquux" :> VNil)) :> (("bazfoo" :> ("quuxbar" :> VNil)) :> VNil)}

-- ┌              ┐     ┌              ┐     ┌                    ┐
-- | "foo" "bar"  |  +  | "baz" "quux" |  =  | "foobaz" "barquux" |
-- | "baz" "quux" |     | "foo" "bar"  |     | "bazfoo" "quuxbar" |
-- └              ┘     └              ┘     └                    ┘

Есть еще одна допустимая матрица Monoid (для квадратных матриц newtype Square n = Square (Mat n n)), которая выполняет умножение матриц с единичной матрицей mempty. Я не буду показывать это здесь. Вы можете понять это сами.

Наконец, добавим тензоры, представляющие собой n-мерные матрицы. Тензор — это семейство типов, индексированных списком измерений. То есть Tensor — это функция из списка измерений в конструктор типа * -> *. Добавление нового измерения в список добавляет слой Vecs.

type family Tensor (dims :: [Nat]) :: * -> * where
    Tensor '[d] = Vec d
    Tensor (d ': ds) = Vec d :.: Tensor ds

Итак, Tensor '[One, Two, Three] a, тензор один на два на три, newtype-изоморфен Vec One (Vec Two (Vec Three a)).

Еще раз, определяя Tensor через Vec и :.:, мы бесплатно получаем нужный экземпляр.

t1 :: Tensor '[Two, Two, Two] String
t1 = Compose (m1 :> m2 :> VNil)
t2 :: Tensor '[Two, Two, Two] String
t2 = Compose (m2 :> m1 :> VNil)

ghci> t1 `mappend` t2
Compose {getCompose = Compose {getCompose = ("foobaz" :> ("barquux" :> VNil)) :> (("bazfoo" :> ("quuxbar" :> VNil)) :> VNil)} :> (Compose {getCompose = ("bazfoo" :> ("quuxbar" :> VNil)) :> (("foobaz" :> ("barquux" :> VNil)) :> VNil)} :> VNil)}

-- i'm not going to try drawing that