Pattern matching on length using this GADT:

Question

I've defined the following GADT:

data Vector v where
    Zero    :: Num a => Vector a
    Scalar  :: Num a => a -> Vector a
    Vector  :: Num a => [a] -> Vector [a]
    TVector :: Num a => [a] -> Vector [a]

If it's not obvious, I'm trying to implement a simple vector space. All vector spaces need vector addition, so I want to implement this by making Vector and instance of Num. In a vector space, it doesn't make sense to add vectors of different lengths, and this is something I would like to enforce. One way I thought to do it would be using guards:

instance Num (Vector v) where
    (Vector a) + (Vector b) | length a == length b =  
                                Vector $ zipWith (+) a b
                            | otherwise = 
                                error "Only add vectors with the same length."

There is nothing really wrong with this approach, but I feel like there has to be a way to do this with pattern matching. Perhaps one way to do it would be to define a new data type VectorLength, which would look something like this:

data Length l where
    AnyLength   :: Nat a => Length a
    FixedLength :: Nat a -> Length a

Then, a length component could be added to the Vector data type, something like this:

data Vector (Length l) v where
    Zero :: Num a => Vector AnyLength a
    -- ...
    Vector :: Num a => [a] -> Vector (length [a]) [a]

I know this isn't correct syntax, but this is the general idea I'm playing with. Finally, you could define addition to be

instance Num (Vector v) where
    (Vector l a) + (Vector l b) = Vector $ zipWith (+) a b

Is such a thing possible, or is there any other way to use pattern matching for this purpose?

Answer 1

What you're looking for is something (in this instance confusingly) named a Vector as well. Generally, these are used in dependently typed languages where you'd write something like

data Vec (n :: Natural) a where
  Nil  :: Vec 0 a
  Cons :: a -> Vec n a -> Vec (n + 1) a

But that's far from valid Haskell (or really any language). Some very recent extensions to GHC are beginning to enable this kind of expression but they're not there yet.

You might be interested in fixed-vector which does a best approximation of a fixed Vector available in relatively stable GHC. It uses a number of tricks between type families and continuations to create classes of fixed-size vectors.

Answer 2

Just to add to the example in the other answer - this nearly works already in GHC 7.6:

{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeOperators #-}

import GHC.TypeLits

data Vector (n :: Nat) a where
    Nil  :: Vector 0 a
    Cons :: a -> Vector n a -> Vector (n + 1) a

That code compiles fine, it just doesn't work quite the way you'd hope. Let's check it out in ghci:

*Main> :t Nil
Nil :: Vector 0 a

Good so far...

*Main> :t Cons "foo" Nil
Cons "foo" Nil :: Vector (0 + 1) [Char]

Well, that's a little odd... Why does it say (0 + 1) instead of 1?

*Main> :t Cons "foo" Nil :: Vector 1 String

<interactive>:1:1:
    Couldn't match type `0 + 1' with `1'
    Expected type: Vector 1 String
      Actual type: Vector (0 + 1) String
    In the return type of a call of `Cons'
    In the expression: Cons "foo" Nil :: Vector 1 String

Uh. Oops. That'd be why it says (0 + 1) instead of 1. It doesn't know that those are the same. This will be fixed (at least this case will) in GHC 7.8, which is due out... In a couple months, I think?