Использование индуктивно определенных аппликативных экземпляров на типовых безопасных векторах

Question

Я пытаюсь записать Category ^{(конечномерных свободных)} векторных пространств, но я не могу убедить GHC, что любой заданный индексированный вектор длины Applicative,

вот что у меня есть:

{-# LANGUAGE DataKinds, PolyKinds, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts, GADTs, DeriveTraversable, StandaloneDeriving #-}

-- | Quick(slow) and dirty typesafe vectors
module Vector where
import Control.Category

Векторы - это списки с параметром длины

data Natural = Z | S Natural
data Vec (n :: Natural) a where
  VNil :: Vec Z a
  VCons :: a -> Vec n a -> Vec (S n) a
deriving instance Functor (Vec n)
deriving instance Foldable (Vec n)
deriving instance Traversable (Vec n)

Чтобы получить категорию, нам нужно матричное умножение. Очевидная реализация заставляет индексы немного отступить от того, что мы обычно хотим.

vmult :: Num a => Vec i (Vec k a) -> Vec j (Vec k a) -> Vec j (Vec i a)
--                    ^      ^           ^      ^           ^      ^
vmult _ VNil = VNil
vmult xs (VCons y ys) = VCons (dotProduct y <$> xs) $ vmult xs ys

dotProduct :: Num a => Vec n a -> Vec n a -> a
dotProduct VNil VNil = 0
dotProduct (VCons x xs) (VCons y ys) = x * y + dotProduct xs ys

РЕДАКТИРОВАТЬ

с помощью @ Проби мне удалось решить более раннюю проблему, которой достаточно, чтобы определить экземпляр для Semigroupoid s

data KNat n where
  KZ :: KNat Z
  KS :: Finite n => KNat n -> KNat (S n)

class Finite (a :: Natural) where toFNat :: proxy a -> KNat a
instance Finite Z where toFNat _ = KZ
instance Finite n => Finite (S n) where toFNat _= KS (toFNat (Proxy :: Proxy n))

instance Finite n => Applicative (Vec n) where
  pure :: forall a. a -> Vec n a
  pure x = go (toFNat (Proxy :: Proxy n))
    where
      go :: forall (m :: Natural). KNat m -> Vec m a
      go KZ = VNil
      go (KS n) = VCons x $ go n

  (<*>) :: forall a b. Vec n (a -> b) -> Vec n a -> Vec n b
  nfs <*> nxs = go (toFNat (Proxy :: Proxy n)) nfs nxs
    where
      go :: forall (m :: Natural). KNat m -> Vec m (a -> b) -> Vec m a -> Vec m b
      go KZ VNil VNil = VNil
      go (KS n) (VCons f fs) (VCons x xs) = VCons (f x) (go n fs xs)

data Matrix a i j where
  Matrix :: (Finite i, Finite j) => Vec i (Vec j a) -> Matrix a i j

instance Num a => Semigroupoid (Matrix a) where
  Matrix x `o` Matrix y = Matrix (vmult (sequenceA x) y)

но я сталкиваюсь с аналогичной проблемой, как и раньше при определении Category.id:

instance Num a => Category (Matrix a) where
  (.) = o
  id :: forall (n :: Natural). Matrix a n n
  id = Matrix (go (toFNat (Proxy :: Proxy n)))
    where
      go :: forall (m :: Natural). (KNat m) -> Vec m (Vec m a)
      go KZ = VNil
      go (KS n) = VCons (VCons 1 (pure 0)) (VCons 0 <$> go n)

Вместо того, чтобы вызвать Applicative (Vec n) из воздуха мне сейчас нужна Finite n,

src/Vector.hs:59:8: error:
    • Could not deduce (Finite n) arising from a use of ‘Matrix’
      from the context: Num a
        bound by the instance declaration at src/Vector.hs:56:10-37
      Possible fix:
        add (Finite n) to the context of
          the type signature for:
            Control.Category.id :: forall (n :: Natural). Matrix a n n
    • In the expression: Matrix (go (toFNat (Proxy :: Proxy n)))
      In an equation for ‘Control.Category.id’:
          Control.Category.id
            = Matrix (go (toFNat (Proxy :: Proxy n)))
            where
                go :: forall (m :: Natural). (KNat m) -> Vec m (Vec m a)
                go KZ = VNil
                go (KS n) = VCons (VCons 1 (pure 0)) (VCons 0 <$> go n)
      In the instance declaration for ‘Category (Matrix a)’
   |
59 |   id = Matrix (go (toFNat (Proxy :: Proxy n)))
   |        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Кажется, нет никакого выхода из необходимости побочных условий для этого.

конец редактирования

---

Для контекста, это то, что я имел раньше, Vec n индуктивно Applicative

instance Applicative (Vec Z) where
  pure _ = VNil
  _ <*> _ = VNil
instance Applicative (Vec n) => Applicative (Vec (S n)) where
  pure a = VCons a $ pure a
  VCons f fs <*> VCons x xs = VCons (f x) (fs <*> xs)

чтобы получить экземпляр категории, нам нужно изменить a за индексами...

data Matrix a i j where
  Matrix :: Vec i (Vec j a) -> Matrix a i j

Но нет никакой возможности переставить сами индексы, не переставив тоже ни одного из терминов...

instance Num a => Category (Matrix a) where
  Matrix x . Matrix y = Matrix $ (vmult (sequenceA x) y)
--                                       ^^^^^^^^^

Тем не мение:

src/Vector.hs:36:42: error:
    • Could not deduce (Applicative (Vec c))
        arising from a use of ‘sequenceA’
      from the context: Num a
        bound by the instance declaration at src/Vector.hs:35:10-37
    • In the first argument of ‘vmult’, namely ‘(sequenceA x)’
      In the second argument of ‘($)’, namely ‘(vmult (sequenceA x) y)’
      In the expression: Matrix $ (vmult (sequenceA x) y)
   |
36 |   Matrix x . Matrix y = Matrix $ (vmult (sequenceA x) y)
   |                                          ^^^^^^^^^^^

Answer 1

Я не слишком много играл с зависимыми типами в Haskell, но это похоже на то, что должно быть возможно. Мне удалось получить что-то, что компилируется, но я думаю, что есть лучший способ...

Хитрость заключается в том, чтобы иметь возможность производить что-то, за что вы можете справиться, что несет в себе достаточную информацию о типе без необходимости уже иметь Vector, Это позволяет нам свести оба экземпляра Applicative в один экземпляр Applicative (к сожалению, добавив ограничение, Finite что, надеюсь, не вызовет проблем позже)

{-# LANGUAGE DataKinds, PolyKinds, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts, GADTs, DeriveTraversable, StandaloneDeriving, ScopedTypeVariables #-}

module Vector where
import Control.Category
import Data.Proxy

data Natural = Z | S Natural

data SNat n where
  SZ :: SNat Z
  SS :: Finite n => SNat n -> SNat (S n)

class Finite (a :: Natural) where
  toSNat :: proxy a -> SNat a

instance Finite Z where
  toSNat _ = SZ
instance (Finite a) => Finite (S a) where
  toSNat _ = SS (toSNat (Proxy :: Proxy a))

data Vec (n :: Natural) a where
  VNil :: Vec Z a
  VCons :: (Finite n) => a -> Vec n a -> Vec (S n) a

deriving instance Functor (Vec n)
deriving instance Foldable (Vec n)
deriving instance Traversable (Vec n)

instance (Finite n) => Applicative (Vec n) where
  pure (a :: a) = go (toSNat (Proxy :: Proxy n))
    where go :: forall (x :: Natural) . SNat x -> Vec x a
          go SZ = VNil
          go (SS m) = VCons a (go m)
  (fv :: Vec n (a -> b)) <*> (xv :: Vec n a) = go (toSNat (Proxy :: Proxy n)) fv xv
    where go :: forall (x :: Natural) . SNat x -> Vec x (a -> b) -> Vec x a -> Vec x b
          go SZ VNil VNil = VNil
          go (SS m) (VCons f fs) (VCons x xs) = VCons (f x) (go m fs xs)

vmult :: Num a => Vec i (Vec k a) -> Vec j (Vec k a) -> Vec j (Vec i a)
vmult _ VNil = VNil
vmult xs (VCons y ys) = VCons (dotProduct y <$> xs) $ vmult xs ys

dotProduct :: Num a => Vec n a -> Vec n a -> a
dotProduct VNil VNil = 0
dotProduct (VCons x xs) (VCons y ys) = x * y + dotProduct xs ys

data Matrix a i j where
  Matrix :: (Finite i, Finite j) => Vec i (Vec j a) -> Matrix a i j

instance Num a => Category (Matrix a) where
  Matrix x . Matrix y = Matrix $ (vmult (sequenceA x) y)

Редактировать: Matrix не категория Там нет идентичности - мы требуем forall (n :: Natural) . Matrix a n n

К сожалению, все виды в Haskell населяются Any так что мы должны иметь возможность Matrix a Any Any, но у нас могут быть только матрицы, размеры которых "истинны" Natural S, так что лучшее, что мы можем сделать, это forall (n :: Natural) . Finite n => Matrix a n n Оказывается, я здесь не прав, и это действительно можно сделать

Answer 2

После небольшого доказательства запугиванием (и нескольких часов в поезде) я придумал это.

Если вы отложите доказательство FiniteКонечно, вы можете умножить все, что угодно... термины, которые мы хотим написать, являются прямыми.

vdiag :: forall a i j. a -> a -> a -> KNat i -> KNat j -> Vec i (Vec j a)
vdiag u d l = go
  where
    go :: forall i' j'. KNat i' -> KNat j' -> Vec i' (Vec j' a)
    go (KS i) (KS j) =
      VCons (VCons d  $  vpure u j)
            (VCons l <$> go i j)
    go KZ _ = VNil
    go (KS i) KZ = vpure VNil (KS i)

vpure :: a -> KNat m -> Vec m a
vpure x KZ = VNil
vpure x (KS n) = VCons x $ vpure x n

Но мы не знаем, что i а также j будет, когда нам действительно нужно использовать их для Category.id (кроме этого они равны). Мы их CPS! Дополнительный конструктор для Matrix a дается с ограничением ранга 2.

data Matrix a i j where
  DiagonalMatrix :: (Finite i => KNat i -> Vec i (Vec i a)) -> Matrix a i i
--                  ^^^^^^^^^                             ^
  Matrix :: (Finite i, Finite j) => Vec i (Vec j a) -> Matrix a i j

Каждый раз, когда нам нужно умножить такие вещи, мы можем использовать тот факт, что мы знаем внутренний индекс k из другого умножаемого члена:

instance Num a => Semigroupoid (Matrix a) where
  o :: forall a i j k. Num a => Matrix a k j -> Matrix a i k -> Matrix a i j
  Matrix x          `o` Matrix y          =
      Matrix (vmult (sequenceA   x                             )   y)
  DiagonalMatrix fx `o` Matrix y          =
      Matrix (vmult (sequenceA (fx (toFNat (Proxy :: Proxy k))))   y)
  Matrix x          `o` DiagonalMatrix fy = 
      Matrix (vmult (sequenceA   x                             ) (fy (toFNat (Proxy :: Proxy k))))

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

  DiagonalMatrix fx `o` DiagonalMatrix fy = DiagonalMatrix $ 
      \i -> vmult (sequenceA (fx i)) (fy i)

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

В любом случае, мы закончили, id это CPS'd vdiag,

instance Num a => Category (Matrix a) where
  (.) = o
  id = DiagonalMatrix $ \i -> vdiag 0 1 0 i i

конечно, извлечение строк и столбцов из Matrix a требует, чтобы вы знали, насколько велика матрица, которую вы просили.

unMatrix :: (Finite i, Finite j) => Matrix a i j -> Vec i (Vec j a)
unMatrix (Matrix x) = x
unMatrix (DiagonalMatrix fx) = fx (toFNat (Proxy))

type Zero = Z
type One = S Z
type Two = S One
type Three = S Two
type Four = S Three

f :: Vec Two (Vec Three Int)
f = VCons (VCons 1 $ VCons 2 $ VCons 3 VNil)
  $ VCons (VCons 4 $ VCons 5 $ VCons 6 VNil)
  $ VNil

g :: Vec Four (Vec Two Int)
g = VCons (VCons 1 $ VCons 2 VNil)
  $ VCons (VCons 3 $ VCons 4 VNil)
  $ VCons (VCons 5 $ VCons 6 VNil)
  $ VCons (VCons 7 $ VCons 8 VNil)
  $ VNil

fg = unMatrix $ Matrix f . id . Matrix g
--                         ^^

но это не слишком большое обязательство.

> fg
VCons (VCons 9 (VCons 12 (VCons 15 VNil))) (VCons (VCons 19 (VCons 26 (VCons 33 VNil))) (VCons (VCons 29 (VCons 40 (VCons 51 VNil))) (VCons (VCons 39 (VCons 54 (VCons 69 VNil))) VNil)))

для полноты вот что: https://gist.github.com/danbornside/f44907fe0afef17d5b1ce93dd36ce84d