On Sat, 19 Jul 2014 19:44:46 -0300, Rafael Almeida
How could we address this? Can we make a general function, yet retain the type safety? I suppose maybe there's something that could be done with TH so that we automatically generate those Point2D, Point3D, etc code. I'm not sure that would be a nice path to follow, though.
This can be achieved with only the help of GADTs: data Zero data Succ dim data Vector dim a where VEmpty :: Vector Zero a VCons :: a -> Vector d a -> Vector (Succ d) a add :: Num a => Vector d a -> Vector d a -> Vector d a add VEmpty VEmpty = VEmpty add (VCons a x) (VCons b y) = VCons (a+b) (add x y) If we allow for the use of DataKinds as well, we can get some additional niceties by defining our Zero/Succ like this instead: data Dim = Zero | Succ Dim In this representation, we can also add a typeclass to define something like: class Dimension (d :: Dim) where inj :: a -> Vector d a dim :: Vector d a -> Dim instance Dimension Zero where inj _ = VEmpty dim _ = Zero instance Dimension d => Dimension (Succ d) where inj a = VCons a (inj a) dim (VCons _ v) = Succ (dim v) This allows us to write, among other things: fromInteger :: (Num a, Inj d) => Integer -> Vector d a fromInteger = inj . fromInteger Ultimately leading to: instance (Dimension d, Num a) => Num (Vector d a) where ... Figuring out the details of this is left as an exercise to the reader.