How do you design similar types to enforce particular rules?

Suppose you have a naive vector type, such as

data Vector a
  = V2 a a
  | V3 a a a

I am interested in how you can — and how you should — implement particular logic specific to the type's constructor. What I mean can be clarified with an example.

Suppose I want to implement:

instance Num a => Num (Vector a) where
  (+) = 
  (*) = _
  abs = _
  signum = _
  fromInteger = _
  negate = _

Due to pattern matching, I can very easily match V2 with V2. However, what if I want it to be invalid for a particular combination, such as between V2 and V3?

In this case, is it required to make individual types for V2and V3? Then, however, do I not lose the polymorphic properties they currently have, being the same type? For example, if I begin building operations consuming my Vector, I currently need only one function. However, if I split into two types, I need two distinct functions.

How can I solve this problem by thinking in types?

Solution

So you want your ADT cases to look like distinct types sometimes, so they can't be accidentally mixed, yet other times you want to be able to treat them homogeneously? That's what GADTs are for (among other things).

Give your type a phantom type parameter, and force it to be different for the different constructors. When you don't care, you can just make that type parameter generic:

data Len2
data Len3

data Vector len a where
  V2 :: a -> a -> Vector Len2 a
  V3 :: a -> a -> a -> Vector Len3 a

vectorAdd :: Num a => Vector len a -> Vector len a -> Vector len a
vectorAdd (V2 x1 y1) (V2 x2 y2) = V2 (x1+x2) (y1+y2)
vectorAdd (V3 x1 y1 z1) (V3 x2 y2 z2) = V3 (x1+x2) (y1+y2) (z1+z2)

vectorFst :: Vector len a -> a
vectorFst (V2 x _) = x
vectorFst (V3 x _ _) = x

In vectorAdd the compiler recognizes that V2 and V3 can never be matched because they always have different len parameters, yet you still can write vectorFst that works for any len.

Next level - don't create special-purpose Len2 and Len3 types, use numeric type-level literals, which GHC supports:

data Vector len a where
  V2 :: a -> a -> Vector 2 a
  V3 :: a -> a -> a -> Vector 3 a