[Haskell-cafe] Creating a Point
Niklas Haas
haskell at nand.wakku.to
Sat Jul 19 23:05:32 UTC 2014
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.
More information about the Haskell-Cafe
mailing list