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

Question

我正在编写一个用于大地测量计算的库。我想包括的一件事是网格投影的类型(例如军械测量国家网格)和这些网格上的点(由“eastings”和“northings”指定)。网格由将其连接到地球的原点和一系列几何参数指定。应用程序员可以使用这些参数创建许多任意网格。还将有一系列基于不同底层预测的网格类型。

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

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

我已经阅读了 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)给出类型错误。