How to make fixed-length vectors instance of Applicative?

Question

I recently learned about promotion and decided to try writing vectors.

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}
module Vector where
  data Nat = Next Nat | Zero
  data Vector :: Nat -> * -> * where
    Construct :: t -> Vector n t -> Vector ('Next n) t
    Empty :: Vector 'Zero t
  instance Functor (Vector n) where
    fmap f a =
      case a of
        Construct x b -> Construct (f x) (fmap f b)
        Empty -> Empty

So far, everything is working. But I ran into a problem when trying to make Vector instance of Applicative.

instance Applicative (Vector n) where
  a <*> b =
    case a of
      Construct f c ->
        case b of
          Construct x d -> Construct (f x) (c <*> d)
      Empty -> Empty
  pure x = _

I had no idea how to do pure. I tried this:

case n of
  Next _ -> Construct x (pure x)
  Zero -> Empty

but got Variable not in scope: n :: Nat error for the first line and Couldn't match type n with 'Zero for the third line of this expression.

So, I used the following hack.

class Applicative' n where
  ap' :: Vector n (t -> u) -> Vector n t -> Vector n u
  pure' :: t -> Vector n t
instance Applicative' n => Applicative' ('Next n) where
  ap' (Construct f a) (Construct x b) = Construct (f x) (ap' a b)
  pure' x = Construct x (pure' x)
instance Applicative' 'Zero where
  ap' Empty Empty = Empty
  pure' _ = Empty
instance Applicative' n => Applicative (Vector n) where
  (<*>) = ap'
  pure = pure'

It gets the job done, but it's not pretty. It introduces a useless class Applicative'. And every time I want to use Applicative for Vector in any function, I have to supply the additional useless constraint Applicative' n which actually holds for any n.

What would be a better, cleaner way of doing this?

Answer 1

You could make same directly:

instance Applicative (Vector Zero) where
  a <*> b = Empty
  pure x = Empty

instance Applicative (Vector n) => Applicative (Vector (Next n)) where
  a <*> b = 
    case a of
      Construct f c ->
        case b of
          Construct x d -> Construct (f x) (c <*> d)
  pure x = Construct x (pure x)

As I can reason about it: for different types of the class, the code should be type-aware. If you had several instances, different types would get different implementation, and it would be easily resolved. But, if you try to make it with single non-recursive instance, there is basically no information about the type in runtime, and code which is always the same still needs to decide which type to handle. When you have input parameters, you can exploit GADTs to provide you the type information. But for pure there are no input parameters. So you have to have some context for the Applicative instance.