indique/elm-bounded-nat 7.0.1

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

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 🙂.

digit

toDigit : Char -> Maybe Int

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

How can this be negative?
How can this have multiple digits?

toDigit : Char -> Maybe Digit

type alias Digit =
    Nat (In Nat0 Nat9)

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!

indique/elm-bounded-nat/7.0.1