Как разрешить одному ограничению подразумевать другое в Haskell?

Question

Я экспериментирую с программированием на уровне типов, и я хотел реализовать несколько интересных примеров для таких вещей, как Num, позволяющих математические операторы с фиксированной длиной Vector s.

Некоторые из соответствующие части, которые у меня в настоящее время есть, следующие (в дополнение к экземпляру Functor):

data Nat = One
         | Succ Nat
             deriving (Show, Eq)

data Vector (n :: Nat) a where
  VecSing :: a -> Vector 'One a
  (:+) :: a -> Vector n a -> Vector ('Succ n) a

instance Num a => Num (Vector 'One a) where
  (+) = vecZipWith (+)
  (*) = vecZipWith (*)
  abs = fmap abs
  signum = fmap signum
  negate = fmap negate
  fromInteger = VecSing . fromInteger

instance (Num a, Num (Vector n a)) => Num (Vector ('Succ n) a) where
  (+) = vecZipWith (+)
  (*) = vecZipWith (*)
  abs = fmap abs
  signum = fmap signum
  negate = fmap negate
  fromInteger a = fromInteger a :+ fromInteger a

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

addAndMultiply :: (Num a) => Vector n a -> Vector n a -> Vector n a -> Vector n a
addAndMultiply a b c = (a + b) * c
-- Compilation error snippet:
-- Could not deduce (Num (Vector n a)) arising from a use of `*'
--      from the context: Num a

То, что я хотел бы, - это способ обозначить, что, когда у вас есть Num a, любые Vector n a также удовлетворяют ограничению Num.

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

Возможно ли это? Если да, то как?

Answer 1

Во-первых, вам действительно не нужно разбирать параметр размера в любых экземплярах num / vector-space. В любом случае реализация просто передает все в экземпляр Functor; если вы также реализуете Applicative один, вы можете все на основе этого, например

instance Num a => AdditiveGroup (Vector n a) where
  zeroV = pure 0
  negateV = fmap negate
  (^+^) = liftA2 (+)
instance Num a => VectorSpace (Vector n a) where
  type Scalar (Vector n a) = a
  μ *^ v = fmap (μ*) v

Но, конечно, это зависит от того, чтобы сначала иметь этот экземпляр Applicative для действительно произвольного n. Этот должен быть интуитивно возможен, поскольку оба конструктора Nat порождают экземпляры, но на самом деле компилятору нужна дополнительная помощь в виде класса типов. В стандартной версии nats уровня типов это KnownNat; для вашей собственной версии вы можете сделать это так:

{-# LANGUAGE GADTs, KindSignatures, TypeInType #-}
import Data.Kind

data NatS :: Nat -> Type where
  OneS :: NatS One
  SuccS :: KnownNat n => NatS (Succ n)

class KnownNat (n :: Nat) where
  natSing :: NatS n  -- I like to call such values “witnesses”, but
                     -- the conventional terminology is “singletons”.

instance KnownNat 'One where
  natSing = OneS
instance KnownNat n => KnownNat ('Succ n) where
  natSing = SuccS

Затем создайте экземпляры функтора на этом:

{-# LANGUAGE ScopedTypeVariables, UnicodeSyntax, TypeApplications #-}
instance ∀ n . KnownNat n => Functor (Vector n) where
  fmap f = case natSing @n of
    OneS -> \(VecSing x) -> VecSing $ f x
    SuccS -> \(x :+ v) -> f x :+ fmap f v

Аналогично для Applicative.

Тогда , для VectorSpace и c. экземпляров, вам больше не нужно явно обрабатывать эти синглтоны, просто укажите KnownNat n, и вы сможете использовать экземпляр Applicative.