Designing strongly typed range

Recently in our codebase I have introduced ranges to disambiguate the values we passed around, such as:

listGuideTours :: Members AppEffects r => GuideId -> Day -> Day -> m [Tour]

It's not clear wether each bound is exclusive or not (even though we assumed first argument should be inferior to the second).

Hackage has few range libraries: range, data-interval, interval, intervals, etc.

Which let me write something like:

listGuideTours :: Members AppEffects r => GuideId -> Range Day -> m [Tour]

The thing is, nothing forces Range to have any bounds, that's why I wanted to make this log: show the design process behind the incremental strong typing.

Let's start with a regular types:

-- | Represents a bound, with exclusiveness.
data Bound a
  = -- | The value should be included in the bound.
    InclusiveBound a
  | -- | The value should be excluded in the bound.
    ExclusiveBound a
  deriving stock (Eq, Show, Functor)

-- | All kinds of ranges.
data Range a
  = -- | A single element. It is equivalent to @SpanRange (InclusiveBound a) (InclusiveBound a)@.
    SingletonRange a
  | -- | A span of elements. Make sure lower bound <= upper bound.
    SpanRange (Bound a) (Bound a)
  | -- | A range with a finite lower bound and an infinite upper bound.
    LowerBoundRange (Bound a)
  | -- | A range with an infinite lower bound and a finite upper bound.
    UpperBoundRange (Bound a)
  | -- | An infinite range.
    InfiniteRange
  | -- | An empty range.
    EmptyRange
  deriving stock (Eq, Functor)

The thing is, we need to somehow add type-level information on each constructor to specify the presence/absence of the bounds, however, by default, all constructors have the same types.

To do so, we need to rely on GADTs:

-- | All kinds of ranges.
data Range (hasLowerBound :: Bool) (hasUpperBound :: Bool) (a :: Type) where
  -- | A single element. It is equivalent to @SpanRange (InclusiveBound a) (InclusiveBound a)@.
  SingletonRange :: a -> Range 'True 'True a
  -- | A span of elements. Make sure lower bound <= upper bound.
  SpanRange :: Bound a -> Bound a -> Range 'True 'True a
  -- | A range with a finite lower bound and an infinite upper bound.
  LowerBoundRange :: Bound a -> Range 'True 'False a
  -- | A range with an infinite lower bound and a finite upper bound.
  UpperBoundRange :: Bound a -> Range 'False 'True a
  -- | An infinite range.
  InfiniteRange :: Range 'False 'False a
  -- | An empty range.
  EmptyRange :: Range 'False 'False a

We have introduced two phantom types (types not present at value-level), representing bounds presence as type-level Bool (via dataype promotion).

Great, so far we are able to constraint bounds, but we no longer can mix ranges in lists, such as:

[lbe @Int 1, ubi 1, 1 +=* 2]

Hopefully, Haskell comes with Explicit forall, which allows us to define dataypes "hiding" type variables:

data AnyRange a = forall hasLowerBound hasUpperBound. AnyRange (Range hasLowerBound hasUpperBound a)

So any type/constructor wrapped would have the same type, and could be used in lists again:

[AnyRange $ lbe @Int 1, AnyRange $ ubi 1, AnyRange $ 1 +=* 2]

Consequently, if all Range became identical (at type-level), we can't enforce bounds, back to square one.

We're not done yet, Haskell gives us Constraint kind, kinds are types of types (by default all data type have the kind Type, they can be promoted as seen above, so each constructor have the kind of its type, e.g. 'True kind is Bool).

data AnyRangeFor (c :: (Type -> Type) -> Constraint) a
  = forall hasLowerBound hasUpperBound.
    c (Range hasLowerBound hasUpperBound) =>
    AnyRangeFor (Range hasLowerBound hasUpperBound a)

It means, we have to specify some constraints for every Range wrapped, such as:

      let _ = [AnyRangeFor @WithUpperBound $ ubi 1, AnyRangeFor $ lbe 1, AnyRangeFor $ 1 +=* 2]

won't work, because lbe has no upper bound and WithUpperBound is defined as:

class WithUpperBound range

instance WithUpperBound (Range l 'True)

That being said AnyRange was broken in the process (() has the kind Constraint, while AnyRangeFor's first type parameter should be of type (Type -> Type) -> Constraint):

type AnyRange = AnyRangeFor AnyRangeConstraint

class AnyRangeConstraint (range :: Type -> Type)

instance AnyRangeConstraint (Range l h)

So that it can be used with any Range:

      let _ = [AnyRangeFor @AnyRangeConstraint $ ubi 1, AnyRangeFor $ lbe 1, AnyRangeFor $ 1 +=* 2]

Note: Everything described in the log is packed in typed-range