elmboundednat
Typesafe natural numbers (>= 0
), ensuring that a Nat
is in a range at compiletime:
toHexChar : Nat (In min Nat15 maybeN) > Char
No number below 0 or above 15 can be passed in as an argument!
Setup
import Nat exposing (Nat)
import Nat.Bound exposing (..)
In, Only, N, Is, To, ValueIn, ValueOnly, ValueMin, ValueN
import TypeNats exposing (..)
Nat0 to Nat160 & Nat0Plus to Nat60Plus
import NNats exposing (..) nat0 to nat160
import NNat
import InNat
import MinNat
example: 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
🙂
example: 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
example: 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 > Nat.toMin
, 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 elmboundedarray
to see a lot of this in action!
You get to know that
 a
Nat (In ...)
is very useful as an index 
Nat.Bound
s can describe amounts well