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

我正在編寫一個用於大地測量計算的庫。我想包括的一件事是用於網格投影的類型（例如Ordnance Survey National Grid）和這些網格上的點（由「eastings」和「northings」指定）。一個網格由一個原點指定，該原點將其連接到地球和一堆幾何參數。應用程序員可以使用這些參數創建許多任意網格。根據不同的基礎預測，也會有一系列類型的網格。如何使用類型來分隔不兼容的值

很顯然，我希望能夠對網格點（例如距離，軸承等）進行計算，但同時我想使用Haskell類型系統來防止應用程序員請求兩個之間的距離點在不同的網格上。我想知道是否使用沿着ST monad行的類型參數的Reader Monad可以工作，但我希望應用程序員能夠將這些位置值存儲在monad之外，而ST則是關於防止STRefs從runST。

我在底層橢球上也發現了一個類似的大地測量位置（緯度&經度）的問題。但是網格版本可能更容易解釋，因爲這個問題的焦點是類型系統而不是大地測量。

我讀過GADT和存在類型，但我看不出如何做到這一點。

來源

2012-10-29 Paul Johnson

可能是一種使用類型算術完成此操作的方法：http://www.haskell.org/haskellwiki/Type_arithmetic – Wes

「但同時我想使用Haskell類型系統來阻止應用程序員請求不同網格上兩點之間的距離「 - 爲什麼？點可以在不同的網格上定義，並且仍然代表相同的_physical_位置，爲什麼你不想計算這些點之間的距離？ – leftaroundabout

@leftaroundabout：是的，但這需要座標變換和更復雜的計算。在某些情況下，簡單的平面計算也是正確的（例如，在處理雷達時）。 –

您可以使用兩種GHC擴展，允許您標記與他們來自網格座標：（該擴展在GHC工作7.4+，不知道什麼更低）

{-# LANGUAGE DataKinds, KindSignatures #-} 

data CoordinateType = Geodetic | OSNG -- etc. 

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

zeroZero :: Coordinate Geodetic 
zeroZero = Coord 0 0

然後，要求它的任何功能都可以執行grid幻象參數的等式：

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

現在distance zeroZero (Coord 1 2 :: Coordinate OSNG)給出了一個類型的錯誤。

來源

2012-10-29 11:36:49 huon

如果我正確理解這一點，它只適用於CoordinateType值的硬編碼列表（實際上，我已經使用類型類完成了這些操作，儘管比較詳細）。我想說一些類似於「data CoordType = Grid Double Double」的內容，以便「foo = Grid 3 4; bar = Grid 2 4.2」可以在類型級別將「foo」中的座標與「bar」中的座標區分開來。 –

@PaulJohnson，你不限於硬編碼的值列表，因爲（現在需要GHC 7。6）你可以在字體級別使用字符串和自然數（「提升的文字」）。關於數據 - >善意促銷的文檔是[here]（http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/promotion.html），你可以看看是否有幫助。 – huon

但它們也必須是文字：我無法（據我所知）從文件中讀取字符串並將其提升爲類型。 –

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

回答

相關問題