Example of has

Points.hs

import Data.Has
import Control.Applicative

data X = X; data Y = Y; data Z = Z

newtype Point2D = P2 (X :> Int :&: Y :> Int)
    deriving (Has (X `Labelled` Int),Has (Y `Labelled` Int))

getXY :: (Knows X Int p, Knows Y Int p) => p -> (Int,Int)
getXY = liftA2 (,) (prjl X) (prjl Y)

instance Show Point2D where
    show = show . getXY

-- Calculating distance can be polymorphic
-- dist2d :: (Knows X Int p, Knows Y Int p) => p -> p -> Double
dist2d p1 p2 = let (x1,y1) = getXY p1; (x2,y2) = getXY p2
               in sqrt . fromIntegral $ ((x2-x1)^2) + ((y2-y1)^2)

p2 :: Int -> Int -> Point2D
p2 x y = P2 (X .> x & Y .> y)

p = p2 1 3
q = p2 4 5
r = p2 8 (-2)

d0 = dist2d p q
d1 = dist2d p r

newtype Point3D = P3 (Z :> Int :&: Point2D)
    deriving (Has (X `Labelled` Int)
             ,Has (Y `Labelled` Int)
             ,Has (Z `Labelled` Int))

-- instance Show Point3D where
--     show p = let (X x,Y y,Z z) = getXYZ p
--              in show (x,y,z)

getXYZ :: (Knows X Int p, Knows Y Int p, Knows Z Int p) => p -> (Int,Int,Int)
getXYZ = liftA3 (,,) (prjl X) (prjl Y) (prjl Z)

p3 :: Int -> Int -> Int -> Point3D
p3 x y z = P3 (Z .> z & p2 x y)

dist3d p1 p2 = let (x1,y1,z1) = getXYZ p1; (x2,y2,z2) = getXYZ p2
               in sqrt . fromIntegral $ ((x2-x1)^2) + ((y2-y1)^2) + ((z2-z1)^2)

p' = p3 1 1 0
q' = p3 3 4 2
r' = p3 6 (-1) 2

d3 = dist3d p' q'
d4 = dist3d p' r'

-- dist2d still can be applied to Point3D
d3' = dist2d p' q'
d4' = dist2d p' r'

removeZ :: (Knows Z Int p) => p -> p
removeZ p = injl Z 0 p

t1 = dist2d p' q' == dist3d (removeZ p') (removeZ q')
t2 = dist2d p' r' == dist3d (removeZ p') (removeZ r')