Implementing zipWith for type-safe vectors
haskell, linear-algebra, types
Solution
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).
Problem
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?