PLT-1611: Fix Interval for discrete intervals (#5190)

* PLT-1611: Fix Interval for discrete intervals

`Interval` was not in a good place. It violated a bunch of laws.
The first thing this PR does is add a bunch more tests:
- Generic tests for the typeclasses that `Interval` has instances of.
- Some specific tests that test that finite intervals behave the same as
  sets of consecutive numbers.

The latter gives us a "semantic" test that lets us check whether our
operations on intervals are doing the right thing with respect to a
model - in this case the model is the set of values that fall into the
inteval.

Then we need to actually fix `Interval`. The most straightforward
solution I could see is just to restrict most of its operations to
intervals on enumerable types. That lets us turn non-inclusive bounds
into inclusive bounds, which simplifies things a lot. Without that
information, we can't easily even tell if e.g. an interval is empty or
not.

Arguably we should just have never had non-inclusive bounds in the first
place and it's unnecessary generality. However, I think changing that
now would be more disruptive than it is worth.

Fixes #5185

* Review comments

* Add tests for closed boolean intervals

plutus-ledger-api/changelog.d/20230302_163021_michael.peyton-jones_fix_interval.md

@@ -0,0 +1,3 @@
+### Fixed
+
+- Fixed numerous bugs in the behaviour of `Interval`s with open endpoints.

plutus-ledger-api/plutus-ledger-api.cabal

@@ -138,17 +138,17 @@ test-suite plutus-ledger-api-test
 
  build-depends:
  , barbies
- , base >=4.9 && <5
+ , base  >=4.9 && <5
  , bytestring
  , containers
  , extra
  , hedgehog
  , lens
  , mtl
  , nothunks
- , plutus-core ^>=1.2
- , plutus-ledger-api  ^>=1.2
- , plutus-ledger-api-testlib ^>=1.2
+ , plutus-core  ^>=1.2
+ , plutus-ledger-api:{plutus-ledger-api, plutus-ledger-api-testlib} ^>=1.2
+ , plutus-tx:plutus-tx-testlib  ^>=1.2
  , tasty
  , tasty-hedgehog
  , tasty-hunit

plutus-ledger-api/src/PlutusLedgerApi/V1/Interval.hs

@@ -41,21 +41,29 @@ import Prelude qualified as Haskell
 import Prettyprinter (Pretty (pretty), comma, (<+>))
 
 import PlutusTx qualified
+import PlutusTx.Eq as PlutusTx
 import PlutusTx.Lift (makeLift)
+import PlutusTx.Ord as PlutusTx
 import PlutusTx.Prelude
 
+-- See Note [Enumerable Intervals]
 {- | An interval of @a@s.
 
 The interval may be either closed or open at either end, meaning
 that the endpoints may or may not be included in the interval.
 
 The interval can also be unbounded on either side.
 
-The 'Haskell.Eq'uality of two intervals is specified as the canonical, structural equality and not
-the equality of the elements of their two underlying sets; the same holds for 'Haskell.Ord'.
+The 'Eq' instance gives equality of the intervals, not structural equality.
+There is no 'Ord' instance, but 'contains' gives a partial order.
+
+Note that some of the functions on `Interval` rely on `Enum` in order to
+handle non-inclusive endpoints. For this reason, it may not be safe to
+use `Interval`s with non-inclusive endpoints on types whose `Enum`
+instances have partial methods.
 -}
 data Interval a = Interval { ivFrom :: LowerBound a, ivTo :: UpperBound a }
- deriving stock (Haskell.Eq, Haskell.Ord, Haskell.Show, Generic)
+ deriving stock (Haskell.Show, Generic)
  deriving anyclass (NFData)
 
 instance Functor Interval where
@@ -66,7 +74,7 @@ instance Pretty a => Pretty (Interval a) where
 
 -- | A set extended with a positive and negative infinity.
 data Extended a = NegInf | Finite a | PosInf
- deriving stock (Haskell.Eq, Haskell.Ord, Haskell.Show, Generic)
+ deriving stock (Haskell.Show, Generic)
  deriving anyclass (NFData)
 
 instance Functor Extended where
@@ -79,14 +87,30 @@ instance Pretty a => Pretty (Extended a) where
  pretty PosInf = pretty "+∞"
  pretty (Finite a) = pretty a
 
+-- See Note [Enumerable Intervals]
 -- | Whether a bound is inclusive or not.
 type Closure = Bool
 
 -- | The upper bound of an interval.
 data UpperBound a = UpperBound (Extended a) Closure
- deriving stock (Haskell.Eq, Haskell.Ord, Haskell.Show, Generic)
+ deriving stock (Haskell.Show, Generic)
  deriving anyclass (NFData)
 
+-- | For an enumerable type, turn an upper bound into a single inclusive
+-- bounding value.
+--
+-- Since the type is enumerable, non-inclusive bounds are equivalent
+-- to inclusive bounds on the predecessor.
+--
+-- See Note [Enumerable Intervals]
+inclusiveUpperBound :: Enum a => UpperBound a -> Extended a
+-- already inclusive
+inclusiveUpperBound (UpperBound v True) = v
+-- take pred
+inclusiveUpperBound (UpperBound (Finite x) False) = Finite $ pred x
+-- an infinity: inclusive/non-inclusive makes no difference
+inclusiveUpperBound (UpperBound v False) = v
+
 instance Functor UpperBound where
  fmap f (UpperBound e c) = UpperBound (f <$> e) c
 
@@ -98,9 +122,24 @@ instance Pretty a => Pretty (UpperBound a) where
 
 -- | The lower bound of an interval.
 data LowerBound a = LowerBound (Extended a) Closure
- deriving stock (Haskell.Eq, Haskell.Ord, Haskell.Show, Generic)
+ deriving stock (Haskell.Show, Generic)
  deriving anyclass (NFData)
 
+-- | For an enumerable type, turn an lower bound into a single inclusive
+-- bounding value.
+--
+-- Since the type is enumerable, non-inclusive bounds are equivalent
+-- to inclusive bounds on the successor.
+--
+-- See Note [Enumerable Intervals]
+inclusiveLowerBound :: Enum a => LowerBound a -> Extended a
+-- already inclusive
+inclusiveLowerBound (LowerBound v True) = v
+-- take succ
+inclusiveLowerBound (LowerBound (Finite x) False) = Finite $ succ x
+-- an infinity: inclusive/non-inclusive makes no difference
+inclusiveLowerBound (LowerBound v False) = v
+
 instance Functor LowerBound where
  fmap f (LowerBound e c) = LowerBound (f <$> e) c
 
@@ -127,6 +166,9 @@ instance Eq a => Eq (Extended a) where
  Finite l == Finite r = l == r
  _ == _ = False
 
+instance Eq a => Haskell.Eq (Extended a) where
+ (==) = (PlutusTx.==)
+
 instance Ord a => Ord (Extended a) where
  {-# INLINABLE compare #-}
  NegInf `compare` NegInf = EQ
@@ -137,31 +179,40 @@ instance Ord a => Ord (Extended a) where
  PosInf `compare` _ = GT
  Finite l `compare` Finite r = l `compare` r
 
-instance Eq a => Eq (UpperBound a) where
+instance Ord a => Haskell.Ord (Extended a) where
+ compare = PlutusTx.compare
+
+-- See Note [Enumerable Intervals]
+instance (Enum a, Eq a) => Eq (UpperBound a) where
  {-# INLINABLE (==) #-}
- UpperBound v1 in1 == UpperBound v2 in2 = v1 == v2 && in1 == in2
+ b1 == b2 = inclusiveUpperBound b1 == inclusiveUpperBound b2
 
-instance Ord a => Ord (UpperBound a) where
+instance (Enum a, Eq a) => Haskell.Eq (UpperBound a) where
+ (==) = (PlutusTx.==)
+
+-- See Note [Enumerable Intervals]
+instance (Enum a, Ord a) => Ord (UpperBound a) where
  {-# INLINABLE compare #-}
- UpperBound v1 in1 `compare` UpperBound v2 in2 = case v1 `compare` v2 of
- LT -> LT
- GT -> GT
- -- A closed upper bound is bigger than an open upper bound. This corresponds
- -- to the normal order on Bool.
- EQ -> in1 `compare` in2
-
-instance Eq a => Eq (LowerBound a) where
+ b1 `compare` b2 = inclusiveUpperBound b1 `compare` inclusiveUpperBound b2
+
+instance (Enum a, Ord a) => Haskell.Ord (UpperBound a) where
+ compare = PlutusTx.compare
+
+-- See Note [Enumerable Intervals]
+instance (Enum a, Eq a) => Eq (LowerBound a) where
  {-# INLINABLE (==) #-}
- LowerBound v1 in1 == LowerBound v2 in2 = v1 == v2 && in1 == in2
+ b1 == b2 = inclusiveLowerBound b1 == inclusiveLowerBound b2
 
-instance Ord a => Ord (LowerBound a) where
+instance (Enum a, Eq a) => Haskell.Eq (LowerBound a) where
+ (==) = (PlutusTx.==)
+
+-- See Note [Enumerable Intervals]
+instance (Enum a, Ord a) => Ord (LowerBound a) where
  {-# INLINABLE compare #-}
- LowerBound v1 in1 `compare` LowerBound v2 in2 = case v1 `compare` v2 of
- LT -> LT
- GT -> GT
- -- An open lower bound is bigger than a closed lower bound. This corresponds
- -- to the *reverse* of the normal order on Bool.
- EQ -> in2 `compare` in1
+ b1 `compare` b2 = inclusiveLowerBound b1 `compare` inclusiveLowerBound b2
+
+instance (Enum a, Ord a) => Haskell.Ord (LowerBound a) where
+ compare = PlutusTx.compare
 
 {-# INLINABLE strictUpperBound #-}
 {- | Construct a strict upper bound from a value.
@@ -195,25 +246,38 @@ The resulting bound includes all values that are equal or smaller than the input
 upperBound :: a -> UpperBound a
 upperBound a = UpperBound (Finite a) True
 
-instance Ord a => JoinSemiLattice (Interval a) where
+-- See Note [Enumerable Intervals]
+instance (Enum a, Ord a) => JoinSemiLattice (Interval a) where
  {-# INLINABLE (\/) #-}
  (\/) = hull
 
-instance Ord a => BoundedJoinSemiLattice (Interval a) where
+-- See Note [Enumerable Intervals]
+instance (Enum a, Ord a) => BoundedJoinSemiLattice (Interval a) where
  {-# INLINABLE bottom #-}
  bottom = never
 
-instance Ord a => MeetSemiLattice (Interval a) where
+-- See Note [Enumerable Intervals]
+instance (Enum a, Ord a) => MeetSemiLattice (Interval a) where
  {-# INLINABLE (/\) #-}
  (/\) = intersection
 
-instance Ord a => BoundedMeetSemiLattice (Interval a) where
+-- See Note [Enumerable Intervals]
+instance (Enum a, Ord a) => BoundedMeetSemiLattice (Interval a) where
  {-# INLINABLE top #-}
  top = always
 
-instance Eq a => Eq (Interval a) where
+-- See Note [Enumerable Intervals]
+instance (Enum a, Ord a) => Eq (Interval a) where
  {-# INLINABLE (==) #-}
- l == r = ivFrom l == ivFrom r && ivTo l == ivTo r
+ -- Degenerate case: both the intervals are empty.
+ -- There can be many empty intervals, so we check for this case
+ -- explicitly
+ iv1 == iv2 | isEmpty iv1 && isEmpty iv2 = True
+ (Interval lb1 ub1) == (Interval lb2 ub2) = lb1 == lb2 && ub1 == ub2
+
+instance (Enum a, Ord a) => Haskell.Eq (Interval a) where
+ {-# INLINABLE (==) #-}
+ (==) = (PlutusTx.==)
 
 {-# INLINABLE interval #-}
 -- | @interval a b@ includes all values that are greater than or equal to @a@
@@ -255,7 +319,7 @@ never = Interval (LowerBound PosInf True) (UpperBound NegInf True)
 
 {-# INLINABLE member #-}
 -- | Check whether a value is in an interval.
-member :: Ord a => a -> Interval a -> Bool
+member :: (Enum a, Ord a) => a -> Interval a -> Bool
 member a i = i `contains` singleton a
 
 {-# INLINABLE overlaps #-}
@@ -267,46 +331,69 @@ overlaps l r = not $ isEmpty (l `intersection` r)
 {-# INLINABLE intersection #-}
 -- | 'intersection a b' is the largest interval that is contained in 'a' and in
 -- 'b', if it exists.
-intersection :: Ord a => Interval a -> Interval a -> Interval a
+intersection :: (Enum a, Ord a) => Interval a -> Interval a -> Interval a
 intersection (Interval l1 h1) (Interval l2 h2) = Interval (max l1 l2) (min h1 h2)
 
 {-# INLINABLE hull #-}
 -- | 'hull a b' is the smallest interval containing 'a' and 'b'.
-hull :: Ord a => Interval a -> Interval a -> Interval a
+hull :: (Enum a, Ord a) => Interval a -> Interval a -> Interval a
 hull (Interval l1 h1) (Interval l2 h2) = Interval (min l1 l2) (max h1 h2)
 
 {-# INLINABLE contains #-}
 {- | @a `contains` b@ is true if the 'Interval' @b@ is entirely contained in
 @a@. That is, @a `contains` b@ if for every entry @s@, if @member s b@ then
 @member s a@.
 -}
-contains :: Ord a => Interval a -> Interval a -> Bool
+contains :: (Enum a, Ord a) => Interval a -> Interval a -> Bool
+-- Everything contains the empty interval
+contains _ i2 | isEmpty i2 = True
+-- Nothing is contained in the empty interval (except the empty interval,
+-- which is already handled)
+contains i1 _ | isEmpty i1 = False
+-- Otherwise we check the endpoints. This doesn't work for empty intervals,
+-- hence the cases above.
 contains (Interval l1 h1) (Interval l2 h2) = l1 <= l2 && h2 <= h1
 
 {-# INLINABLE isEmpty #-}
-{- | Check if an 'Interval' is empty.
-
-There can be many empty intervals, given a set of values.
-Two 'Interval's being empty does not imply that they are `Haskell.Eq`ual to each other.
--}
+{- | Check if an 'Interval' is empty. -}
 isEmpty :: (Enum a, Ord a) => Interval a -> Bool
-isEmpty (Interval (LowerBound v1 in1) (UpperBound v2 in2)) = case v1 `compare` v2 of
- LT -> if openInterval then checkEnds v1 v2 else False
+isEmpty (Interval lb ub) = case inclusiveLowerBound lb `compare` inclusiveUpperBound ub of
+ -- We have at least two possible values, the lower bound and the upper bound
+ LT -> False
+ -- We have one possible value, the lower bound/upper bound
+ EQ -> False
+ -- We have no possible values
  GT -> True
- EQ -> not (in1 && in2)
- where
- openInterval = in1 == False && in2 == False
- -- | We check two finite ends to figure out if there are elements between them.
- -- If there are no elements then the interval is empty (#3467).
- checkEnds (Finite v1') (Finite v2') = succ v1' == v2'
- checkEnds _ _ = False
 
 {-# INLINABLE before #-}
 -- | Check if a value is earlier than the beginning of an 'Interval'.
-before :: Ord a => a -> Interval a -> Bool
+before :: (Enum a, Ord a) => a -> Interval a -> Bool
 before h (Interval f _) = lowerBound h < f
 
 {-# INLINABLE after #-}
 -- | Check if a value is later than the end of an 'Interval'.
-after :: Ord a => a -> Interval a -> Bool
+after :: (Enum a , Ord a) => a -> Interval a -> Bool
 after h (Interval _ t) = upperBound h > t
+
+{- Note [Enumerable Intervals]
+The 'Interval' type is set up to handle open intervals, where we have non-inclusive
+bounds. These are only meaningful for orders where there do not exist (computable)
+joins and meets over all elements greater or less than an element.
+
+If those do exist, we can eliminate non-inclusive bounds in favour of inclusive bounds.
+For example, in the integers, (x, y) is equivalent to [x+1, y-1], because
+x+1 = sup { z | z > x} and y-1 = inf { z | z < y }.
+
+Checking equality, containment etc. of intervals with non-inclusive bounds is
+tricky. For example, to know if (x, y) is empty, we need to know if there is a
+value between x and y. We don't have a typeclass for that!
+
+In practice, most of the intervals we care about are enumerable (have 'Enum'
+instances). We assume that `pred` and `succ` calculate the infima/suprema described
+above, and so we can turn non-inclusive bounds into inclusive bounds, which
+makes things much easier. The downside is that some of the `Enum` instances have
+partial implementations, which means that, e.g. `isEmpty (False, True]` will
+throw.
+
+The upshot of this is that many functions in this module require 'Enum'.
+-}