More Applicative trouble with a vector type enforcing length 2^n

Question

Sorry for the botched up first version of the simplified function, I hope that the updated second version below makes more sense. Sorry also for the non-standard notation, but I didn't/don't care much about the auxiliary type Nat and preferred to save some typing for my "scalar vectors" (for my next question I promise to value the sanity of my readers higher, and adapt my code before posting).

---

I'm using the same vector type constrained to have $2^n$ elements as in my question few hours ago:

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

instance (Num t, Applicative (Vector n)) => Num (Vector n t) where
  v + v' = (+) <$> v <*> v'
  v * v' = (*) <$> v <*> v'
  abs = fmap abs
  signum = fmap signum
  fromInteger = pure . fromInteger
  negate = fmap negate

Now I failed to implement a quite complex recursive function that I cannot reproduce here, but the essence of my problems can be seen in this much simpler function (that doesn't make much sense, sorry):

dummy :: Applicative (Vector n) => Vector n Int -> Vector n Int -> Int
dummy (S a) (S b)       = a + b
dummy (V a a') (V b b') = dummy (a*b) (a'*b')

The error message my compiler (ghci, still Haskell Platform 8.0.2-a on Windows 7) gives me is (slightly shortened):

• Could not deduce (Applicative (Vector n2))
    arising from a use of ‘dummy’
  from the context: Applicative (Vector n)
    bound by the type signature for:
               dummy :: Applicative (Vector n) =>
                        Vector n Int -> Vector n Int -> Int
    at ...
  or from: n ~ 'N n2
    bound by a pattern with constructor:
               V :: forall t (n :: Nat).
                    Vector n t -> Vector n t -> Vector ('N n) t,
             in an equation for ‘dummy’
    at ...
• In the expression: dummy (a * b) (a' * b')
  In an equation for ‘dummy’:
      dummy (V a a') (V b b') = dummy (a * b) (a' * b')

To me it looks similar to the problem in this question.

I tried way around it, by defining separately

dummy :: Applicative (Vector Z) => Vector n Int -> Vector n Int -> Int
dummy = ...

and

dummy :: Applicative (Vector n) => Vector (N n) Int -> Vector (N n) Int -> Int
dummy = ...

but then the Compiler complains

...: error:
  Duplicate type signatures for ‘dummy’
  at ...

Do I have to define a type class with the only function dummy and then make Vector Z and (Vector (N n)) instances of it?

class Dummy d where
  dummy :: d -> d -> Int
instance Dummy (Vector Z Int) where
  dummy (S a) (S b) = a + b
instance (Applicative (Vector n), Dummy (Vector n Int)) => Dummy (Vector (N n) Int) where
  dummy (V a a') (V b b') = dummy (a*b) (a'*b')

The compiler takes it, but is there no better way to do it?

---

I guess dfeuer's answer contains a better solution, but I wasn't able to adapt it to my definition of Nat (yet).

Answer 1

Good question! One way to do this is to recover an Applicative instance just in time, recursing over the spine of the tree when we discover we need it. So:

{-# LANGUAGE RankNTypes #-}
withApplicative :: Vector n t -> (Applicative (Vector n) => a) -> a
withApplicative S{} a = a
withApplicative (V v _) a = withApplicative v a

Armed with this, we can call for the appropriate instance without putting it in our context:

dummy :: Vector n Int -> Vector n Int -> Int
dummy (S a) (S b) = a + b
dummy (V a a') (V b b') = withApplicative a (dummy (a*b) (a'*b'))

Since withApplicative is linear in the depth of your tree, and we call withApplicative once at each depth, this adds a runtime component that is quadratic in the depth of your tree to build up appropriate Applicative dictionaries. With some work it should be possible to share the dictionaries across recursive calls to drop the cost to linear in the depth; but since the computation itself is already exponential in the depth, perhaps an extra quadratic cost is small enough already.

What's going on with withApplicative?

Okay, we've got a Vector n t in our hands. Now, we carefully set up Vector so that it only accepts Nat-kinded values of n, and we smart programmers know that a Nat is some longish sequence of applications of Ns to a final Z. But the compiler doesn't know that*, it just knows that it has some type n of kind Nat. Consequently, since it doesn't know it's a bunch of Ns applied to Z, it doesn't know how to build up an Applicative instance -- since all the Applicative instances for Vector demand that the Nat argument to Vector be visibly either a Z or an N _. The type variable n is neither of these. This is the problem we are setting out to solve.

Or, you can take this alternative description of the problem: even if we tell the compiler that we have an Applicative instance for Vector n, as soon as we discover that n ~ N n' (say, by pattern-matching on the Vector and seeing that it's got a V constructor at its head), we are back to square one on the recursive call, because we haven't told the compiler that we have an Applicative instance for Vector n'. So an alternative way of thinking of the solution is that we'd like to have some way of saying that if we've got an Applicative instance for Vector n, we must have had an Applicative instance for all the predecessors of n (all the "smaller" Nats).

But wait! We have a trick up our sleeves. We've stored away some information in our Vector that, through pattern matching, lets us figure out exactly what Nat that n variable is! Namely: S _ vectors have got n ~ Z, and V _ _ vectors have got n ~ N n' (then we must recurse to figure out what n' is). So if we were somehow able to pattern match all the way down to an S, we would have simultaneously caused the type-checker to know the value of n all the way down to a Z. Then it could work its way back up, constructing Applicative instances for Z and then N Z and then N (N Z) and so on all the way back up to the value it now knows for n.

So this is the plan: if we need an Applicative instance to compute a thing, pattern match on applications of V all the way down to an S to learn how many applications of N there are to a Z; then use this knowledge to build the instance.

That's the intuition. Let's get to the mechanics.

withApplicative :: Vector n t -> (Applicative (Vector n) => a) -> a

This type signature says: suppose you need an Applicative instance to compute a thing -- specifically, an a thing. That is, suppose you've got a computation of type Applicative (Vector n) => a. If you also have a Vector n t, I can pattern match on that Vector to learn the value of n and build you the Applicative instance, so I can give you back an a thing that has already used the Applicative instance and doesn't need it any more. Compare this type:

withFoo :: Foo -> (Foo -> a) -> a

"If you have a thing that depends on a Foo, and a Foo, I can give you the corresponding thing." And this type:

withComputedFoo :: Bar -> (Foo -> a) -> a

"If you have a thing that depends on a Foo, I can cook up a Foo to hand it even if you give me a Bar instead." (For example, withComputedFoo might contain within it a function of type Bar -> Foo which it applies to the Bar you give it.) And now revisiting our type:

withApplicative :: Vector n t -> (Applicative (Vector n) => a) -> a

"If you have a thing that depends on an Applicative (Vector n) dictionary, if you hand me a Vector n t I'll cook up the dictionary for you and give you the corresponding thing."

Alright, but how does it work?

withApplicative S{} a = a

If you handed me a vector whose constructor is S, then I know that n was Z. So now I've learned that whereas before I had a :: Applicative (Vector n) => a, now I have a :: Applicative (Vector Z) => a. Since there's an Applicative (Vector Z) instance in the global scope, I can just use that, so I can also give this the type a :: a. Done with this case!

withApplicative (V v _) a = withApplicative v a

If you handed me a vector whose constructor is V instead, then I know that n was actually N n' for some n' (and crucially, v :: Vector n' t). So now whereas before I had a :: Applicative (Vector n) => a, now I have a :: Applicative (Vector (N n')) => a. Ah! But we have an instance Applicative (Vector n) => Applicative Vector (N n) in the global scope, so this constraint can be simplified a little bit to just a :: Applicative (Vector n') => a. Since we have a vector of length n' lying around -- namely, v -- now we can recurse, although notice that the Nat-kinded type in the recursive call has changed! Now we are calling withApplicative with v :: Vector n' t and a :: Applicative (Vector n') => a, that is, with n's predecessor, n'.

And that's all she wrote! The recursion takes care of building the dictionary for the predecessor, and we use the globally-available instance for building the slightly larger dictionary for n, and we're on our way.

* The compiler doesn't know it because it isn't, in fact, true. We're lying to ourselves. But it's close enough to true to be a useful mental model.

Answer to a previous version of the question follows.

Your dummy compiles just fine for me if I just leave off the Applicative constraint:

dummy :: Vector n Int -> Vector n Int -> Int
dummy (S a) (S b)       = a + b
dummy (V a a') (V b b') = let c  = dummy a b
                              c' = dummy a' b'
                          in c + c'

(Perhaps you need to make your motivating example a little bit more complicated to really capture what's hard about your problem...?)

Answer 2

I'm going to rename your constructors for the sake of my sanity.

data Nat = Z | S Nat

data Vector n a where
  Leaf :: a -> Vector 'Z a
  Branch :: Vector n a -> Vector n a -> Vector ('S n) a

The trouble is in the recursive case. Knowing Applicative ('S n) does not give you Applicative n; you can use only superclass constraints, not instance constraints, for this. The reason is that an instance constraint just says how to construct a dictionary; it doesn't say anything about what's in it.

I suspect that what you probably want is a very common folklore mechanism using a "singleton" type.

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

class KnownNat n where
  known :: SNat n

instance Known 'Z where
  known = SZ

instance Known n => Known ('S n) where
  known = SS known

Now you can write functions that work with SNats, and ones that work implicitly with KnownNat.

dummy :: KnownNat n => Vector n Int -> Vector n Int -> Int
dummy = dummy' known

dummy' :: SNat n -> Vector n Int -> Vector n Int -> Int

Note: if you look at my answer to your previous question, you'll see that only the pure method of Applicative is size-dependent. So if you don't need pure, you can probably yank the constraint altogether.