Implementing zipWith for type-safe vectors

Question

I am trying to write a vector library that has type-safe lengths, meaning adding two vectors of different lengths will not fly.

My current implementation is roughly:

data Natural where
  Zero :: Natural
  Succ :: Natural -> Natural

type One   = Succ Zero
type Two   = Succ One
type Three = Succ Two
type Four  = Succ Three

data Vector n e where
  Nil  :: Vector Zero e
  (:|) :: e -> Vector n e -> Vector (Succ n) e

infixr :|

I am now trying to implement zipWith because it will help with implementing things like dot product and the Num typeclass.

I have gotten this far

zipWith :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
zipWith f (a :| as) (b :| bs) = f a b :| zipWith f as bs
zipWith _ _ _ = Nil

but I receive the error

Couldn't match type `n' with 'Zero
      `n' is a rigid type variable bound by
          the type signature for
            zipWith :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
          at LinearAlgebra.hs:51:12
    Expected type: Vector n c
      Actual type: Vector 'Zero c
    In the expression: Nil
    In an equation for `zipWith': zipWith _ _ _ = Nil

I believe the reason is that the variable n can only take on one value - either Succ or Zero?

How can I remedy this?

Answer 1

Take the following pattern:

zipWith _ as bs = Nil

Here GHC only knows that the type of as is Vector n a and the type of bs is Vector n b, from the signature of the function. Also, the signature says that the right hand side must have type Vector n c, where n is the same as the other n-s in the left hand side. Nil has type Vector Zero x, for an arbitrary x.

The types don't match because the length parameter on the left hand side is an unknown arbitrary n, while the the right hand side has length Zero. Pattern matching on the arguments brings in the necessary additional information:

zipWith _ Nil Nil = Nil 
-- "zipWith _ as Nil" also works, because now "as" is constrained to also have Zero length

If you have GHC 7.8.x, you can write the following:

zipWith f as bs = _

and GHC will provide you highly useful messages about the expected type of the hole and the the types of the variables in scope (to GHC's best knowledge, given the constructors you've pattern matched on).