lue-bird/elm-bounded-nat/21.0.0

bounded-nat

A 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 anyMinimum_ N15 difference_) -> 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

• ≥ 0; anyMinimum_ value allowed
• ≤ N15
• which might be a specific value like n0, n1, ... which has a difference_ )

Users can prove this by explicitly

• using exact values

  toHexChar n2 --→ 'c'
  red = rgbPercent { r = n100, g = n0, b = n0 }  --👍

• handling the possibility that a number isn't in the expected range

  toPositive : Int -> Maybe (N (Min N1))
  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 N0 (Add9 a_) {}))

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
• a specific value? N (In ... (Is ...))
  • allows precise adding, subtracting, ...

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)!

factorial : N (In min_ max_ difference_) -> N (Min N1)
factorial =
    factorialBody

Says: For every n ≥ 0, n! ≥ 1.

factorialBody : N (In min_ max_ difference_) -> N (Min N1)
factorialBody x =
    case x |> N.isAtLeast n1 of
        Err _ ->
            n1 |> N.noMax

        Ok n1AtLeast ->
            -- n1AtLeast : N (Min N1)
            -- so subtracting 1, we're still ≥ 0
            factorial (n1AtLeast |> N.minSub n1)
                |> N.mul n1AtLeast

factorial n4 |> N.toInt --→ 24

→ You can't put a negative number in

→ We have an extra promise! every result is ≥ 1

Sadly, we need separate factorial & factorialBody because there's no support for polymorphic recursion.

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

safeFactorial : N (In min_ N18 difference_) -> N (Min N1)
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"

  • elm-radio
  • elm-patterns

• keep argument types as broad as possible

  Instead of accepting only n0, n1, ... values in a range

  percent :
      N (In p_ atLeast_ (Is (Diff to100_ To N100) diff1_))
      -> Length

  accept values that are somewhere in a range.

  percent : N (In min_ N100 difference_) -> Length

  difference_ says that it can be exact anyway.

  Or instead of

  charFromCode : N (Min min_) -> Char

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

  charFromCode : N (In min_ max_ difference_) -> Char

ready? go!

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