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

On Sat, Jul 19, 2014 at 07:44:46PM -0300, Rafael Almeida wrote:

I was talking to friends about how could you make a Point type in haskell. It's intuitive to make a 2D point such as:

type Point2D = (Double, Double)

Using a list would be more general:

type Point = [Double]

now we have a nice, general add function

add = zipWith (+)

It's not so fun that we are able to do something like:

add [2,3] [5,7,11]

We have no type-safety that we can only operate on points with the same dimension.

How could we address this? Can we make a general function, yet retain the type safety?

A possible solution /without/ using Template Haskell is using phantom types for the various kind of |Point|s. Example: data Point a = Point [Int] deriving (Show) data Two -- data declaration sans constructors data Three crea2d :: Int -> Int -> Point Two crea2d a b = Point [a,b] crea3d :: Int -> Int -> Int -> Point Three crea3d a b c = Point [a,b,c] addPoints :: Point a -> Point a -> Point a addPoints (Point pa) (Point pb) = Point $ zipWith (+) pa pb So you are sure addPoints is will only type-check on two similarly constructed (i.e. same dimensions) |Point|s: ex2 = crea2d 1 2 -- make sure that "exSomething" is the only way to ex3 = crea3d 1 2 3 -- create Points (i.e. don't export Point(..)) works = addPoints ex2 ex2 stillworks = addPoints ex3 ex3 doesntwork = addPoints ex2 ex3 -- won't type-check Phantom types are a well known trick for "shifting" checks from run-time to compile-time.