What is called "partial order" is in fact merely a preorder.

[kindaro]

I have a problem with this.

According to some notes, that seem to me correct in this point, a partial order is a preorder that is antisymmetric. What I claim is that it's undecidable whether a preorder relation on an arbitrary datatype is antisymmetric. (Kindly do point out if I am wrong.)

In other words:

quickCheck $ \x y -> (x `leq` y && y `leq` x) && (x == y)

— May fail.

Consider the following example:

module Soup where

import Algebra.PartialOrd
import Test.QuickCheck

data Soup = Juice Bool | Topping | Android deriving (Show, Eq)

instance PartialOrd Soup where
    leq (Juice x) (Juice y) = x <= y
    leq (Juice _) _ = False
    leq _ (Juice _) = False
    leq _ _ = True

instance Arbitrary Soup where
    arbitrary = oneof [Juice <$> arbitrary, return Topping, return Android]

This leq :: Soup -> Soup -> Bool relation on a set of as many as four elements I believe to be reflexive and transitive. Can you see where it fails to be antisymmetric?

What I am suspicious about is that:

• The naming is misleading in that there are in fact less guarantees than implied.
• Do these functions even work as expected?

Example, again:

λ partialOrdEq Topping Android 
True

(I thought partial orders were antisymmetric!)

Another example:

cycleMonotone Topping = Android
cycleMonotone Android = Topping

λ lfpFrom Topping cycleMonotone  -- At least it runs in constant space!

(I thought lfpFrom was safe!)

[phadej]

-- | A partial ordering on sets
-- (<http://en.wikipedia.org/wiki/Partially_ordered_set>) is a set equipped
-- with a binary relation, `leq`, that obeys the following laws
--
-- @
-- Reflexive:     a ``leq`` a
-- Antisymmetric: a ``leq`` b && b ``leq`` a ==> a == b
-- Transitive:    a ``leq`` b && b ``leq`` c ==> a ``leq`` c
-- @

Your PartialOrd Soup instance is unlawful, you violate the assumptions, something breaks because of that.

[kindaro]

What I meant is that this interface may be split to the part that describes a preorder, and the part that makes an assumption that it is also antisymmetric and operates on this assumed partial order. The preorder part would then be more widely useful per se.

[phadej]

I see. Do you have good examples or preorders which aren't partial?

https://en.wikipedia.org/wiki/Preorder mentions subtyping relation, but I wonder what the type-system would look like where subsuming relation isn't antisymmetric. One example is record permutation as in http://www.cs.cornell.edu/courses/cs6110/2013sp/lectures/lec28-sp13.pdf. EDIT: from my POV I'd rather design a type-system where subsuming relation is partiial order, it's good property to have.

Another question: does Preorder has interesting general applications. For PartialOrd we have e.g. partialOrdEq etc. But can we have interesting Preorder a => ... functions? Or would it be only for the sake of ad-hoc polymorphism to use the same name?

[phadej]

TL;DR I can be convinced Preorder is useful, but I'm not yet.

[kindaro]

One thing I like about preorders is that there may be three different kinds of relation between any two objects, that a suitable combination of leq would reveal:

1. Equivalent.
2. Related: either Less or Greater.
3. Unrelated.

This is what both partialOrdEq and comparable may be generalized to.

Then, one may throw away some of these options and call it a subclass:

• For an equivalence relation, you keep the first and the last one.
• For a total order, you keep the second.
• For a poset, you keep the last two.

I don't have an immediate example of a type that is a useful preorder. The PreOrd class is not in standard libraries, so the idea must not be crossing people's minds that often.

First, let us call something a proper preorder when it is a preorder but not a poset, by analogy with the notion of a "proper subset".

• There is one way to construct a proper preorder that I'm certain about. Such a type would be a sum where on the left there is a poset, and on the right a set with non-trivial equivalence. I'd say both are a rarity. This is how I obtained Soup.

• I'm not sure about this one, but if it's true, it makes many things a proper preorder. Take a functor that happens not to be faithful. If the range is a poset, there is an induced preorder in the domain.

  For example, lists under forall x. x `elem` xs => x `elem` ys relation do not form a poset, because [1,2,3] is equivalent to [1,3,2] and any other permutation of these numbers. There is still clearly some notion of order, as [1,2] is in some sense "strictly less" than any permutation of [1,2,3], while unrelated to [5,6,7] or any other zs. length zs == 3. If I am correct, then this would be a preorder induced on a free monoid by a forgetful functor to Set.

[phadej]

forall x. `elem` xs => x `elem` ys is a partial order, it's isSubsetOf if you see lists as sets (there [1,1] and [1] are equivalent. You may do something with multiplicities of elements, but then you get partial order for Map k v).

[kindaro]

Of course it is a partial order on Data.Set, as you describe. And it is made possible by the forgetful functor embodied in Set.fromList. But it's not a partial order on lists. As long as you remember the specific ordering of elements, I believe Data.List to be a preorder under the relation I described.

[phadej]

I see, but we have already different partial order on lists: isInfixOf. We cannot have that to be an instance for [a]. So I have to make a newtype, why wouldn't I make it's equality based on equivalence class?

I really want to be convinced there is practical benefit, not only theoretical correctness. (That's why I'm hesitant to add Heyting class too, as there wouldn't be much use for it).

[kindaro]

Maybe it's a chicken and egg problem. Haskell was also practically useless for the first decade of its existence. Anyway, I'm out of arguments.

[andreasabel]

@phadej wrote (ping @kindaro):

forall x. x `elem` xs => x `elem` ys is a partial order, it's isSubsetOf if you see lists as sets (there [1,1] and [1] are equivalent. You may do something with multiplicities of elements, but then you get partial order for Map k v).

You can alway quotient a preorder to get a partial order, that is what is going on in this argument.
However, quotienting maybe too computationally expensive, and you might want to abstain from it, sticking with a preorder.
Or, quotienting may be undesirable for other reasons.

ATTEMPT 1:
A typical examples would be typing contexts and renamings (of de Bruijn indices) between these. This is basically the example already discussed, but a proof-relevant version thereof. So x elem xs (where x is a type expression and xs a context, i.e., a list of type expressions) is witnessed by a de Bruijn index, the index of x in xs. A renaming is then a proof-relevant version of isSubsetOf, but you do not want to equate contexts that are just permutations of each other, since silently replacing contexts by "equal" ones would disturb all the de Bruijn indices.
So the preorder isSubsetOf would be "there exists a renaming".
But now that I think of it, one should model this as a category rather than a preorder if one wants to carry around the witnessing renamings. Unfortunately, the standard Haskell categories are a type-level structure only, we would also need a value-level structure (so that leq a b could deliver a set of witnesses).

ATTEMPT 2:
Take a badly engineered real-life programming languages like JavaScript and let a <= b be in the preorder if values of type a can be coerced to values of type b. You might have coercions Int <= Double <= Int but still do not want Int == Double.

Appropos practical benefit: I am not arguing for a direct application I am desperately needing here. But this is due to the fact that I have problems with the class PartialOrd in general (issue #117).