Laws didn't hold for BoundedEnum #23
Conversation
|
I think the last two laws should be left alone; I can't see that the presence of As you realised, of course, I'd like to suggest the following instead:
|
|
I used the word "retracts" based on what I read here, in case anyone was wondering: https://en.wikipedia.org/wiki/Section_(category_theory) |
|
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
And similarly for |
|
If nobody objects I'll implement @hdgarrood's suggestions. |
|
All the above sounds good to me! |
There was a problem hiding this comment.
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
succis the opposite ofpred; if you dosuccand thenpredon a value, you should end up with what you started with (although of course this doesn't apply if you tried tosuccthe last value in an enumeration and therefore gotNothingout).
The non-skipping laws can intuitively be understood as saying thatsuccshouldn't skip over any elements of your type. For example, without the non-skipping laws, it would be permissible to write anEnum Intinstance wheresucc x = Just (x+2), and similarlypred 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.
| -- | - Predecessor: `maybe true (_ < a) (pred a)` | ||
| -- | - Succ retracts pred: `pred a >>= succ >>= pred = pred a` | ||
| -- | - Pred retracts succ: `succ a >>= pred >>= succ = succ a` | ||
| -- | - Non-skipping succ: `y <= x || maybe false (_ <= y) (succ x)` |
There was a problem hiding this comment.
This is a much better reformulation of what I wrote 👍
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
That's fine, perhaps then you could use what I wrote?
| -- | - `pred a < succ a` | ||
| -- | - `pred >=> succ >=> pred = pred` | ||
| -- | - `succ >=> pred >=> succ = succ` | ||
| -- | - Successor: `maybe true (a < _) (succ a)` |
There was a problem hiding this comment.
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.
| -- | - Predecessor: `maybe true (_ < a) (pred a)` | ||
| -- | - Succ retracts pred: `pred a >>= succ >>= pred = pred a` | ||
| -- | - Pred retracts succ: `succ a >>= pred >>= succ = succ a` | ||
| -- | - Non-skipping succ: `b <= a || maybe false (_ <= b) (succ a)` |
There was a problem hiding this comment.
Similarly: b <= a || any (_ <= b) (succ a)?
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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 -> xI 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.
There was a problem hiding this comment.
True, forAllA is somewhat forced there.
given isn't implies AFAICS.
given a b = a `implies` (fromMaybe true b)
There was a problem hiding this comment.
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.
|
It might be good to also add a note that the set of values is partitioned into two sets for each value |
|
Does the partitioning follow from |
|
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. |
|
Ah, right, yeah. :) |
|
Another slightly different formulation with three sets says that the set of values partitions into
which gives a nice little proof technique: if you can prove that (I think..) |
|
Are we happy with the laws in this PR now then? Sorry, I kinda lost track of the discussion. /cc @hdgarrood @paf31 |
|
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 |
|
Also regarding |
|
What's the status of this? Coming back to this, I must say I do prefer the docs which use |
|
Merged in #32. Thank you! |
No description provided.