# 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`