indique/elm-bounded-nat/5.0.0

elm-bounded-nat

Current attempts of represening natural numbers >= 0 only have quite lose promises.

• If you know that your Nat is >= 3, why can't you subtract 1 or 2 or 3?

This package contains many ways to ensure that a Nat is in a range at compile-time.

• Min knows the minimum possible value: ⨯[✓✓✓✓✓✓✓...
• In knows the range it's in: ⨯⨯[✓✓✓]⨯⨯...
• N & Only know the actual value: ⨯✓⨯⨯⨯⨯...

Setup

import Nat exposing (Nat)
import Nat.Bound exposing (..)
    --In, Min, Only, N, Difference, Is, To
import Nat.Min
import Nat.In
import Nat.N
import Nat.Ns exposing (..) --nat0 to nat192

import Nat.N.Type exposing (..)
    --Nat0 to Nat192 & Nat0Plus to Nat192Plus

2 examples

color

rgb : Float -> Float -> Float -> Color

This is common, but the one implementing the function has to handle the case where a value is not between 0 and 1.

rgbPer100 :
    Nat (In redMin Nat100)
    -> Nat (In greenMin Nat100)
    -> Nat.In (In blueMin Nat100)
    -> Color

Here, the one using this function must make sure to you that the numbers are actually between 0 and 100.

They can prove it by

• clamping

  grey float =
      let
          from0To100 =
              (float * 100) |> floor
                  |> Nat.In.intInRange nat0 nat100 --easy
      in
      rgbPer100 from0To100 from0To100 from0To100

• already knowing

  nat100
  -- of type Nat (N Nat100 ...)
  -- → We know the EXACT value
      |> Nat.N.toIn
      -- → it must also be in range 100 to 100 + ...
  red =
    rgbPer100 (nat100 |> Nat.N.toIn)
        (nat0 |> Nat.N.toIn) (nat0 |> Nat.N.toIn)
        -- 👍

• checking

  isUserIntANat : Int -> Maybe (Nat (Min Nat0))
  isUserIntANat =
      Nat.Min.isAtLeast nat0
          { equalOrGreater = Just
          , less = \_-> Nothing
          }

• There are more ways, but this is enough to understand the idea 🙂.

factorial

intFactorial : Int -> Int
intFactorial x =
    if x == 0 then
        1

    else
        x * intFactorial (x - 1)

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

Let's disallow negative numbers here!

factorial : Nat (Min min) -> Nat (Min Nat1)

Says: for every natural number n >= 0, n! >= 1.

factorialHelp =
    Nat.Min.isAtLeast (nat1 |> Nat.N.toIn)
        { min = nat0 } -- the minimum of the x
        { less = \_ -> Nat.N.toMin nat1 -- x < 1 ? → then 1
        , equalOrGreater = -- x >= 1 ?
            \oneOrGreater -> --we now know it is a Nat.Min Nat1
                oneOrGreater
                    |> Nat.Min.mul
                        (factorialHelp
                            (oneOrGreater |> Nat.Min.subN nat1)
                            -- so we can safely subtract 1 👍
                        )
        }

As the minimum is allowed to be anything >= 0:

factorial =
    Nat.Min.lowerMin (nat0 |> Nat.N.toIn)
        >> factorialHelp

→ factorial (nat4 |> Nat.N.toMin) --> Nat 24

→ There is no way to put a negative number in.

→ We have the extra promise, that every result is >= 1

We can do even better! We know that !19 is already bigger than the maximum safe Int 2^53 - 1.

safeFactorial : Nat (In min Nat18) -> Nat (Min Nat1)
safeFactorial =
    Nat.In.dropMax >> factorial

tips

• keep as much type information as possible and drop it only where you need to.

  squaresTo10 =
      Nat.In.range nat0 nat10
          --nats from 0 to 10
          |> List.map
              (Nat.Min.dropMax
                  --we can no longer compute the maximum
                  >> Nat.Min.toPower 2
                  --we can't compute the exact minimum
                  --but we know its at least Nat0
              )

• keep your function annotations as general as possibleInstead of accepting only values where you know the values exact

  rgb : Nat (N red Is (Difference inverseRed To Nat100)) --...

  accept values that are somewhere in a range.

  rgb : Nat (In redMin Nat100) --...

Take a look at elm-bounded-array to see a lot of this in action!