Rafael Almeida | 20 Jul 00:44 2014
Picon

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

    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? 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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Niklas Haas | 20 Jul 01:05 2014
Picon

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 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.
Frank Staals | 20 Jul 20:00 2014
Picon

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
[2] http://hackage.haskell.org/package/vinyl
[3] http://hackage.haskell.org/package/fixed-vector

--

-- 

- Frank
Francesco Ariis | 20 Jul 01:17 2014
Picon

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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane