Re: [Haskell-cafe] Creating a Point

Niklas Haas writes:

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:

<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