boundednat
Natural number ≥ 0 that has extra information about its range at compiletime
toHexChar
example: toHexChar : Int > Char
 the type doesn't show that an
Int
between 0 & 15 is expected 
the one implementing
toHexChar
has to handle the cases where the argument isn't between 0 & 15 either by introducing
Maybe
which will be carried throughout your program  or by providing silent default error values like
'?'
or even worse'0'
 either by introducing
 the
Int
range promise of the argument is lost after the operation
with boundednat
:
toHexChar : N (In min_ (Up maxTo15_ To N15)) > Char
 the type tells us that a number between 0 & 15 is wanted
 the user proves that the number is actually between 0 & 15
The argument type says: Give me an integer ≥ 0 N
In
range

≥ 0
→ any minimum allowed →min_
type variable that's only used once 
≤ 15
→ if we increase some number (maxTo15_
type variable that's only used once) by the argument's maximum, we getN15
Users can prove this by explicitly

using specific values
red = rgbPercent { r = n100, g = n0, b = n0 } 👍 n7 > N.subtract n1 > N.divideBy n2 > toHexChar → '3'

handling the possibility that a number isn't in the expected range
toPositive : Int > Maybe (N (Min (Up1 x_))) toPositive = N.intIsAtLeast n1 >> Result.toMaybe

clamping
floatPercent float = float * 100 > round > N.intIn ( n0, n100 )

there are more ways, but you get the idea
🙂
toDigit
example: 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 (N (In (Up0 minX_) (Up9 maxX_)))
The type of an N
value will reflect how much you and the compiler know
factorial
example: intFactorial : Int > Int
intFactorial x =
case x of
0 >
1
non0 >
non0 * intFactorial (non0  1)
This forms an infinite loop if we call intFactorial 1
...
Let's disallow negative numbers here (& more)!
import N exposing (N, In, Min, Up1, n1, n4)
 for every `n ≥ 0`, `n! ≥ 1`
factorial : N (In min_ max_) > N (Min (Up1 x_))
factorial =
factorialBody
factorialBody : N (In min_ max_) > N (Min (Up1 x_))
factorialBody x =
case x > N.isAtLeast n1 of
Err _ >
n1 > N.maxToInfinity
Ok xMin1 >
 xMin1 : N (Min ..1..), so xMin1  1 ≥ 0
factorial (xMin1 > N.subtractMin n1)
> N.multiplyBy xMin1
factorial n4 > N.toInt > 24
 nobody can put a negative number in
 we have an extra promise! every result is
≥ 1
Separate factorial
& factorialBody
are needed because there's no support for polymorphic recursion
We can do even better!
!19
is already >
the maximum safe Int
2^53  1
safeFactorial : N (In min_ (Up maxTo18_ To N18)) > N (Min (Up1 x_))
safeFactorial =
factorial
No extra work
tips

keep as much type information as possible and drop it only where you need to: "Wrap early, unwrap late"

keep argument types as broad as possible
like instead of
charFromCode : N (Min min_) > Char
which you should never do, allow maximumconstrained numbers to fit as well:
charFromCode : N (In min_ max_) > Char
ready? go!

👀 typesafearray
shows that
N (In ...)
is very useful as an index 
In
,Min
,Exactly
can also describe a length
