How do I use types to separate incompatible values

Question

I'm writing a library for geodetic calculations. One thing I want to include is a type for grid projections (e.g. Ordnance Survey National Grid) and points on those grids (specified by "eastings" and "northings"). A grid is specified by an origin point that ties it to the Earth and a bunch of geometrical parameters. The application programmer can create many arbitrary grids using these parameters. There are also going to be a range of types of grids based on different underlying projections.

Obviously I want to be able to do calculations on grid points (e.g. distance, bearing etc), but at the same time I want to use the Haskell type system to prevent an application programmer from asking for the distance between two points on different grids. I wondered if a Reader Monad using a type parameter along the lines of the ST monad would work, but I want the application programmer to be able to store these position values outside of the monad, whereas ST is all about preventing the leakage of STRefs from the runST.

I've also got a similar problem with geodetic positions (latitude & longitude) on the underlying ellipsoids. But the grid version is probably easier to explain, given that the focus of this question is the type system rather than geodetics.

I've read up on GADTs and existential types, but I can't see how to do this.

Answer 1

You can use two GHC extensions to allow you to mark coordinates with the grid they come from:

{-# LANGUAGE DataKinds, KindSignatures #-}

data CoordinateType = Geodetic | OSNG -- etc.

data Coordinate (grid :: CoordinateType) = Coord Int Int

zeroZero :: Coordinate Geodetic
zeroZero = Coord 0 0

(The extensions work in GHC 7.4+, not sure about anything lower.)

Then, any functions requiring it can enforce equality of the grid phantom parameter:

distance :: Coordinate grid -> Coordinate grid -> Float
distance p q = undefined

Now distance zeroZero (Coord 1 2 :: Coordinate OSNG) gives a type error.