Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Laws didn't hold for BoundedEnum #23

Closed
wants to merge 4 commits into from
Closed

Laws didn't hold for BoundedEnum #23

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
1649f75
Laws didn't hold for BoundedEnum
jacereda Nov 11, 2016
fb36705
New laws
jacereda Nov 11, 2016
8da4a4d
Fix inconsistency in variable names
jacereda Nov 13, 2016
f4fb6c1
Use pred/succ instead of arithmetic
jacereda Nov 15, 2016
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 8 additions & 6 deletions src/Data/Enum.purs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,10 +37,12 @@ derive newtype instance ordCardinality :: Ord (Cardinality a)
-- | Type class for enumerations.
-- |
-- | Laws:
-- | - `succ a > pred a`
-- | - `pred a < succ a`
-- | - `pred >=> succ >=> pred = pred`
-- | - `succ >=> pred >=> succ = succ`
-- | - Successor: `maybe true (a < _) (succ a)`
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)`
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

True, forAllA is somewhat forced there.

given isn't implies AFAICS.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

-- | - Non-skipping pred: `a <= b || maybe false (b <= _) (pred a)`
class Ord a <= Enum a where
succ :: a -> Maybe a
pred :: a -> Maybe a
Expand Down Expand Up @@ -148,8 +150,8 @@ downFrom = unfoldr (map diag <<< pred)
-- | - ```pred top >>= pred >>= pred ... pred [cardinality - 1 times] == bottom```
-- | - ```forall a > bottom: pred a >>= succ == Just a```
-- | - ```forall a < top: succ a >>= pred == Just a```
-- | - ```forall a > bottom: fromEnum <$> pred a = Just (fromEnum a - 1)```
-- | - ```forall a < top: fromEnum <$> succ a = Just (fromEnum a + 1)```
-- | - ```forall a > bottom: fromEnum <$> pred a = pred (fromEnum a)```
-- | - ```forall a < top: fromEnum <$> succ a = succ (fromEnum a)```
-- | - ```e1 `compare` e2 == fromEnum e1 `compare` fromEnum e2```
-- | - ```toEnum (fromEnum a) = Just a```
class (Bounded a, Enum a) <= BoundedEnum a where
Expand Down