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

Just the exact number.

Only useful as a function argument type.

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

byte : Arr (Only maybeN Nat8) 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 also uses the knowledge that the number is exact 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)
    -> Nat (In 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
    (Nat5Plus more)
    (Is myAge To sistersAge)
    (Is mothersAge To fathersAge)

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

No special meaning.

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
⨯ [✓ ✓ ✓ ✓ ✓ ✓ ✓] ⨯ ⨯ ⨯...

To be used as a return type, not as a function argument.

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 & return 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 a 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 first to last, is the Int

• inRange

• greater than the last or

• less than the first?

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 of type Nat (ValueMin Nat5)


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

The remainder after division.

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

atMost7 |> Nat.remainderBy nat3
--> Nat 1 of type 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 of type Nat (ValueMin Nat5)


atLeast2 |> Nat.mul nat5
--> Nat 10 of type 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 of type 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.maxIs nat18 {- works :) -})

lowerMin is also handy in those situations.