Laws didn't hold for BoundedEnum

[jacereda]

No description provided.

[hdgarrood]

I think the last two laws should be left alone; I can't see that the presence of Nothing causes any problems there.

As you realised, of course, succ a > pred a does not hold if succ a is Nothing, since Nothing is less than everything else, so I agree that that needs addressing. Also, if we have a law-abiding Ord instance, the second law is redundant. Finally, I think it's a bit strange that we're comparing succ a to pred a; wouldn't it make more sense to compare it to a?

I'd like to suggest the following instead:

• Successor: maybe true (_ > a) (succ a)
• Predecessor: maybe true (_ < a) (pred a)
• Succ retracts pred: pred >=> succ >=> pred = pred
• Pred retracts succ: succ >=> pred >=> succ = succ

[hdgarrood]

I used the word "retracts" based on what I read here, in case anyone was wondering: https://en.wikipedia.org/wiki/Section_(category_theory)

[hdgarrood]

Come to think of it, I wonder if we should have a law that prevents you from skipping over things? We already require that we have a total order from the Ord constraint, so it seems like a sensible law to have.

• For all x, there is no y such that y is between x and succ x; i.e. there is no y such that x < y and maybe true (y < _) (succ x) both hold.

And similarly for pred.

[jacereda]

If nobody objects I'll implement @hdgarrood's suggestions.

[garyb]

All the above sounds good to me!

[hdgarrood]

I've just realised that it's not all that easy to develop intuition for what some of these laws mean. I think it would be nice to also add a bit more prose explaining this. (Maybe we should do this for some other classes too.) For example:

The retraction laws can intuitively be understood as saying that succ is the opposite of pred; if you do succ and then pred on a value, you should end up with what you started with (although of course this doesn't apply if you tried to succ the last value in an enumeration and therefore got Nothing out).
The non-skipping laws can intuitively be understood as saying that succ shouldn't skip over any elements of your type. For example, without the non-skipping laws, it would be permissible to write an Enum Int instance where succ x = Just (x+2), and similarly pred x = Just (x-2).

Also bit of a nitpick, but I think it would be nice to be consistent with the variable names. That is, I think we should use either a and b or x and y for values of type a throughout, but not a mixture of the two.

[hdgarrood]

This is a much better reformulation of what I wrote 👍

[jacereda]

I agree it would be nice to explain the rules properly, but since I'm not native I guess I'm not the most appropriate person to do it.

[hdgarrood]

That's fine, perhaps then you could use what I wrote?

[paf31]

This can alternatively be written all (a < _) (succ a), which I think sums things up nicely: if there is a successor, it's greater than the number you first had. In other words, every successor is greater.

[paf31]

Similarly: b <= a || any (_ <= b) (succ a)?

[hdgarrood]

I think I prefer maybe true and maybe false, as bringing in Foldable means you have to recall more things to be able to understand these laws, but I don't feel strongly about this.

[paf31]

yes, I'm not sure either. On the one hand, I have to unpack the maybe definitions when I read them, where I find the any/all definitions clearer (if I read all as ∀, etc.), but Foldable does add some mental overhead.

[jacereda]

I don't know what I'd like to see in the specs, but for -quickcheck-laws, how about something like this? My beginner mind has less problems parsing it than the maybe true/maybe false/any/all alternatives.

    successor :: a -> Boolean
    successor a = forAllA $ (a < _) <$> (succ a)

    predecessor :: a -> Boolean
    predecessor a = forAllA $ (_ < a) <$> (pred a)

    forAllA :: Maybe Boolean -> Boolean
    forAllA = fromMaybe true

    nonSkippingSucc :: a -> a -> Boolean
    nonSkippingSucc a b = given (a < b) $ (_ <= b) <$> (succ a)

    nonSkippingPred :: a -> a -> Boolean
    nonSkippingPred a b = given (b < a) $ (b <= _) <$> (pred a)

    given :: Boolean -> Maybe Boolean -> Boolean
    given a b = not a || fromMaybe true b

[hdgarrood]

forAllA is a bit strange to me because the name doesn't really match up with what it does. For me, it obscures rather than illuminates.

Just an observation: your given is similar to implies from the HeytingAlgebra Boolean instance (which is in Prelude), so I might use that instead.

If maybe is awkward, try imagining it with the definition inlined:

maybe x f y
-- becomes
case y of
  Just z -> f z
  Nothing -> x

I think it's probably best that the checks in quickcheck-laws match as closely as is reasonable with the actual laws in the documentation, though; in this case I think I would stick with the way they're written.

[jacereda]

True, forAllA is somewhat forced there.

given isn't implies AFAICS.

given a b = a `implies` (fromMaybe true b)

[hdgarrood]

Yes, exactly - given isn't implies, but they're similar enough that I would consider using implies instead of defining another function.

But that's a little academic because in this case I think the best approach is to write the checks the same way as the actual laws, as then it's very easy to verify that the checks are actually equivalent to the laws. If the laws are unnecessarily hard to understand we should consider changing the laws themselves so this is no longer the case.

[paf31]

It might be good to also add a note that the set of values is partitioned into two sets for each value a: those <= a, and those >= succ a. Similarly for pred. So succ and pred give us laws which look a bit like trichotomy for the ordering.

[hdgarrood]

Does the partitioning follow from Ord and the non-skipping law, though?

[paf31]

Yes, sorry, I should have said this was just a slightly different way of thinking about non-skipping. As I was unpacking the definition, that's how I understood it.

[hdgarrood]

Ah, right, yeah. :)

[paf31]

Another slightly different formulation with three sets says that the set of values partitions into

• y <= x
• y == x
• any (_ <= y) (succ x)

which gives a nice little proof technique: if you can prove that y > x, and also that z > y for every successor z of x, then y must equal x.

(I think..)

[garyb]

Are we happy with the laws in this PR now then? Sorry, I kinda lost track of the discussion.

/cc @hdgarrood @paf31

[hdgarrood]

Yep, I'm happy with the laws in this PR now. I don't think we have managed to reach a consensus on how best to express these laws in quickcheck-laws yet, but that's arguably outside the scope of this PR, this repo even. I would also like to add a little bit to the documentation about what the laws intuitively mean, but that can come later. 👍 for merging.

[hdgarrood]

Also regarding maybe false vs any - no strong opinion here, I'd be very happy to see this merged either way.

[paf31]

What's the status of this?

Coming back to this, I must say I do prefer the docs which use any and all actually.

[hdgarrood]

Merged in #32. Thank you!