如何使用类型分隔不兼容的值

Question

我正在为大地测量计算编写一个库.我想要包括的一件事是网格投影的类型(例如军械测量国家网格)和那些网格上的点(由"东方"和"北方"指定).网格由原点指定,该原点将其与地球和一堆几何参数联系起来.应用程序员可以使用这些参数创建许多任意网格.基于不同的基础预测,还将有一系列类型的网格.

显然我希望能够对网格点进行计算(例如距离,方位等),但同时我想使用Haskell类型系统来阻止应用程序员询问不同网格上两点之间的距离.我想知道使用ST monad行的类型参数的Reader Monad是否可以工作,但我希望应用程序员能够将这些位置值存储在monad之外,而ST则是为了防止STRef泄漏runST.

我对底层椭球的大地位置(纬度和经度)也有类似的问题.但是网格版本可能更容易解释,因为这个问题的焦点是类型系统而不是大地测量.

我已经阅读了GADT和存在类型,但我看不出怎么做.

Answer 1

您可以使用两个 GHC 扩展来允许您使用它们来自的网格来标记坐标：

{-# LANGUAGE DataKinds, KindSignatures #-}

data CoordinateType = Geodetic | OSNG -- etc.

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

zeroZero :: Coordinate Geodetic
zeroZero = Coord 0 0

（扩展在 GHC 7.4+ 中工作，不确定是否有更低版本。）

然后，任何需要它的函数都可以强制幻像参数相等grid：

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

现在distance zeroZero (Coord 1 2 :: Coordinate OSNG)给出类型错误。