How to specify a number range as a type in Idris?

Question

I've been experimenting with Idris and it seems like it should be simple to specify some sort of type for representing all numbers between two different numbers, e.g. NumRange 5 10 is the type of all numbers between 5 and 10. I'd like to include doubles/floats, but a type for doing the same with integers would be equally useful. How would I go about doing this?

Answer 1

In practice, you may do better to simply check the bounds as needed, but you can certainly write a data type to enforce such a property.

One straightforward way to do it is like this:

data Range : Ord a => a -> a -> Type where
  MkRange : Ord a => (x,y,z : a) -> (x >= y && (x <= z) = True) -> Range y z

I've written it generically over the Ord typeclass, though you may need to specialize it. The range requirement is expressed as an equation, so you simply supply a Refl when constructing it, and the property will then be checked. For example: MkRange 3 0 10 Refl : Range 0 10. One disadvantage of something like this is the inconvenience of having to extract the contained value. And of course if you want to construct an instance programmatically you'll need to supply the proofs that the bounds are indeed satisfied, or else do it in some context that allows for failure, like Maybe.

We can write a more elegant example for Nats without much trouble, since for them we already have a library data type to represent comparison proofs. In particular LTE, representing less-than-or-equal-to.

data InRange : Nat -> Nat -> Type where
  IsInRange : (x : Nat) -> LTE n x -> LTE x m -> InRange n m

Now this data type nicely encapsulates a proof that n ≤ x ≤ m. It would be overkill for many casual applications, but it certainly shows how you might use dependent types for this purpose.