Designing strongly typed range
Gautier DI FOLCO September 24, 2024 [Haskell] #haskell #designRecently in our codebase I have introduced ranges to disambiguate the values we passed around, such as:
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:
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:
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
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