elm-bounded-nat

Type-safe natural numbers (>= 0), ensuring that a Nat is in a range at compile-time:

toHexChar : Nat (In min Nat15 maybeN) -> Char

No number below 0 or above 15 can be passed in as an argument!

examples

elm install lue-bird/elm-bounded-nat
elm install lue-bird/elm-typed-value

import Nat exposing
    ( Nat, In, Only, N, Is, To
    , ValueIn, ValueOnly, ValueMin, ValueN
    )
import NNats exposing (..)
    -- nat0 to nat160
import InNat
import MinNat

import TypeNats exposing (..)
    -- Nat0 to Nat160 & Nat1Plus to Nat160Plus

-- from elm-typed-value
import Typed exposing (val, val2)

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
• the type doesn't tell us that only a Float between 0 & 1 is needed

rgbPer100 :
    Nat (In redMin Nat100 redMaybeN)
    -> Nat (In greenMin Nat100 greenMaybeN)
    -> Nat (In blueMin Nat100 blueMaybeN)
    -> Color

• the one using this function must make sure to you that the numbers are actually between 0 and 100
• you clearly know what input is desired

The type

Nat (In min Nat100 maybeN)

is saying it wants:

an integer >= 0                  Nat          
  in a range                        In       
    at least any minimum value        min   
    at most 100                       Nat100
    which might be exact              maybeN

They can prove it by

• already knowing

-- the type is Nat (ValueN Nat100 ...)
-- so it's also between 100 and 100 (101 / 102 /...)
nat100

red =
    rgbPer100 nat100 nat0 nat0
    -- 👍

• checking

isUserIntANat : Int -> Maybe (Nat (ValueMin Nat0))
isUserIntANat =
    Nat.isIntAtLeast nat0

• clamping

grey float =
    let
        greyLevel =
            float
                * 100
                |> round
                |> Nat.intInRange nat0 nat100
    in
    rgbPer100 greyLevel greyLevel greyLevel

• There are more ways, but you get the idea 🙂

digit

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?
• Could the number have multiple digits?

toDigit : Char -> Maybe Digit

type alias Digit =
    Nat (ValueIn Nat0 Nat9)

The type of a value reflects how much you know.

• ValueIn: between a minimum & maximum value
• ValueMin: at least a minimum value
• ValueN: exact value
  • also describes the difference between 2 values

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 (In min max maybeN) -> Nat (ValueMin Nat1)

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

factorialHelp =
    MinNat.isAtLeast nat1
        { min = nat0 } -- the minimum of the x
        { less =
            -- x < 1 ? → then 1
            \_ -> nat1 |> MinNat.value
        , equalOrGreater =
            \atLeast1 ->
                -- a Nat (ValueMin Nat1)
                atLeast1
                    |> Nat.mul
                        (factorial
                            (atLeast1 |> MinNat.subN nat1)
                            -- we can subtract 1 👍
                        )
        }

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

factorial =
    Nat.lowerMin nat0
        >> factorialHelp

→ factorial nat4 --> 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 maybeN) -> Nat (ValueMin Nat1)
safeFactorial =
    factorial

No extra work.

tips

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

squares2To10 =
    -- every Nat is ValueIn Nat2 (Nat10Plus a)
    Nat.range nat2 nat10
        |> List.map
            (Nat.toPower nat2
            -- we can't compute the exact minimum & maximum
            -- but we know it's at least Nat2
            )

• keep your function annotations as general as possible

Instead of accepting only exact values

rgb : Nat (ValueN red (Is redTo100 To Nat100) x) -> --...

accept values that are somewhere in a range.

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

maybeN says that it can be exact anyway. Or instead of

charFromCode : Nat (ValueMin min) -> Char

which you should also never do, allow Nat (In min ...) with any max & Nat (ValueN ...) to fit in as well!

charFromCode : Nat (In min max maybeN) -> Char

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

You get to know that

• a Nat (In ...) is very useful as an index
• Nat.Bounds can describe amounts well