Ord for partially ordered sets

[Andreas Abel]

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 at gu.se
http://www2.tcs.ifi.lmu.de/~abel/