From 890adb8906f85cba8423c2febfb18da073ec5cc0 Mon Sep 17 00:00:00 2001 From: Jorge Acereda Date: Fri, 11 Nov 2016 13:23:52 +0100 Subject: [PATCH 1/5] Laws didn't hold for BoundedEnum --- src/Data/Enum.purs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Data/Enum.purs b/src/Data/Enum.purs index ecf1281..4e28156 100644 --- a/src/Data/Enum.purs +++ b/src/Data/Enum.purs @@ -39,10 +39,10 @@ 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` +-- | - `succ a > pred a where succ a /= Nothing` +-- | - `pred a < succ a where succ a /= Nothing` +-- | - `pred >=> succ >=> pred = pred where succ a /= Nothing` +-- | - `succ >=> pred >=> succ = succ where succ a /= Nothing` class Ord a <= Enum a where succ :: a -> Maybe a pred :: a -> Maybe a From 1294f2e908ee1d4fe69e44477f8bb94a8bc28c65 Mon Sep 17 00:00:00 2001 From: Jorge Acereda Date: Fri, 11 Nov 2016 16:13:08 +0100 Subject: [PATCH 2/5] New laws --- src/Data/Enum.purs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/Data/Enum.purs b/src/Data/Enum.purs index 4e28156..7395f5a 100644 --- a/src/Data/Enum.purs +++ b/src/Data/Enum.purs @@ -39,10 +39,12 @@ derive newtype instance ordCardinality :: Ord (Cardinality a) -- | Type class for enumerations. -- | -- | Laws: --- | - `succ a > pred a where succ a /= Nothing` --- | - `pred a < succ a where succ a /= Nothing` --- | - `pred >=> succ >=> pred = pred where succ a /= Nothing` --- | - `succ >=> pred >=> succ = succ where succ a /= Nothing` +-- | - Successor: `maybe true (a < _) (succ a)` +-- | - 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)` +-- | - Non-skipping pred: `x <= y || maybe false (y <= _) (pred x)` class Ord a <= Enum a where succ :: a -> Maybe a pred :: a -> Maybe a From 6f34826d54c604cc47bd82d420dec9015c0906f9 Mon Sep 17 00:00:00 2001 From: Jorge Acereda Date: Sun, 13 Nov 2016 23:26:21 +0100 Subject: [PATCH 3/5] Fix inconsistency in variable names --- src/Data/Enum.purs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Enum.purs b/src/Data/Enum.purs index 7395f5a..67f3974 100644 --- a/src/Data/Enum.purs +++ b/src/Data/Enum.purs @@ -43,8 +43,8 @@ derive newtype instance ordCardinality :: Ord (Cardinality a) -- | - 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)` --- | - Non-skipping pred: `x <= y || maybe false (y <= _) (pred x)` +-- | - Non-skipping succ: `b <= a || maybe false (_ <= b) (succ a)` +-- | - Non-skipping pred: `a <= b || maybe false (b <= _) (pred a)` class Ord a <= Enum a where succ :: a -> Maybe a pred :: a -> Maybe a From 186f26a3fca3ba36a197440a9a5f70588773c245 Mon Sep 17 00:00:00 2001 From: Jorge Acereda Date: Tue, 15 Nov 2016 23:02:52 +0100 Subject: [PATCH 4/5] Use pred/succ instead of arithmetic --- src/Data/Enum.purs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Enum.purs b/src/Data/Enum.purs index 67f3974..854c935 100644 --- a/src/Data/Enum.purs +++ b/src/Data/Enum.purs @@ -159,8 +159,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 From 97e2ac555b28a3e790ee3c8f1eb7a539db74bd6e Mon Sep 17 00:00:00 2001 From: Harry Garrood Date: Sat, 29 Jul 2017 17:44:58 +0100 Subject: [PATCH 5/5] Minor tweaks to Enum laws - Use `any` and `all` per @paf31's suggestion - Add law explanations --- src/Data/Enum.purs | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/src/Data/Enum.purs b/src/Data/Enum.purs index 854c935..fb886e6 100644 --- a/src/Data/Enum.purs +++ b/src/Data/Enum.purs @@ -39,12 +39,22 @@ derive newtype instance ordCardinality :: Ord (Cardinality a) -- | Type class for enumerations. -- | -- | Laws: --- | - Successor: `maybe true (a < _) (succ a)` --- | - 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)` --- | - Non-skipping pred: `a <= b || maybe false (b <= _) (pred a)` +-- | - Successor: `all (a < _) (succ a)` +-- | - Predecessor: `all (_ < a) (pred a)` +-- | - Succ retracts pred: `pred >=> succ >=> pred = pred` +-- | - Pred retracts succ: `succ >=> pred >=> succ = succ` +-- | - Non-skipping succ: `b <= a || any (_ <= b) (succ a)` +-- | - Non-skipping pred: `a <= b || any (b <= _) (pred a)` +-- | +-- | The retraction laws can intuitively be understood as saying that `succ` is +-- | the opposite of `pred`; if you apply `succ` and then `pred` to something, +-- | 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)`. class Ord a <= Enum a where succ :: a -> Maybe a pred :: a -> Maybe a