[Haskell-cafe] Creating a Point

[Frank Staals]

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