On 04/24/2015 03:06 PM, Ivan Lazar Miljenovic wrote:
What is the validity of defining an Ord instance for types for which
mathematically the `compare` function is partially ordered?
I'd say this is harmful, as functions like min and max (and others) rely on the totality of the ordering.
Partial orderings are useful in itself, I implemented my own library
https://hackage.haskell.org/package/Agda-2.4.2/docs/Agda-Utils-PartialOrd.html
mainly to use it for maintaining sets of incomparable elements:
https://hackage.haskell.org/package/Agda-2.4.2/docs/Agda-Utils-Favorites.html
Specifically, I have a pull request for fgl [1] to add Ord instances
for the graph types (based upon the Ord instances for Data.Map and
Data.IntMap, which I believe are themselves partially ordered), and
I'm torn as to the soundness of adding these instances. It might be
useful in Haskell code (the example given is to use graphs as keys in
a Map) but mathematically-speaking it is not possible to compare two
arbitrary graphs.
What are people's thoughts on this? What's more important: potential
usefulness/practicality or mathematical correctness?
(Of course, the correct answer is to have a function of type a -> a ->
Maybe Ordering :p)
[1]: https://github.com/haskell/fgl/pull/11
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
andreas.abel@gu.se
http://www2.tcs.ifi.lmu.de/~abel/
_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries