Open kindaro opened 6 years ago
-- | 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.
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.
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?
TL;DR I can be convinced Preorder
is useful, but I'm not yet.
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:
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:
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.
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
).
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.
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).
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.
@phadej wrote (ping @kindaro):
forall x. x `elem` xs => x `elem` ys
is a partial order, it'sisSubsetOf
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 forMap 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).
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:
— May fail.
Consider the following example:
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:
Example, again:
(I thought partial orders were antisymmetric!)
Another example:
(I thought
lfpFrom
was safe!)