From 1649f75ae295de6796fd2317fe08d5f4fa415435 Mon Sep 17 00:00:00 2001 From: Jorge Acereda Date: Fri, 11 Nov 2016 13:23:52 +0100 Subject: [PATCH 1/4] 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 d7f9577..98ac5ab 100644 --- a/src/Data/Enum.purs +++ b/src/Data/Enum.purs @@ -37,10 +37,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 fb36705573bac5a8ea21f6729c7213c15898d7ef Mon Sep 17 00:00:00 2001 From: Jorge Acereda Date: Fri, 11 Nov 2016 16:13:08 +0100 Subject: [PATCH 2/4] 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 98ac5ab..8d530d4 100644 --- a/src/Data/Enum.purs +++ b/src/Data/Enum.purs @@ -37,10 +37,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 8da4a4d2d0da718259f30b241354d62841076625 Mon Sep 17 00:00:00 2001 From: Jorge Acereda Date: Sun, 13 Nov 2016 23:26:21 +0100 Subject: [PATCH 3/4] 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 8d530d4..75590f4 100644 --- a/src/Data/Enum.purs +++ b/src/Data/Enum.purs @@ -41,8 +41,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 f4fb6c1488a3d2795b075ba5dcca0f47f97b77b8 Mon Sep 17 00:00:00 2001 From: Jorge Acereda Date: Tue, 15 Nov 2016 23:02:52 +0100 Subject: [PATCH 4/4] 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 75590f4..30074cb 100644 --- a/src/Data/Enum.purs +++ b/src/Data/Enum.purs @@ -150,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