How to define a usable Applicative instance for a vector type enforcing length 2^n

Question

For some application I need vectors of length $2^n$. To enforce that the lengths match for some operations, I defined my type with ist applicative instance as follows:

{-# LANGUAGE GADTs, DataKinds, FlexibleInstances, FlexibleContexts #-}
data Nat = Z | N Nat
data Vector n t where
  S :: t -> Vector Z t
  V :: Vector n t -> Vector n t -> Vector (N n) t

instance Functor (Vector n) where
  fmap f (S t ) = S (f t)
  fmap f (V t t') = V (fmap f t) (fmap f t')

instance Applicative (Vector Z) where
  pure = S
  S f <*> S a = S (f a)

instance Applicative (Vector n) => Applicative (Vector (N n)) where
  pure a = let a' = pure a in V a' a'
  V f f' <*> V a a' = V (f <*> a) (f' <*> a')

The language extensions I chose as suggested by ghci to make the code compile. The whole structure is inspired by How to make fixed-length vectors instance of Applicative?.

Trouble starts when I try to use it:

instance Num t => Num (Vector n t) where
  v + v' = (+) <$> v <*> v'
  (*) = undefined
  abs = undefined
  signum = undefined
  fromInteger = undefined
  negate = undefined

Adding these lines Triggers following error:

• Could not deduce (Applicative (Vector n)) arising from a use of ‘<*>’ from the context: Num t bound by the instance declaration at ...

• In the expression: (+) v <> v' In an equation for ‘+’: v + v' = (+) v <> v' In the instance declaration for ‘Num (Vector n t)’

I'm using Haskell Platform 8.0.2-a on Windows 7.

Any idea what's going? In the linked question the same trick seems to work!? (Adding KindSignatures in the first line does not help, and without FlexibleInstances/Contexts I get a Compiler error.)

Answer 1

You should add a type constraint in your Num (Vector n t) instance declaration, that specifies that Vector n a is an instance of Applicative, otherwise you can not use (<*>) here.

You thus can fix the problems with:

instance (Num t, Applicative (Vector n)) => Num (Vector n t) where
  v + v' = (+) <$> v <*> v'
  -- ...

We here thus say that Vector n t is an instance of Num given t is an instance of Num, and Vector n is an instance of Applicative.

Since you defined your instance Applicative for your Vector n in such way that it holds for all ns, all Vector n ts are members of Num given Num t, regardless of the value for n, but it needs to be part of the signature of the instance declaration.

Answer 2

I think it's a bit nicer to use an auxiliary class. I also tend to prefer liftA2 to <*> for instances, so I'll use that; it's not essential. Note that you only need to differentiate between sizes for pure; the zipping operation doesn't need that. There's a trade-off: if you make the zipping operation a method, then it'll tend to inline, whereas if it's a function it generally won't. This could balance code size against speed when the vectors are small enough. Still, this is how I'd probably do it.

class App' n where
  pure' :: a -> Vector n a

instance App' 'Z where
  pure' = S

instance App' n => App' ('N n) where
  pure' a = let a' = pure' a in V a' a'

liftA2'
  :: (a -> b -> c)
  -> Vector n a
  -> Vector n b
  -> Vector n c
liftA2' f = \xs -> go xs
  where
    go (S x) (S y) = S (f x y)
    go (V l1 r1) (V l2 r2) =
      V (go l1 l2) (go r1 r2)

instance App' n => Applicative (Vector n) where
  pure = pure'
  -- import Control.Applicative to get the liftA2 method
  liftA2 = liftA2'