zellige / hs-geojson

GeoJSON parsing library [Haskell]
BSD 3-Clause "New" or "Revised" License
23 stars 13 forks source link

`instance Traversable LinearRing` violates the Traversable laws #21

Open tysonzero opened 5 years ago

tysonzero commented 5 years ago

Specifically the composition law:

traverse (Compose . fmap g . f) = Compose . fmap (traverse g) . traverse f
traverse (Compose . fmap g . f) x = Compose . fmap (traverse g) . traverse f $ x
f = enumFromTo 1
g = mfilter (> 1) . Just
x = LinearRing 2 2 2 (fromList [])
traverse (Compose . fmap g . f) x
Compose [Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Just (LinearRing 2 2 2 (fromList []))]
Compose . fmap (traverse g) . traverse f $ x
Compose [Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Nothing,Just (LinearRing 2 2 2 (fromList [])),Just (LinearRing 2 2 2 (fromList []))]
newmana commented 5 years ago

This is interesting because I guess it's because the traversable instance tries to close the LinearRing. I imagine the Foldable instance will have a similar issue.

tysonzero commented 5 years ago

The Foldable instance is technically lawful, because Foldable has no laws (besides free theorem laws that will obviously hold).

Now if you did fix the Traversable instance to avoid the "closing" (you are correct that is the reason), then a different Traversable law would be broken, the one that requires Traversable and Foldable to agree.

So if you do want to have a lawful Traversable instance then yeah the Foldable instance would have to be changed as well.

I would say its reasonable to drop the "closing" part, as its (IMO) perfectly reasonable for (0, 0) (0, 1) (1, 0) to represent a triangle. Although if you do I would suggest dropping it in most places, such as fromList.

Although I realize it has become pretty standard to represent rings with a duplicated point at the end rather than using the more Haskell-like approach of using the type/constructor to indicate whether you have a LineString or a LinearRing.