[Haskell-cafe] Creating a Point

[Niklas Haas]

On Sat, 19 Jul 2014 19:44:46 -0300, Rafael Almeida <almeidaraf at gmail.com> wrote:
> 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.