A bounded natural number (>= 0).

value / return types

-- >= 4
Nat (Min Nat4)


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


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

function argument types

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


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


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


-- any, just >= 0
Nat range

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

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

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

percent : Nat (ArgIn 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 (ArgIn min max maybeN)

A number, at least 5:

Nat (ArgIn (Nat5Plus minMinus5) max maybeN)

• max could be a maximum value if there is one

• maybeN could contain extra information if the argument is a Nat (N ...)

Expect an exact number.

Only useful as an argument / storage type.

Every ArgIn NatXYZ (NatXYZPlus a) maybeN is a ArgOnly NatXYZ maybeN.

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

→ A given Arr must have exact 8 Bits.

ArgOnly 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
        (ArgN
            added
            (Is min To sumMin)
            (Is max To sumMax)
        )
    -> Nat (ArgIn min max maybeN)
    -> Nat (In sumMin sumMax)

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

addN :
    Nat (ArgN added (Is min To sumMin) x)
    -> Nat (ArgIn min max maybeN)
    -> Nat (Min 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 (In Nat0 ??)

This is where to use Min.

abs : Int -> Nat (Min Nat0)

A number >= 5 for example:

Nat (Min Nat5)

Every Min min is of type ArgIn min ....

In 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 (In Nat3 (Nat5Plus a))

The most detailed description of an exact value.

Don't use this as a function argument.

Just the exact number.

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

→ A given Arr must have exactly n elements.

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

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

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 (In ...)s from a first to last value.

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


from3ToAtLeast10 : List (Nat (Min 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 (In ...) in a range.

A Nat (Min ...) 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
        )
        (MinNat.value nat0)

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

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

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

9 |> Nat.intInRange nat3 nat12 --> Nat 9

0 |> Nat.intInRange nat3 nat12 --> Nat 3

99 |> Nat.intInRange nat3 nat12 --> 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

• AboveRange: greater than the upper bound or

• BelowRange: less than the lower bound?

rejectOrAcceptUserInt int =
    case int |> Nat.isIntInRange nat1 nat100 of
        InRange inRange ->
            Ok inRange

        BelowRange () ->
            Err "must be >= 1"

        AboveRange _ ->
            Err "must be <= 100"


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

If the Int >= a minimum, Just the Nat (Min 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 result of comparing a Nat to another Nat.

• EqualOrLess: <= that Nat

• Above: > that Nat

Values exist for each condition.

The result of comparing a Nat to another Nat.

• EqualOrGreater: >= that Nat

• Below: < that Nat

Values exist for each condition.

The result of comparing a Nat to a range from a lower to an upper bound.

• InRange

• AboveRange: greater than the upper bound

• BelowRange: less than the lower bound?

Values exist for each condition.

The result of comparing a Nat to another Nat.

• Equal to that Nat

• Less than that Nat

• Greater than that Nat

Values exist for each condition.

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

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


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

The remainder after division.

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

atMost7 |> Nat.remainderBy nat3
--> Nat 1 : Nat (ArgIn Nat0 (Nat3Plus a))

In theory, x % d should be at most d - 1, but this can't be expressed well by the type.

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

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


atLeast2 |> Nat.mul nat5
--> Nat 10 : Nat (Min 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 (In Nat0 (Nat7Plus a))

Set the minimum lower.

[ atLeast3, atLeast4 ]

Elm complains:

But all the previous elements in the list are: Nat (Min 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 (ArgIn 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.