What do Lattice/DistributedLattice offer?

[joneshf]

I was thinking about this the other day. Is anything really gained by either of these two type classes.

I'd posit that there isn't. From the Ord superclass, you can derive sup and inf:

sup x y = if x <= y then y else x
inf x y = if x <= y then x else y

I'm not sure if this is the only law abiding implementation though. But, these two definitions together satisfy all the laws of Lattice and DistributedLattice (also BoundedLattice, but you still need the Bounded superclass). The only thing to be gained is the opportunity to use a slightly more efficient implementation--or in the case of something like Boolean, a lazy version. Is that worth it?

Maybe it makes sense to drop Lattice and DistributedLattice, provide sup/inf in terms of the Ord constraint, keep BoundedLattice and ComplementedLattice, and move (||)/(&&) into BooleanAlgebra so you can still provide special implementations.

Maybe some other thing makes sense?

[hdgarrood]

Here's an application of lattices: http://www.cs.indiana.edu/~lkuper/papers/lvars-fhpc13.pdf. Perhaps, since the application is parallelism, they're not very helpful as long as the only non-experimental compilation target is JavaScript. However it does look like that will change soon :)

Anyway - I agree, I think something is a little off here.

Despite the names, we don't currently require that sup and inf actually give the supremum and infimum of the 2-element set they are applied to. For example, sup as bitwise or and inf as bitwise and would satisfy the laws, despite the fact that, for example, 0b10 .|. 0b01 is not the least upper bound of {0b10, 0b01}.

If we require that inf and sup are the real infimum and supremum respectively, and if the type does have a total ordering, I am pretty sure that you're right - the only possible Lattice instance would use your definitions of sup and inf. If, however, the type has a non-total ordering, then I think we would need the user to define their own Lattice instance.

An example from that paper had the set as the natural numbers augmented with a separate top and bottom, and the relation defined by:

bottom <= _ = true
_ <= top = true
_ <= _ = false

While I believe this relation does fully specify how sup and inf should behave, assuming that we do really mean supremum and infimum respectively, I don't think it's possible for their definitions to be derived given only an Ord instance.

I wonder if it's sensible to describe Ord as a partial ordering. 99% of the time I use Ord, I pretend it's a total ordering (I suspect I'm not the only one). I think 99% of the instances that exist are total orderings anyway.

If we really want a partial ordering type class, I think it's very unintuitive for EQ to mean "equal or incomparable", especially since x <= y is true in the case where x is incomparable to y, and especially especially since for any x, y, it is always true that x <= y || y <= x. I think compare :: a -> a -> Maybe Ordering would make a lot more sense - and if we were to go down that route, I think I'd rather leave Ord alone and make a new, separate type class for partial orderings.

[paf31]

I wonder if it's sensible to describe Ord as a partial ordering.

I always thought Ord did represent a partial ordering. That's why Eq is a superclass, so that you can distinguish actually-equal things from merely-incomparable things.

Even in the absence of parallelism, using lattices to represent partial information is a good enough use case IMO. You can also interpret boolean algebra in any lattice, which makes it useful for abstract interpretation.

[joneshf]

@hdgarrood most of that makes sense. So since Ord is a total ordering, the Lattice instance is unique, right?

An example from that paper had the set as the natural numbers augmented with a separate top and bottom, and the relation defined by:

bottom <= _ = true
_ <= top = true
_ <= _ = false

While I believe this relation does fully specify how sup and inf should behave, assuming that we do really mean supremum and infimum respectively, I don't think it's possible for their definitions to be derived given only an Ord instance.

If you mean the example from Figure 2(a), then shouldn't the last line read _ <= _ = true? At least that's what the explanation states in section 3.1.
If the line is as you wrote it, you couldn't have an Ord instance at all, as it would fail to hold for reflexivity. You also couldn't have an Eq instance for the same reason.
If it's as the paper explained, the Ord instance would have to be:

instance ordNat :: Ord Nat where
  compare _ _ = EQ

which would also imply this Eq instance:

instance eqNat :: Eq Nat where
  (==) _ _ = true

and thus the equations above for sup and inf should still hold as valid derivations.

You still don't see the actual supremum or infimum, so yeah something does seem a bit off, as you stated.

I wonder if it's sensible to describe Ord as a partial ordering.

I always thought Ord did represent a partial ordering. That's why Eq is a superclass, so that you can distinguish actually-equal things from merely-incomparable things.

I think Ord has to be a total ordering, at least the type says it is.

[joneshf]

If we really want a partial ordering type class, I think it's very unintuitive for EQ to mean "equal or incomparable", especially since x <= y is true in the case where x is incomparable to y, and especially especially since for any x, y, it is always true that x <= y || y <= x. I think compare :: a -> a -> Maybe Ordering would make a lot more sense - and if we were to go down that route, I think I'd rather leave Ord alone and make a new, separate type class for partial orderings.

Wait what? I didn't realize this was how Ordering was defined: https://github.com/purescript/purescript-prelude/blob/master/src/Prelude.purs#L758

Why not just add one more constructor?

data Ordering = LT | EQ | GT | NC

where NC is iNComparable to.

[hdgarrood]

If you mean the example from Figure 2(a), then shouldn't the last line read _ <= _ = true

Oh - sorry, yeah, I wasn't quite right. I think it's really this:

(<=) :: D -> D -> Boolean
_ <= top = true
bottom <= _ = true
x <= y = x == y

It's not really expressible in terms of the current Ord type class, since we need not (x <= y || y <= x) to hold for any x, y if neither of x and y is top or bottom.

In retrospect, I think I confused myself a little by conflating the uniqueness of a Lattice instance with the possibility of it being derived given an Ord instance. I think any set with an ordering, partial or not, does uniquely determine a lattice, as long as the condition is satisfied that any pair of elements has a LUB and a GLB (source: Wikipedia). Given a partial ordering <=, you can't have more than one way of taking a least upper bound, or greatest lower bound.

However, in PureScript, it's not possible to write a function sup :: forall a. (Ord a) => a -> a -> a that works in the presence of partial orderings, because the lub of x and y might be neither of x and y — because of parametricity, we can't produce any values of the type a other than the ones we're given in the arguments.

I always thought Ord did represent a partial ordering

Not in Haskell, by the looks of things: https://hackage.haskell.org/package/base-4.8.0.0/docs/Prelude.html#t:Ord

I looked back and Ord has been described as "for totally ordered datatypes" since base-4.1.

[joneshf]

Sorry, I wasn't aware of how Ordering was defined. I think that negates everything I've posted here.

I am curious now though. How would you define D instances?

data D = Bottom | N Nat | Top

instance a :: Eq D where
  (==) Bottom Bottom = true
  (==) Top    Top    = true
  (==) (N m)  (N n)  = m == n
  (==) _      _      = false

instance b :: Ord D where
  compare Top    Top    = EQ
  compare Top    _      = GT
  compare _      Top    = LT
  compare Bottom Bottom = EQ
  compare Bottom _      = LT
  compare _      Bottom = GT
  compare _      _      = EQ

That seems the only sensible implementation, but then that doesn't satisfy the antisymmetry law. So maybe D can't be represented by the Ord class. Not really a bit deal in the grand scheme of things (not every type has to be able to implement all classes), but maybe there's some reformulation that might work?

[joneshf]

Also, I'm seeing now why it's not so simple to just add another constructor to Ordering. It pretty much breaks trichotomy. So you can't reason about things as easily down the line. But I also suspect most people down the line aren't aware that EQ means both equality and incomparability.

[hdgarrood]

I think the problem is the way (<=) is defined:

(<=) a1 a2 = case a1 `compare` a2 of
  GT -> false
  _ -> true

If we want Ord to be a partial ordering, and we assume that we're leaving Ordering alone, I think it should be:

(<=) a1 a2 = case a1 `compare` a2 of
  GT -> false
  EQ -> a1 == a2
  LT -> true

Although I do quite like the idea of a separate constructor for "incomparable".

Also, I'm seeing now why it's not so simple to just add another constructor to Ordering. It pretty much breaks trichotomy

If Ord is really a partial ordering then it shouldn't be expected to satisfy trichotomy. Take D from that paper: 1 < 2, 1 == 2, and 1 > 2 would all be false.

[paf31]

If it is a total ordering, then there are no interesting lattices, because every ordering is just one big chain. I feel like there is more value in letting Ord represent partial orderings, since Eq lets us disambiguate equal and noncomparable elements. What is the downside of allowing partial orderings? The Map implementation currently works with partial Ord instances, I think.

[hdgarrood]

I think total orderings are:

• much more widely understood
• significantly easier to reason about
• much more common

than partial (non-total) orderings, so I think I'd rather have a total ordering type class in the Prelude.

For the Map instance, do you mean this one? https://github.com/purescript/purescript-maps/blob/master/src/Data/Map.purs#L50-L51

I guess that means the Ord instance for Map is non-total iff either of its keys or values are, since it's converting to an array of tuples first, and both Array and Tuple use lexicographical ordering.

[paf31]

Total orderings could easily form a subclass with an additional law.

For Map, I was referring to insert and delete which both use the Ord constraint.

[hdgarrood]

Total orderings could easily form a subclass with an additional law.

True. What do you think about changing (<=) etc as I described a minute ago?

For Map, I was referring to insert and delete which both use the Ord constraint.

Come to think of it, I am not sure if a tree-based Map would work without a total ordering on keys.

According to http://www.cs.princeton.edu/~dpw/courses/cos326-12/ass/2-3-trees.pdf every element in a right subtree (of either a 2- or 3-node) must be >= to the root. The insert implementation in purescript-maps doesn't seem to respect this for partial orderings, as it will look in the right subtree if k < k1 and k == k1 both evaluate to false. It seems to be assuming that the trichotomy property holds.

[hdgarrood]

I think Map might actually be broken if the keys have a non-total ordering. See https://github.com/hdgarrood/purescript-maps/commit/755a9c874e7b3b879327a6f2d6543d27dcca32b3

[hdgarrood]

Also, I'm not sure if a tree-based map implementation like the one in purescript-maps is necessarily broken in the presence of non-total key orderings, but it does appear impossible to ensure logarithmic insert/lookup time in this case.

[joneshf]

I think there's a purpose for both. Maybe the prelude doesn't need to have both. If a partial order is chosen, then I feel Ordering should add another constructor.

Also, there should be more partial orderings than total orderings, since a total ordering is stronger than a partial ordering.

Also, I'm not sure if a tree-based map implementation like the one in purescript-maps is necessarily broken in the presence of non-total key orderings, but it does appear impossible to ensure logarithmic insert/lookup time in this case.

That's what I meant about it breaking trichotomy. It's not necessarily that anyone stated trichotomy holds for Ordering/Ord (nor does trichotomy need to hold in the first place), but I think many of us have made an assumption that it does. In this case, only the invariants are broken, but in others there could be different bugs.

[hdgarrood]

Also, there should be more partial orderings than total orderings, since a total ordering is stronger than a partial ordering.

I'll try to explain what I meant more clearly. Of all the Ord instances that programmers encounter, I would guess that the vast majority of these represent total orderings.

• Number, String, Boolean, Ordering, Unit all do,
• The instances for Maybe, Either, Const, Tuple, Array, Map, List, Seq all do, as long as their type parameters do.

I don't think I've ever been in a position in Haskell or PureScript where I was aware that I was dealing with a non-totally ordered data type, or found myself in a position where I wanted to abstract over non-total orderings. Generally in Haskell I just slap a deriving Ord on most things, which is also total.

I also came across another potential example of brokenness arising from assuming Ord is a total ordering: if you have two tuples Tuple a b and Tuple c d, and a is incomparable to c, but b < d, then surely would it make more sense for Tuple a b to be regarded as incomparable to Tuple c d? At the moment you get LT.

only the invariants are broken

I think I might have downplayed the severity a little - the test that failed when I tried running the Map tests with partially ordered keys was verifying that M.lookup k (M.insert k v m) == Just v holds, which is arguably quite an important one.

[hdgarrood]

A not-necessarily-exhaustive list of things that use Ord constraints, and break when used with non-total orderings:

• the Ord instance for Tuple, as I described above
• lots of Ord instances which implement lexicographical orderings are broken in the same way: Array, List, Seq, Map, Set...
• Everything in purescript-sequences
• Data.Map insert/lookup purescript-maps
• min and max from purescript-posets / Possible functions. #20 - for a partial ordering, if two elements are incomparable, they have no minimum or maximum. min and max should therefore return Maybe a.
• Consequently, Min, Max, and MinMax from purescript-posets are also broken (since they depend on min and max)

I think that non-total orderings should require an explicit opt-in - it's far too easy to forget about them and just write Ord code that assumes total orderings. I was previously undecided but now I'm pretty sure that putting Lattice and a separate type class for partial orderings in a separate library would be a better approach.

[paf31]

Then, I think we have to have Ord represent totally-ordered sets, but we should add trichotomy to the laws, or equivalently: a == b implies compare a b = EQ.

We could make Poset a superclass of Ord, and Lattice a subclass of Poset, but I don't know if that complexity belongs in Prelude. I think we need Boolean || and && to be in Prelude though, whatever we pick.

The original goal was to refine BoolLike, and I think Lattice does that nicely, but if we're going to use lattices, I think we should be able to represent interesting lattices which are not totally-ordered.

One downside of having Poset <= Ord is that lexicographical ordering can't be defined in any sensible way. What is the Poset instance for Tuple? We would have to make a Lexicographical newtype - not great. So another option is to have a separate Poset hierarchy, but again, that seems like too much complexity for Prelude.

All of the lattice stuff is still in master only, right?

I think the Map issue can be fixed in either case. I think of the issue as a strict generalization of the problem of hash collisions when inserting into a hash map - you get worst case linear time at the leaves if things can't be distinguished by their order.

[hdgarrood]

Re refining BoolLike, have we considered:

class (Eq a, Semiring a) <= BooleanAlgebra a where
  not :: a -> a

and a few additional laws?

We could then have the following functions, with BooleanAlgebra constraints:

(&&) = (*)
(||) = (+)
(==>) a b = not a || b
xor = (x || y) && not (x && y)

All of the lattice stuff is still in master only, right?

In psci 0.6.9.5, I have:

:t (&&)
forall b. (Prelude.BoolLike b) => b -> b -> b

so yes, it seems so.

[joneshf]

This seems to have been resolved by purescript/purescript#1099