Plutus.V1.Ledger.Interval

• 1. 📜 Overview

• 2. 🔧 LANGUAGE PRAGMAS AND IMPORTS

• 3. 🗄️ Data Types

  • 3.1 ➰ Extended

  • 3.2 🆙 UpperBound

  • 3.3 🆕 LowerBound

  • 3.4 📏 Interval

• 4. ⚙️ Functions

  • 4.1 ⚖️ strictUpperBound

  • 4.2 ⚖️ strictLowerBound

  • 4.3 🔽 lowerBound

  • 4.4 🔼 upperBound

  • 4.5 🏷️ interval

  • 4.6 🔢 singleton

  • 4.7 ▶️ from

  • 4.8 ◀️ to

  • 4.9 ♾️ always

  • 4.10 🚫 never

  • 4.11 🧮 member

  • 4.12 🔄 overlaps

  • 4.13 🛠️ intersection

  • 4.14 🏔️ hull

  • 4.15 🔍 contains

  • 4.16 📭 isEmpty

  • 4.17 ⏮️ before

  • 4.18 ⏭️ after

• 5. 🤝 Typeclass Instances

• 6. 🏭 On-Chain Derivations

• 7. 📚 Glossary

---

1 📜 Overview

The Plutus.V1.Ledger.Interval module defines a generic interval type over any ordered domain, with support for open/closed and bounded/unbounded ends, plus a rich API for constructing and querying intervals:

• Extended a: values extended with negative and positive infinity.

• LowerBound a, UpperBound a: bound types carrying an Extended a and a closure flag.

• Interval a: a pair of lower and upper bounds.

• Functions: create intervals (interval, singleton, from, to, always, never) and query them (member, overlaps, etc.).

• Instances: Functor, Eq, Ord, JoinSemiLattice, MeetSemiLattice, and Pretty for human-friendly rendering.

All key types derive Generic and NFData, and on-chain serialization is provided via makeIsDataIndexed and makeLift.

---

2 🔧 LANGUAGE PRAGMAS AND IMPORTS

{-# LANGUAGE DeriveAnyClass       #-}
{-# LANGUAGE DeriveGeneric        #-}
{-# LANGUAGE DerivingStrategies   #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE MonoLocalBinds       #-}
{-# LANGUAGE NoImplicitPrelude    #-}
{-# LANGUAGE TemplateHaskell      #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-omit-interface-pragmas #-}
{-# OPTIONS_GHC -fno-specialise            #-}
{-# OPTIONS_GHC -fno-ignore-interface-pragmas #-}

module Plutus.V1.Ledger.Interval where

import Control.DeepSeq (NFData)
import GHC.Generics    (Generic)
import Prelude qualified as Haskell
import Prettyprinter  (Pretty(pretty), comma, (<+>))

import PlutusTx qualified
import PlutusTx.Lift (makeLift)
import PlutusTx.Prelude

• DataKinds not needed here; key pragmas include generic deriving, template Haskell, and flexible/monomorphic binds.

• NoImplicitPrelude: uses PlutusTx.Prelude for on-chain code.

• OPTIONS_GHC ensure interface pragmas and specialization are preserved for on-chain performance.

---

3 🗄️ Data Types

3.1 ➰ Extended

data Extended a = NegInf | Finite a | PosInf
  deriving stock   (Haskell.Eq, Haskell.Ord, Haskell.Show, Generic)
  deriving anyclass (NFData)

• Purpose: represent values with negative or positive infinity.

• Example:

  Finite 5 :: Extended Int
  NegInf             == NegInf
  PosInf             > Finite 100

3.2 🆙 UpperBound

data UpperBound a = UpperBound (Extended a) Closure
  deriving stock   (Haskell.Eq, Haskell.Ord, Haskell.Show, Generic)
  deriving anyclass (NFData)

• Fields:

  • Extended a endpoint.

  • Closure flag: True = inclusive (]), False = exclusive ()).

• Example:

  UpperBound (Finite 10) True  -- represents ≤10
  UpperBound PosInf False      -- unbounded above

3.3 🆕 LowerBound

data LowerBound a = LowerBound (Extended a) Closure
  deriving stock   (Haskell.Eq, Haskell.Ord, Haskell.Show, Generic)
  deriving anyclass (NFData)

• Closure: True = inclusive ([), False = exclusive (().

• Example:

  LowerBound (Finite 0) True   -- represents ≥0
  LowerBound NegInf False      -- unbounded below

3.4 📏 Interval

data Interval a = Interval
  { ivFrom :: LowerBound a
  , ivTo   :: UpperBound a
  }
  deriving stock   (Haskell.Eq, Haskell.Ord, Haskell.Show, Generic)
  deriving anyclass (NFData)

• Combines lower and upper bounds into an interval.

• Example:

  Interval (lowerBound 1) (upperBound 5)  -- [1,5]

---

4 ⚙️ Functions

All functions are marked {-# INLINABLE #-} for on-chain compilation.

4.1 ⚖️ strictUpperBound

strictUpperBound :: a -> UpperBound a
strictUpperBound a = UpperBound (Finite a) False

• Inputs: endpoint a

• Output: exclusive upper bound (a.

• Example:

  strictUpperBound 10  -- represents values <10

4.2 ⚖️ strictLowerBound

strictLowerBound :: a -> LowerBound a
strictLowerBound a = LowerBound (Finite a) False

• Exclusive lower bound (a.

4.3 🔽 lowerBound

lowerBound :: a -> LowerBound a
lowerBound a = LowerBound (Finite a) True

• Inclusive lower bound [a.

4.4 🔼 upperBound

upperBound :: a -> UpperBound a
upperBound a = UpperBound (Finite a) True

• Inclusive upper bound a].

4.5 🏷️ interval

interval :: a -> a -> Interval a
interval lo hi = Interval (lowerBound lo) (upperBound hi)

• Closed interval [lo,hi].

4.6 🔢 singleton

singleton :: a -> Interval a
singleton x = interval x x

• Single-value interval [x,x].

4.7 ▶️ from

from :: a -> Interval a
from lo = Interval (lowerBound lo) (UpperBound PosInf True)

• Interval [lo, +∞].

4.8 ◀️ to

to :: a -> Interval a
to hi = Interval (LowerBound NegInf True) (upperBound hi)

• Interval [-∞, hi].

4.9 ♾️ always

always :: Interval a
always = Interval (LowerBound NegInf True) (UpperBound PosInf True)

• Entire domain [-∞, +∞].

4.10 🚫 never

never :: Interval a
never = Interval (LowerBound PosInf True) (UpperBound NegInf True)

• Empty interval.

4.11 🧮 member

member :: Ord a => a -> Interval a -> Bool
member x i = i `contains` singleton x

• Checks if x lies within interval i.

4.12 🔄 overlaps

overlaps :: (Enum a, Ord a) => Interval a -> Interval a -> Bool
overlaps a b = not $ isEmpty (a `intersection` b)

• True if intervals share any point.

4.13 🛠️ intersection

intersection :: Ord a => Interval a -> Interval a -> Interval a
intersection (Interval l1 u1) (Interval l2 u2) = Interval (max l1 l2) (min u1 u2)

• Largest common sub-interval.

4.14 🏔️ hull

hull :: Ord a => Interval a -> Interval a -> Interval a
hull (Interval l1 u1) (Interval l2 u2) = Interval (min l1 l2) (max u1 u2)

• Smallest interval containing both.

4.15 🔍 contains

contains :: Ord a => Interval a -> Interval a -> Bool
contains (Interval l1 u1) (Interval l2 u2) = l1 <= l2 && u2 <= u1

• Checks if one interval is inside another.

4.16 📭 isEmpty

isEmpty :: (Enum a, Ord a) => Interval a -> Bool

• True for empty intervals, including degenerate cases where bounds cross or close excludes endpoints.

4.17 ⏮️ before

before :: Ord a => a -> Interval a -> Bool
before x (Interval l _) = strictLowerBound x > l

• True if x lies strictly before the interval’s start.

4.18 ⏭️ after

after :: Ord a => a -> Interval a -> Bool
after x (Interval _ u) = strictUpperBound x < u

• True if x is strictly after the interval’s end.

---

5 🤝 Typeclass Instances

instance Functor Interval where
  fmap f (Interval l u) = Interval (fmap f l) (fmap f u)

• Lifts functions over interval endpoints.

instance Ord a => JoinSemiLattice (Interval a) where
  (\/) = hull
instance Ord a => BoundedJoinSemiLattice (Interval a) where
  bottom = never

• Join (/) = hull; bottom = empty interval.

instance Ord a => MeetSemiLattice (Interval a) where
  (/\) = intersection
instance Ord a => BoundedMeetSemiLattice (Interval a) where
  top = always

• Meet (/) = intersection; top = whole domain.

Explicit Eq and Ord instances via deriving strategies or INLINABLE definitions ensure correct on-chain behavior for Extended, UpperBound, LowerBound, and Interval.

---

6 🏭 On-Chain Derivations

PlutusTx.makeIsDataIndexed ''Extended      [('NegInf,0),('Finite,1),('PosInf,2)]
PlutusTx.makeIsDataIndexed ''UpperBound    [('UpperBound,0)]
PlutusTx.makeIsDataIndexed ''LowerBound    [('LowerBound,0)]
PlutusTx.makeIsDataIndexed ''Interval      [('Interval,0)]

makeLift ''Extended
makeLift ''LowerBound
makeLift ''UpperBound
makeLift ''Interval

• Generates IsData and Lift for on-chain serialization and embedding.

---

7 📚 Glossary

• Extended a: domain a extended with NegInf and PosInf.

• Closure: Bool flag indicating inclusive (True) or exclusive (False) bound.

• LowerBound/UpperBound: bound wrappers pairing an Extended a with a closure.

• Interval a: value range from a lower to an upper bound.

• Functor: structure supporting fmap for endpoints.

• Join/Meet SemiLattice: algebraic classes for hull and intersection.

• BoundedJoin/MeetSemiLattice: includes bottom (empty) and top (universal) elements.

• INLINABLE: GHC pragma for on-chain specialization.

• makeIsDataIndexed: TH for IsData instances with constructor indices.

• makeLift: TH for embedding values in PlutusTx.

• StrictData: pragma making all data fields strict.

• NoImplicitPrelude: uses on-chain PlutusTx.Prelude in place of Haskell’s.