lue-bird/elm-bounded-nat

number in a typed range


Keywords
elm, natural-number, type-level, type-safe
License
MIT
Install
elm-package install lue-bird/elm-bounded-nat 28.0.0

Documentation

bounded-nat

Natural number ≥ 0 that has extra information about its range at compile-time

example: toHexChar

toHexChar : Int -> Char
  • the type doesn't show that an Int between 0 & 15 is expected
  • the one implementing toHexChar has to handle the cases where the argument isn't between 0 & 15
    • either by introducing Maybe which will be carried throughout your program
    • or by providing silent default error values like '?' or even worse '0'
  • the Int range promise of the argument is lost after the operation

with bounded-nat:

toHexChar : N (In min_ (Up maxTo15_ To N15)) -> Char
  • the type tells us that a number between 0 & 15 is wanted
  • the user proves that the number is actually between 0 & 15

The argument type says: Give me an integer ≥ 0 N In range

  • ≥ 0any minimum allowed → min_ type variable that's only used once
  • ≤ 15 → if we increase some number (maxTo15_ type variable that's only used once) by the argument's maximum, we get N15

Users can prove this by explicitly

  • using specific values

    red = rgbPercent { r = n100, g = n0, b = n0 }  --👍
    n7 |> N.subtract n1 |> N.divideBy n2 |> toHexChar --→ '3'
  • handling the possibility that a number isn't in the expected range

    toPositive : Int -> Maybe (N (Min (Up1 x_)))
    toPositive =
        N.intIsAtLeast n1 >> Result.toMaybe
  • clamping

    floatPercent float =
        float * 100 |> round |> N.intIn ( n0, n100 )
  • there are more ways, but you get the idea 🙂

example: toDigit

toDigit : Char -> Maybe Int

You might be able to do anything with this Int value, but you lost useful information:

  • can the result even be negative?
  • can the result even have multiple digits?
toDigit :
  Char
  -> Maybe (N (In (Up0 minX_) (Up9 maxX_)))

The type of an N value will reflect how much you and the compiler know

  • at least a minimum value? Min
  • between a minimum & maximum value? In

example: factorial

intFactorial : Int -> Int
intFactorial x =
    case x of
        0 ->
            1

        non0 ->
            non0 * intFactorial (non0 - 1)

This forms an infinite loop if we call intFactorial -1...

Let's disallow negative numbers here (& more)!

import N exposing (N, In, Min, Up1, n1, n4)

         -- for every `n ≥ 0`, `n! ≥ 1`
factorial : N (In min_ max_) -> N (Min (Up1 x_))
factorial =
    factorialBody

factorialBody : N (In min_ max_) -> N (Min (Up1 x_))
factorialBody x =
    case x |> N.isAtLeast n1 of
        Err _ ->
            n1 |> N.maxToInfinity
        Ok xMin1 ->
            -- xMin1 : N (Min ..1..), so xMin1 - 1 ≥ 0
            factorial (xMin1 |> N.subtractMin n1)
                |> N.multiplyBy xMin1

factorial n4 |> N.toInt --> 24
  • nobody can put a negative number in
  • we have an extra promise! every result is ≥ 1

Separate factorial & factorialBody are needed because there's no support for polymorphic recursion 😢

We can do even better! !19 is already > the maximum safe Int 2^53 - 1

safeFactorial : N (In min_ (Up maxTo18_ To N18)) -> N (Min (Up1 x_))
safeFactorial =
    factorial

No extra work

tips

  • keep as much type information as possible and drop it only where you need to: "Wrap early, unwrap late"

  • keep argument types as broad as possible

    like instead of

    charFromCode : N (Min min_) -> Char

    which you should never do, allow maximum-constrained numbers to fit as well:

    charFromCode : N (In min_ max_) -> Char

ready? go!

  • 👀 typesafe-array shows that
    • N (In ...) is very useful as an index
    • In, Min, Exactly can also describe a length