How do I allow one Constraint to imply another in Haskell?

Question

I am playing around with some type-level programming, and I wanted to implement some interesting instances for things like Num, allowing mathematical operators on fixed-length Vectors.

Some of the pertinent parts I currently have are as follows (in addition to a Functor instance):

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

However, I have come up with an issue when I actually want to use these instances. This is due to the fact, as much as I can surmise, that whenever I want to add two Vectors together, I have to specify that they are, in fact, instances of Num, such as in the below example.

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

What I would like is a way to imply that, when you have a Num a, any Vector n as also fulfill the constraint Num.

I tried to look at this solution, and this one, but I don't think these are quite the same thing; the question-askers usually have a data type that takes a constraint, and does things with the boxed value, while I just want to implicitly imply a constraint from another one; or at least, I think I do.

Is this possible? If so, how?

Please let me know if any additional information is required; the current code base state can be seen at https://github.com/L0neGamer/matrix-pkg if you want to take a dive yourself. — L0neGamer, May 27 '20 at 09:16
Unrelated to the actual question, but: please don't write `Num` instances for non-scalar vector types. The behaviour of `fromIntegral` doesn't really make sense for those; this has led to some nasty hard-to-find bugs for me when using e.g. [`Linear.V3`](https://hackage.haskell.org/package/linear-1.21/docs/Linear-V3.html). The correct typeclass to instantiate is [`VectorSpace`](https://hackage.haskell.org/package/vector-space-0.16/docs/Data-VectorSpace.html). — leftaroundabout, May 27 '20 at 09:24
@leftaroundabout that's reasonable; this is mostly a project for my own entertainment, but I do like learning about the correct way to do things, so thanks for the VectorSpace recommendation. — L0neGamer, May 27 '20 at 09:29

leftaroundabout · Accepted Answer · 2020-05-27T11:21:23.587

First off, you don't really need to deconstruct the size-parameter in any num/vector-space instances. Anyway the implementation basically just passes everything through to the Functor instance; if you also implement an Applicative one then you can to everything based on that, like

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

But of course this relies on first having that Applicative instance for really arbitrary n. This should intuitively be possible since both constructors of Nat give rise to instances, but actually the compiler needs some extra help in form of a typeclass. In the standard version of type-level nats, this is KnownNat; for your own version you could do it like this:

{-# 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

Then base the functor instances on that:

{-# 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

Similarly for Applicative.

Then, for the VectorSpace etc. instances, you don't need to explicitly handle those singletons anymore, just mention KnownNat n and you'll be able to exploit the Applicative instance.

This doesn't seem to work for me; I have implemented `Applicative`s in the manner described (having previously implemented `Functor`s without having to use `KnownNat`), but your code is complaining that couldn't deduce a "zeroV" for the AdditiveGroup. The ability to define Applicatives and the like with only using one instance is nice though; previously I had to recursively define the instances (`instance Applicative (Vector 'One) where`, then `instance Applicative (Vector n) => Applicative (Vector ('Succ n)) where`) — L0neGamer, May 27 '20 at 10:37
The error about `zeroV` is because when you don't define it manually it tries to auto-generate an implementation based on Generics, but that doesn't work in this case. Just define `zeroV = pure 0`. — leftaroundabout, May 27 '20 at 10:46
Alright, that fix worked; additionally, I had to add `KnownNat n` to the instances of `AdditiveGroup` and `VectorSpace`, and change `type Scalar (Vector a) = a` to `type Scalar (Vector n a) = a`. — L0neGamer, May 27 '20 at 10:58

How do I allow one Constraint to imply another in Haskell?

1 Answers1