Jak używać typów do rozdzielania niezgodnych wartości

Question

Piszę bibliotekę do obliczeń geodezyjnych. Jedną rzeczą, którą chcę uwzględnić, jest typ do rzutowania siatki (na przykład Krajowa siatka badania Ordnance Survey) i punkty na tych siatkach (określone przez "wschody" i "północy"). Siatka jest określona przez punkt początkowy, który wiąże ją z Ziemią i wiązkę parametrów geometrycznych. Programista aplikacji może tworzyć wiele arbitralnych sieci przy użyciu tych parametrów. Pojawi się także szereg rodzajów sieci bazujących na różnych projekcjach podstawowych.

Oczywiście chcę mieć możliwość wykonywania obliczeń na punktach siatki (np. Odległość, łożysko itp.), , ale jednocześnie chcę użyć systemu typu Haskell, aby uniemożliwić programistom żądanie odległości między dwoma punkty na różnych siatkach. Zastanawiałem się, czy Monada Reader używająca parametru typu wzdłuż linii monady ST będzie działała, ale chcę, żeby programista mógł przechowywać te wartości pozycji poza monadą, podczas gdy ST chodzi o zapobieganie przeciekom z STRefs. runST.

Mam również podobny problem z położeniami geodezyjnymi (szerokość geograficzna & długości geograficznej) na leżących poniżej elipsoidach. Ale wersja siatkowa jest prawdopodobnie łatwiejsza do wytłumaczenia, zważywszy, że głównym tematem tego pytania jest system typu, a nie geodetyka.

Czytałem o GADT i typach egzystencjalnych, ale nie widzę, jak to zrobić.

Answer 1

Można użyć dwóch rozszerzeń GHC, co pozwala oznaczyć koordynuje z siatki, z którego pochodzą: (. Rozszerzenia pracować w GHC 7.4+, nie wiedząc o niczym niższym)

{-# LANGUAGE DataKinds, KindSignatures #-} 

data CoordinateType = Geodetic | OSNG -- etc. 

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

zeroZero :: Coordinate Geodetic 
zeroZero = Coord 0 0 

następnie wszelkie funkcje wymagające go może wymusić równość parametru grid phantom:

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

teraz distance zeroZero (Coord 1 2 :: Coordinate OSNG) daje błąd typu.