Statically-Bounded Numbers

Checking whether a given value is within its allowable range is a common validation that must occur.

At TripShot, we love the compile-time guarantees you get from the type system of Haskell. Many values are best represented by numbers, especially integral ones. But often we need to constraint the range of values allowed.

Some examples include:

  • The bicycle capacity of a vehicle must be 0 or greater
  • The position of an item in a list on-screen must be 1 or greater
  • The latitude of a location is between -90 and 90
  • The percentage of vehicle battery capacity must be between 0 and 100

The usual way of representing, say, the bicycle capacity, would be with an Int. But then we would end up with partial functions, that need to check at runtime that the value is non-negative:

1if bicycleCapacity < 0 2 then error "Negative bicycle capacity" 3 else ...

What we want is to be able to read the bicycle capacity from the DB, or from user input, confirm once at runtime that it’s not negative, then pass it around in a variable that is known statically to be non-negative. This is the “parse, don’t validate” pattern. We would also like to be able to hard-code a bicycle capacity value and not ever have to check it at runtime.

We could use a Numeric.Natural, but it only checks at runtime that values are non-negative, and it’s represented using arbitrary-precision numbers, so it’s less efficient than using an Int. We could use Word, but it has modular arithmetic semantics, so 0 - 1 wraps to maxBound. And none of those would help us with values that must be 1 or greater, or have an upper bound.

We solved the problem using type-level natural numbers. We created these two datatypes:

1newtype Bound (l :: Nat) (u :: Nat) a = Bound a 2newtype LowerBound (l :: Nat) a = LowerBound a

The LowerBound type is for values that are bounded below but not above, and Bound is for values that are bounded on both sides. We couldn’t call it Bounded, because that would conflict with the type class from Prelude.

For each of these types, we created some handy constraint synonyms:

1type Bounds l u = (l <= u, KnownNat l, KnownNat u) 2type BoundNum l u a = (Bounds l u, Ord a, Num a) 3type LBoundNum l a = (KnownNat l, Ord a, Num a)

We have a function to parse a number into maybe a Bound number at runtime:

1maybeBound :: forall l u a. (BoundNum l u a) => a -> Maybe (Bound l u a) 2maybeBound n 3 | l <= n && n <= u = Just (Bound n) 4 | otherwise = Nothing 5 where 6 l = natVal (Proxy @l) & fromInteger 7 u = natVal (Proxy @u) & fromInteger

We can specify the bounds using the TypeApplications extension. Some example uses:

1> maybeBound @1 @5 4 2Just (Bound @1 @5 4) 3> maybeBound @1 @5 0 4Nothing

To specify a Bound value that is checked at compile time, you can use the bound function. We made this a type class method so it could be shared between Bound and LowerBound:

1class IsBound n a where 2 type BoundConstraint a n :: Constraint 3 bound :: (BoundConstraint a n, KnownNat n) => a 4instance IsBound n (Bound l u a) where 5 type BoundConstraint (Bound l u a) n = (l <= u, Num a, l <= n, n <= u) 6 bound = Bound (fromInteger (natVal @n Proxy)) 7instance IsBound n (LowerBound l a) where 8 type BoundConstraint (LowerBound l a) n = (Num a, l <= n) 9 bound = LowerBound (fromInteger (natVal @n Proxy))

Some examples of using the bound function:

1> bound @5 :: Bound 2 6 Int 2Bound @2 @6 5 3> bound 2 :: LowerBound 0 Double 4LowerBound @0 2.0

We can’t make a Num instance for Bound or LowerBound types, because the operations could violate the bounds. For example, negate would produce a negative number, which is never within the bounds. So instead, we created special functions addB, plusB, and minusB that operate on Bound values, and truncate within the bounds. For LowerBound values, we created addLB, plusLB, and operators |+, |-, and |*. The subtraction operation on LowerBound needs to truncate, but the addition and multiplication operations don’t, because of the lack of an upper bound.

This work is similar to what you can do with the refined package. That package might be a good option for us, but it has one shortcoming: Although values can be checked at compile time, it’s only done via Template Haskell. For various reasons, we like to minimize our use of Template Haskell, so we prefer our approach using type-level Nats. Perhaps in the future we can add support for this method of checking to the refined package.

It’s common in production systems to expect numeric values to fall in a certain range. Haskell gives us the power to guarantee at compile time that these values are constrained. With our Bound/LowerBound types, we’re able to express both compile-time values that don’t need to be checked at runtime, and values that have been parsed at runtime and are guaranteed to be valid.