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

11
votes

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.)

2
haskell
You should write it like instance (Num t, Applicative (Vector n)) => Num (Vector n t) where since otherwise you can indeed not use (<*>). – Willem Van Onsem
Thanks a lot, I somehow wrongly assumed that the compiler knows that all (Vector n) are Applicatives. – John Poe
@JohnPoe Counter-intuitively, not all of them are applicatives, for very subtle reasons. If F x :: Nat is a type family which gets "stuck" (say, F Bool is not defined) the compiler is not allowed to resolve, say, Applicative (Vector (F Bool)) since it can not evaluate F Bool to a concrete Nat, so it can not choose an instance. It is weird to have type-expressions of kind Nat which do not evaluate to a concrete Nat, but that's how GHC works. – chi
@chi: Thank you very much for your explanation, but it might be beyond my current understanding of haskell. Do I understand correctly that the problem is the n in Vector n t, as the compiler has to be able to prove that it is either a Z or N x for a concrete Nat x, which it cannot, as someone might plug in a "weird thing" for n that only "claims" to be a Nat? – John Poe
@JohnPoe Yes, that's a nice way to put it. Your instances will be used only when there is an explicit Z or N x in the type. If there is a type variable like n or a "stuck" type family F Bool, GHC does not know what instance to pick and will not resolve the constraint. There are some ways around that, e.g. exploiting suitable GADTs to prove "n is indeed one of the two possible forms" -- this is a bit advanced, however, so I'd recommend to get familiar with GADTs first. – chi

2 Answers

5
votes

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.

2
votes

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'