bounded-nat

Type-safe natural numbers (>= 0) can ensure that a Nat is in a given range at compile-time.

toHexChar :
    Nat (ArgIn anyMinimum_ Nat15 _)
    -> Char

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

examples

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

import Nat exposing (Nat, Min, In, ArgIn)
import InNat
import MinNat
import Nats exposing (..)
    -- nat0-160, Nat0-160 & -Plus

import Typed

percent

percent : Float -> Length

is common.

the one implementing it has to handle the cases where a value is not between 0 and 1
the type doesn't tell us that a Float between 0 & 1 is wanted

with bounded-nat

percent :
    Nat (ArgIn min_ Nat100 ifN_)
    -> Length

the user it must prove that the numbers are actually between 0 and 100
the type tells us that a number 0 to 100 is wanted

The type

Nat (ArgIn min_ Nat100 ifN_)

is saying it wants:

an integer >= 0: Nat

in a range: ArgIn
- at least 0 → any minimum value: min_
- at most 100: Nat100
- which might be exact: ifN_

Use can prove this by

using exact values

twoThirds = percent nat67

red = rgbPercent nat100 nat0 nat0 -- 👍

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

toPositive : Int -> Maybe (Nat (Min Nat1))
toPositive =
    Nat.isIntAtLeast nat1

clamping

floatPercent float =
    Nat.intInRange nat0 nat100
        (float * 100 |> round)

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?
Can the result even have multiple digits?

toDigit : Char -> Maybe Digit

type alias Digit =
    Nat (In Nat0 Nat9)

The type of a value reflects how much you know.

between a minimum & maximum value: In
at least a minimum value: Min
exact value: N
- can describe the difference between 2 values → useful for adding/subtracting/...

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 (ArgIn min_ max_ ifN_) -> Nat (Min Nat1)
factorial =
    factorialBody

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

factorialBody : -- as in factorial
factorialBody =
    case x |> MinNat.isAtLeast nat1 { lowest = nat0 } of
        Nat.Below _ ->
            Nat.toMin nat1

        Nat.EqualOrGreater atLeast1 ->
            -- atLeast1 is a Nat (Min Nat1)
            Nat.mul atLeast1
                (factorial
                    (atLeast1 |> MinNat.sub nat1)
                    -- so we can subtract 1
                )

factorial nat4 --> Nat 24

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

→ We have the extra promise, that 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 : Nat (ArgIn min_ Nat18 ifN_) -> Nat (Min Nat1)
safeFactorial =
    factorial

No extra work.

tips

keep as much type information as possible and drop it only where you need to.
keep your function annotations as general as possible
Instead of accepting only exact values
```
percent :
    Nat (N p_ atLeast_ (Is to100_ To Nat100) is_)
    -> Length
```
accept values that are somewhere in a range.
```
percent : Nat (ArgIn min_ Nat100 ifN_) -> Length
```
ifN_ says that it can be exact anyway. Or instead of
```
charFromCode : Nat (Min min_) -> Char
```
which you should also never do, allow Nat (In min ...) with any max & Nat (N ...) to fit in as well!
```
charFromCode : Nat (ArgIn min_ max_ ifN_) -> Char
```

ready? go!

Take a look at typesafe-array to see a lot of this in action!
You get to know that
- a Nat (ArgIn ...) is very useful as an index
- In, Min, Only can also describe the array length

lue-bird/elm-bounded-nat/19.0.1