Как создать ограниченный экземпляр на основе значений времени выполнения?

Я написал длинный ответ о хасохизме. экземпляр Matrix из Applicative, использующий конечные наборы в качестве типов индексов, но это, вероятно, излишне для того, что вы хотели, не говоря уже о менее эффективном, чем код на основе Array в сообщении блога.

Ваша проблема связана с тем, что различные операции в коде сообщения в блоге предполагают, что экземпляр Bounded для типа индекса матрицы является покрытием, в том смысле, что каждое значение в пределах границ будет иметь соответствующий элемент в матрица. Основное предположение, по-видимому, состоит в том, что размер матрицы известен статически.

Самый простой способ исправить это — изменить тип Matrix, чтобы он сохранял свой размер. Вам по-прежнему приходится выполнять динамическую проверку границ, но я думаю, что это довольно хороший компромисс по сравнению с весомостью подхода хасохизма.

-- Bounded as an explicit (minBound, maxBound) tuple
type Bounds i = (i, i)
data Matrix i e = Matrix { getBounds :: Bounds i, getMatrix :: Array (Edge i) e }

entireRange :: Ix i => Bounds i -> [i]
entireRange b = range b

matrix :: Ix i => Bounds i -> (Edge i -> e) -> Matrix i e
matrix bounds f = Matrix bounds $ listArray bounds $ map f $ entireRange bounds

Однако это застревает, когда вам нужно построить матрицу в экземпляре класса типа. Вы не можете абстрагировать экземпляры от значений времени выполнения: единственное допустимое значение слева от => в объявлении экземпляра — это другое ограничение класса типа. В декларации типа

instance Bounded i => Applicative (Matrix i) where
    pure x = matrix (const x)
    (<*>) = -- ...

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

Хорошие новости: вы можете эмулировать этот явный стиль передачи словаря, используя сумасшедшую библиотеку reflection, который делает злые, волшебные вещи, чтобы помещать значения времени выполнения в словари классов типов. Это страшная штука, но она работает и безопасна.

Все это происходит в reify и reflect комбинаторы. reify принимает значение времени выполнения и блок кода с ограничением, зависящим от доступности этого значения, и подключает их друг к другу. Вызовы reflect внутри блока возвращают значение, которое было передано reify вне его.

needsAnInt :: Reifies s Int => Proxy s -> IO ()
needsAnInt p = print (reflect p + 1)

example1 :: IO ()
example1 = reify 3 (\p -> needsAnInt p)  -- prints 4
example2 :: IO ()
example2 = reify 5 (\p -> needsAnInt p)  -- prints 6

Найдите минутку, чтобы подумать (ха-ха) о том, как это странно. Обычно для каждого типа существует только один словарь класса (несмотря на перекрывающиеся экземпляры). Proxy имеет только одно значение (data Proxy a = Proxy), так как же reflect может различать два прокси, чтобы каждый раз возвращать разные значения?

В любом случае, какой в ​​этом смысл? Экземпляры не могут зависеть от значений среды выполнения, но могут зависеть от других экземпляров. reflection дает нам инструменты для превращения значения времени выполнения в словарь экземпляров, так что это позволяет нам создавать экземпляры, которые динамически зависят от значений времени выполнения!

В данном случае мы создаем экземпляр Bounded. Нам нужен newtype, чтобы создать экземпляр, который не пересекается ни с какими другими:

-- in this case it's fine to just lift the Ix instance from the underlying type
newtype B s i = B i deriving (Eq, Ord, Ix)

Ясно, что B может быть экземпляром Bounded, если i есть - он может получить minBound и maxBound из экземпляра i, но мы хотим получить их из контекста Reifies. Другими словами, значение времени выполнения, которое мы будем помещать в словарь Reifies, будет парой i.

instance Reifies s (i, i) => Bounded (B s i) where
    minBound = B $ fst $ reflect (Proxy :: Proxy s)
    maxBound = B $ snd $ reflect (Proxy :: Proxy s)

Я использую ScopedTypeVariables крайне важно, чтобы получить значения Proxy правильного типа.

Теперь вы можете написать совершенно обычный код, который использует контекст Bounded (даже если этот контекст возникает из-за какого-то другого экземпляра), и вызывать его с помощью динамически созданного словаря Bounded, используя reify.

entireRange :: (Ix i, Bounded i) => [i]
entireRange = range (minBound, maxBound)

example3 :: IO ()
example3 = reify (3, 6) myComputation
    where myComputation :: forall s. Bounded (B s Int) => Proxy s -> IO ()
          myComputation p = print $ map unB (entireRange :: [B s Int])

ghci> example3
[3,4,5,6]

Эм, да. reflection может быть сложно использовать. В конце концов, наверное, проще просто не заморачиваться с занятиями.

Сегодня в Великобритании выходной, поэтому у меня было время закончить ответ о матрицах статического размера. Я бы не рекомендовал делать это в продакшене — даже если не принимать во внимание глупость кода, это ужасное представление матриц, если вы хотите выполнять эффективную линейную алгебру на реальном оборудовании — но это довольно весело. возиться с.

Из Хазохизм:

-- Natural numbers and their singletons in explicit and implicit varieties
data Nat = Z | S Nat  -- page 2 of the paper
intToNat :: Int -> Maybe Nat  -- paraphrased from page 10
intToNat n
    | n < 0     = Nothing
    | n == 0    = Just Z
    | otherwise = S <$> intToNat (n-1)
data Natty n where  -- page 2
    Zy :: Natty Z
    Sy :: Natty n -> Natty (S n)
-- page 3
class NATTY n where
    natty :: Natty n
instance NATTY Z where
    natty = Zy
instance NATTY n => NATTY (S n) where
    natty = Sy natty

-- turn an explicit Natty into an implicit one
natter :: Natty n -> (NATTY n => r) -> r  -- page 4
natter Zy r = r
natter (Sy n) r = natter n r

-- vectors, matrices in row-major order
data Vec n a where  -- page 2
    V0 :: Vec Z a
    (:>) :: a -> Vec n a -> Vec (S n) a
newtype Mat w h a = Mat { unMat :: Vec h (Vec w a) }  -- page 4

-- vector addition, in the form of an Applicative instance
vcopies :: Natty n -> a -> Vec n a  -- page 4
vcopies Zy x = V0
vcopies (Sy n) x =  :> vcopies n x
vapp :: Vec n (a -> b) -> Vec n a -> Vec n b  -- page 4
vapp V0 V0 = V0
vapp (f :> fs) (x :> xs) = f x :> vapp fs xs
instance NATTY n => Applicative (Vec n) where  -- page 4
    pure = vcopies natty
    (<*>) = vapp

-- iterating vectors
instance Traversable (Vec n) where  -- page 4
    traverse f V0 = pure V0
    traverse f (x :> xs) = liftA2 (:>) (f x) (traverse f xs)
instance Foldable (Vec n) where  -- page 4
    foldMap = foldMapDefault
instance Functor (Vec n) where  -- page 4
    fmap = fmapDefault

transpose :: NATTY w => Mat w h a -> Mat h w a  -- page 4
transpose = Mat . sequenceA . unMat

Я позволил себе переименовать авторский тип Matrix в Mat, переставить его аргументы типа и изменить его с GADT на новый тип. Простите меня за то, что я пропускаю объяснение вышеизложенного - статья работает лучше, чем я мог бы, и я хочу перейти к той части, где я отвечаю на ваш вопрос.

Mat w h является h-вектором из w-векторов. Это композиция на уровне типов. двух функторов Vec. Его экземпляр Applicative, который реализует сложение матриц, отражает эту структуру,

instance (NATTY w, NATTY h) => Applicative (Mat w h) where
    pure = Mat . pure . pure
    Mat fss <*> Mat xss = Mat $ liftA2 (<*>) fss xss

как и его экземпляр Traversable.

instance Traversable (Mat w h) where
    traverse f = fmap Mat . traverse (traverse f) . unMat
instance Foldable (Mat w h) where
    foldMap = foldMapDefault
instance Functor (Mat w h) where
    fmap = fmapDefault

Также нам понадобится немного оборудования для работы с индексами векторов. Чтобы идентифицировать конкретный элемент в n-векторе, вы должны указать число меньше n.

data Fin n where
    FZ :: Fin (S n)
    FS :: Fin n -> Fin (S n)

Тип Fin n содержит ровно n элементов, поэтому Fin — это семейство конечных множеств. Значение типа Fin n структурно является натуральным числом, меньшим n (сравните FS FZ с S Z), поэтому FS FZ :: Fin (S (S Z)) или FS FZ :: Fin (S (S (S Z))), но FS FZ :: Fin (S Z) не пройдет проверку типа.

Вот функция более высокого порядка, которая строит вектор, содержащий все возможные результаты своего аргумента.

tabulate :: Natty n -> (Fin n -> a) -> Vec n a
tabulate Zy f = V0
tabulate (Sy n) f = f FZ :> tabulate n (f . FS)

Теперь можно приступить к работе с полукольцами. Скалярное произведение двух векторов включает в себя умножение их элементов и последующее суммирование результата.

dot :: Semiring a => Vec n a -> Vec n a -> a
dot xs ys = foldr (<+>) zero $ vapp (fmap (<.>) xs) ys

Вот вектор, который равен zero везде, кроме указанного индекса.

oneAt :: Semiring a => Natty n -> Fin n -> Vec n a
oneAt (Sy n) FZ = one :> vcopies n zero
oneAt (Sy n) (FS f) = zero :> oneAt n f

Мы будем использовать oneAt и tabulate для создания матрицы идентичности.

type Square n = Mat n n

identity :: Semiring a => Natty n -> Square n a
identity n = Mat $ tabulate n (oneAt n)

ghci> identity (Sy (Sy Zy)) :: Square (S (S Z)) Int
Mat {unMat = (1 :> (0 :> V0)) :> ((0 :> (1 :> V0)) :> V0)}
-- ┌      ┐
-- │ 1, 0 │
-- │ 0, 1 │
-- └      ┘

И transpose пригодится для умножения матриц.

mul :: (NATTY w, Semiring a) => Mat r h a -> Mat w r a -> Mat w h a
mul m n =
    let mRows = unMat m
        nCols = unMat $ transpose n
    in Mat $ fmap (\r -> dot r <$> nCols) mRows

ghci> let m = Mat $ (1 :> 2 :> V0) :> (3 :> 4 :> V0) :> V0 :: Square (S (S Z)) Int in mul m m
Mat {unMat = (7 :> (10 :> V0)) :> ((15 :> (22 :> V0)) :> V0)}
-- ┌      ┐2   ┌        ┐
-- │ 1, 2 │  = │  7, 10 │
-- │ 3, 4 │    │ 15, 22 │
-- └      ┘    └        ┘

Итак, экземпляр Semiring для квадратных матриц отсортирован. Фу!

instance (NATTY n, Semiring a) => Semiring (Square n a) where
    zero = pure zero
    (<+>) = liftA2 (<+>)
    one = identity natty
    (<.>) = mul

Что следует отметить в этой реализации, так это то, что zero и one динамически создают матрицы статически известного размера, обычно на основе контекстной информации о типе в месте вызова. Они получают представление этого размера во время выполнения (Natty) из словаря NATTY, который разработчик строит на основе предполагаемого типа матрицы.

Это совершенно другой подход, чем в библиотеке reflection (о которой я рассказал в другом моем ответе). reflection — это вставка явных значений времени выполнения в неявные словари экземпляров, тогда как этот стиль берет информацию, которая в противном случае была бы известна только во время выполнения — размер матрицы — и делает ее статической, используя одиночные элементы, чтобы сделать информацию о типе доступной в мире значений. . Конечно, настоящий язык с зависимой типизацией обошелся бы с Natty церемонией: n было бы обычным старым значением, и мы могли бы использовать его напрямую, вместо того, чтобы проходить через синглетон, скрытый в словаре экземпляров.

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

Как мы можем использовать эти матрицы со статическими размерами, если мы не знаем размер статически? Вы упомянули, что ваша программа спрашивает пользователя, насколько велик его граф (и, следовательно, насколько велика матрица смежности, используемая для представления графа). Итак, пользователь вводит число (Nat-значение, а не Nat-тип), и мы каким-то образом должны статически знать, что пользователь собирался ввести?

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

withNatty :: Nat -> (forall n. Natty n -> r) -> r
withNatty Z r = r Zy
withNatty (S n) r = withNatty n (r . Sy)

withNatty n r применяет функцию r к одноэлементному представлению натурального числа n. r имеет Natty n, доступный во время выполнения, поэтому он может восстановить статические знания n по шаблону, соответствующему Natty, но n не может просочиться за пределы блока. (Вы также можете использовать экзистенциальную количественную оценку, которая кратко описана в Хазохизме, чтобы обернуть Natty и передавать ее повсюду. Это то же самое.)

Так, например, предположим, что мы хотим напечатать единичную матрицу динамически определяемого размера:

main = do
    Just size <- fmap intToNat readLn
    withNatty size (print . mkIdentity)
        where mkIdentity :: Natty n -> Square n Int
              mkIdentity n = natter n one

ghci> main
4
Mat {unMat = (1 :> (0 :> (0 :> (0 :> V0)))) :> ((0 :> (1 :> (0 :> (0 :> V0)))) :> ((0 :> (0 :> (1 :> (0 :> V0)))) :> ((0 :> (0 :> (0 :> (1 :> V0)))) :> V0)))}

Тот же метод применяется, если вы хотите, скажем, построить матрицу из списка списков. На этот раз это немного сложнее, потому что вам нужно доказать GHC, что все списки имеют одинаковую длину, путем их измерения.

withVec :: [a] -> (forall n. NATTY n => Vec n a -> r) -> r
withVec [] r = r V0
withVec (x:xs) r = withVec xs (r . (x :>))


-- this operation can fail because the input lists may not all be the same length
withMat :: [[a]] -> (forall w h. (NATTY w, NATTY h) => Mat w h a -> r) -> Maybe r
withMat xss r = assertEqualLengths xss (\vs -> withVec vs (r . Mat))
    where assertEqualLengths :: [[a]] -> (forall n. NATTY n => [Vec n a] -> r) -> Maybe r
          assertEqualLengths [] r = Just (r noVecs)
          assertEqualLengths xss@(xs:_) r = withLen xs (\n -> natter n $ r <$> traverse (assertLength n) xss)

          noVecs :: [Vec Z a]
          noVecs = []

          assertLength :: Natty n -> [a] -> Maybe (Vec n a)
          assertLength Zy [] = Just V0
          assertLength (Sy n) (x:xs) = fmap (x :>) (assertLength n xs)
          assertLength _ _ = Nothing

          withLen :: [a] -> (forall n. Natty n -> r) -> r
          withLen [] r = r Zy
          withLen (x:xs) r = withLen xs (r . Sy)

ghci> withMat [[1,2], [3,4]] show
Just "Mat {unMat = (1 :> (2 :> V0)) :> ((3 :> (4 :> V0)) :> V0)}"
ghci> withMat [[1,2], [3]] show  -- a ragged input list
Nothing

И если вы хотите работать с квадратными матрицами, вы должны доказать GHC, что высота матрицы равна ее ширине.

withEqual :: Natty n -> Natty m -> (n ~ m => r) -> Maybe r
withEqual Zy Zy r = Just r
withEqual (Sy n) (Sy m) r = withEqual n m r
withEqual _ _ _ = Nothing

square :: Natty w -> Natty h -> Mat w h a -> Maybe (Square w a)
square = withEqual