20 Jul 00:44 2014

## Creating a Point

Hello,

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)

Let's define one operation on this new type:

add2D (x1, y1) (x2, y2) = (x1+x2, y1+y2)

Let's say now we want a 3D point. Then we'd be tempted to do:

type Point3D = (Double, Double, Double)

add3D (x1, y1, z1) (x2, y2, z2) = (x1+x2, y1+y2, z1+z2)

Although those types work great and you could make a type class so you don't have to suffix each function with 2D and 3D. It feels like we are just repeating code when defining the add function. If we want to go 4D, 5D, etc it would be more repeated code.

Using a list would be more general:

type Point = [Double]

now we have a nice, general add function

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

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? 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.

[]'s
Rafael
```_______________________________________________
```
20 Jul 01:05 2014

### Re: Creating a Point

```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 (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

instance (Dimension d, Num a) => Num (Vector d a) where
...

Figuring out the details of this is left as an exercise to the reader.
```
20 Jul 20:00 2014

### Re: Creating a Point

```Niklas Haas <haskell <at> nand.wakku.to> writes:

> 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:
>
> <snip>

Small self-plug: I recently started working on a geometry library[1]
based on vinyl[2], fixed-vector[3], and GHC's type-level naturals. It
uses the ideas like the one sketched by Niklas. It is nowhere near finished
(or even usable), and requires pretty much every type-related GHC
extension under the sun. But it does allow you to write cool things
like:

x    = SNatField :: SDField 1
y    = SNatField :: SDField 2

name = SSymField :: SSField "name" String

myPoint :: Point 2 '["name" :~> String] Int
myPoint = point \$ x =: 1
<+>
name =: "myPoint"
<+>
y =: 100

p :: Point 100 '[] Double
p = origin

myVector1 :: Vector (ToNat1 3) Int
myVector1 = Vector \$ V.mk3 1 2 3

-- myPoint1 :: Point 3 '[] Int
myPoint1 = fromVector myVector1

If anyone is interested in this let me know :).

Regards,

[1] https://github.com/noinia/hgeometry

--

--

- Frank
```
20 Jul 01:17 2014

### Re: Creating a Point

```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
>
>
> It's not so fun that we are able to do something like:
>
>
> 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(..))

```_______________________________________________