A bounded natural number (>= 0).

value / return types

-- >= 4
Nat (ValueMin Nat4)


-- 2 <= nat <= 12
Nat (ValueIn Nat2 Nat12)


-- = 3, & 3, described as a difference
Nat
    (ValueN Nat3
        (Nat3Plus more)
        (Is a To (Nat3Plus a))
        (Is b To (Nat3Plus b))
    )

function argument types

-- >= 4
Nat (In (Nat4Plus minMinus4) max maybeN)


-- 4 <= nat <= 15
Nat (In (Nat4Plus minMinus4) Nat15 maybeN)


-- An exact number nTo15 away from 15
Nat (N n (Is nTo15 To Nat15) x)


-- any, just >= 0
Nat range

In minimum maximum maybeN: Somewhere within a minimum & maximum.

   ↓ minimum   ↓ maximum
⨯ [✓ ✓ ✓ ✓ ✓ ✓ ✓] ⨯ ⨯ ⨯...

Note: maximum >= minimum for every existing Nat (In min max ...):

percent : Nat (In min Nat100 maybeN) -> Percent

→ min <= Nat100

If you want a number where you just care about the minimum, leave the max as a type variable.

   ↓ minimum    ↓ maximum or  →
⨯ [✓ ✓ ✓ ✓ ✓ ✓ ✓...

Any natural number:

Nat (In min max maybeN)

A number, at least 5:

Nat (In (Nat5Plus minMinus5) max maybeN)

• max could be a maximum value if there is one

• maybeN could contain extra information for N ... if the number was exact

Expect an exact number.

Only useful as an argument / storage type.

Every In NatXYZ (NatXYZPlus a) maybeN is a Only NatXYZ maybeN.

byte : Arr (Only Nat8 maybeN) Bit -> Byte

→ A given Arr must have exact 8 Bits.

Only is useful for Arrs, but you will never need it in combination with Nats.

Expect an exact value. InNat.addN for example uses this knowledg to describe the number as differences between other type variables.

addN :
    Nat
        (N
            added
            (Is min To sumMin)
            (Is max To sumMax)
        )
    -> Nat (In min max maybeN)
    -> Nat (ValueIn sumMin sumMax)

You can just ignore the second difference if you don't need it (MinNat.addN).

addN :
    Nat (N added (Is min To sumMin) x)
    -> Nat (In min max maybeN)
    -> Nat (ValueMin sumMin)

Is a To b: an exact value as the diffference b - a.

N Nat5
    (Is myAge To sistersAge)
    (Is mothersAge To fathersAge)

• myAge + 5 = sistersAge
• mothersAge + 5 = fathersAge

Only at type-level in Is.

Is a To b

→ distance b - a.

Only value / return types should be Min.

Sometimes, you simply cannot compute a maximum.

abs : Int -> Nat (ValueIn Nat0 ??)

This is where to use Min.

abs : Int -> Nat (Min Nat0)

A number, which is at least 5 is be of type

Nat (ValueMin Nat5)

Every ValueMin min is of type In min ....

ValueIn minimum maximum: A value somewhere within a minimum & maximum. We don't know the exact value, though.

   ↓ minimum   ↓ maximum
⨯ [✓ ✓ ✓ ✓ ✓ ✓ ✓] ⨯ ⨯ ⨯...

Do not use it as an argument type.

A number between 3 and 5

Nat (ValueIn Nat3 (Nat5Plus a))

The most detailed description of an exact value.

Don't use this as a function argument.

Just the exact number.

Only useful as a value type.

repeatOnly :
    Nat (Only n maybeN)
    -> element
    -> Arr (ValueOnly n) element

→ A given Arr must has exactly n elements.

ValueOnly is useful for Arrs, but you will never need it in combination with Nats.

The absolute value of an Int, which is >= Nat0.

Nat.abs 16 --> Nat 16


Nat.abs -4 --> Nat 4

Really only use this if you want the absolute value.

badLength list =
    List.length >> Nat.abs


goodLength =
    List.foldl
        (\_ ->
            MinNat.addN nat1
                >> Nat.lowerMin nat0
        )
        (nat0 |> MinNat.value)

If something like this isn't possible, use MinNat.intAtLeast!

Nat (ValueIn ...)s from a first to last value.

from3To10 : List (Nat (ValueIn Nat3 (Nat10Plus a)))
from3To10 =
    Nat.range nat3 nat10


from3ToAtLeast10 : List (Nat (ValueMin Nat3))
from3ToAtLeast10 =
    Nat.range nat3 atLeast10

The resulting List always has at least 1 element.

With Arr.range the type even knows the length! Try it.

Generate a random Nat (ValueIn ...) in a range.

A Nat (ValueMin ...) from an Int; if the Int < minimum, minimum is returned.

9 |> Nat.intAtLeast nat3
--> Nat 9


0 |> Nat.intAtLeast nat3
--> Nat 3

You can also use this if you know an Int must be at least minimum.

But avoid it if you can do better, like

goodLength =
    List.foldl
        (\_ ->
            MinNat.addN nat1
                >> Nat.lowerMin nat0
        )
        (nat0 |> MinNat.value)

If you want to handle the case < minimum yourself, use Nat.isIntAtLeast.

A Nat (ValueIn ...) from an Int, clamped between a minimum & maximum.

• if the Int < minimum, minimum is returned
• if the Int > maximum, maximum is returned

clampBetween3And12 =
    Nat.intInRange nat3 nat12

9 |> clampBetween3And12 --> Nat 9

0 |> clampBetween3And12 --> Nat 3

99 |> clampBetween3And12 --> Nat 12

If you want to handle the cases < minimum & > maximum explicitly, use isIntInRange.

Compared to a range from a lower to an upper bound, is the Int

• inRange

• greater than the upper bound or

• less than the lower bound?

rejectOrAcceptUserInt =
    Nat.isIntInRange nat1 nat100
        { less = Err "must be >= 1"
        , greater = \_-> Err "must be <= 100"
        , inRange = Ok
        }

rejectOrAcceptUserInt 0
--> Err "must be >= 1"

If the Int >= a minimum, Just the Nat (ValueMin minimum), else Nothing.

4 |> Nat.isIntAtLeast nat5 --> Nothing


1234 |> Nat.isIntAtLeast nat5 --> Just (Nat 1234)

The greater of 2 Nats.

Nat.theGreater between1And3 (nat4 |> Nat.lowerMin nat1)
--> Nat 4

The smaller of 2 Nats.

Nat.theSmaller nat3 (nat4 |> Nat.lowerMin nat3)
--> Nat 3

The Nat ^ a Nat >= 1. We know that if a >= 1 → x ^ a >= x

atLeast5 |> Nat.toPower nat2
--> Nat 25 : Nat (ValueMin Nat5)


atLeast2 |> Nat.toPower nat5
--> Nat 25 : Nat (ValueMin Nat2)

The remainder after division.

• % 0 is impossible
• x % d is at most x

atMost7 |> Nat.remainderBy nat3
--> Nat 1 : Nat (In Nat0 (Nat7Plus a))

Multiply by a Nat >= 1. we know that if a >= 1, x * a >= x.

atLeast5  |> Nat.mul nat2
--> Nat 10 : Nat (ValueMin Nat5)


atLeast2 |> Nat.mul nat5
--> Nat 10 : Nat (ValueMin Nat2)

The maximum value of both factors can be Infinity.

Divide (//) by a Nat >= 1.

• / 0 is impossible

• x / d is at most x

atMost7
    |> Nat.div nat3
--> Nat 2 : Nat (ValueIn Nat0 (Nat7Plus a))

Set the minimum lower.

[ atLeast3, atLeast4 ]

Elm complains:

But all the previous elements in the list are: Nat (ValueMin Nat3)

[ atLeast3
, atLeast4 |> Nat.lowerMin nat3
]

Make it fit into functions with require a higher maximum.

You should design type annotations as general as possible.

onlyAtMost18 : Nat (In min Nat18 maybeN)


onlyAtMost18 between3And8 --fine

But once you implement onlyAtMost18, you might use the value in onlyAtMost19.

onlyAtMost18 value =
    -- onlyAtMost19 value --error :(
    onlyAtMost19
        (value |> Nat.restoreMax nat18 {- works :) -})

lowerMin is also handy in those situations.