A bounded natural number (>= 0).

argument-only type

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


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


-- any, just >= 0
Nat range

value types

-- >= 4
Nat (Min Nat4)


-- 2 <= nat <= 12
Nat (In Nat2 (Nat12Plus a_))

storage types

Like what to store in the Model for example.

-- >= 4
Nat (Min Nat4)


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

n

An exact number. It's type enables adding/subtracting Nat... types.

nat3
    : Nat
        (N Nat3
            (Nat3Plus x_)
            (Is a To (Nat3Plus a))
            (Is b To (Nat3Plus b))
        )


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

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 In 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_))

Expect an exact number.

Only useful as an argument & storage type in combination with Arrs, not with Nats.

byte : Arr (Only Nat8) Bit -> Byte

→ A given Arr must have exactly 8 Bits.

type alias TicTacToeBoard =
    Arr
        (Only Nat3)
        (Arr (Only Nat3) TicTacToField)

→ A given Arr must have exactly 3 by 3 TicTacToeFields.

The most detailed description of an exact value.

InNat.add for example uses this knowledge to describe the number as differences between other type variables.

add :
    Nat
        (N
            added_
            atLeastAdded_
            (Is min To sumMin)
            (Is max To sumMax)
        )
    -> Nat (ArgIn min max ifN_)
    -> Nat (In sumMin sumMax)

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

add :
    Nat
        (N
            added_
            atLeastAdded_
            (Is min To sumMin)
            is_
        )
    -> Nat (ArgIn min max_ ifN_)
    -> Nat (Min sumMin)

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

N Nat5
    (Nat5Plus a_)
    (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.

ArgIn minimum maximum ifN_: An argument somewhere within a minimum & maximum.

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

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

percent : Nat (ArgIn min_ Nat100 ifN_) -> 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_ ifN_)

A number, at least 5:

Nat (ArgIn (Nat5Plus minMinus5_) max_ ifN_)

• max_ could be a maximum value if there is one

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

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.add nat1
                >> Nat.lowerMin nat0
        )
        (nat0 |> Nat.toMin)

If something like this isn't possible, MinNat.intAtLeast is the best way!

Nats from a first to last value.

Nat.range nat3 nat10
--> : List (Nat (In Nat3 (Nat10Plus a_)))


Nat.range nat3 atLeast10
--> : List (Nat (Min Nat3))

The resulting List always has >= 1 element.

With nats in typesafe-array the type even knows the length! Try it.

Generate a random Nat in a range.

Nat.random nat1 nat10
--> Random.Generator (Nat (In Nat1 (Nat10Plus a_)))

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

rejectOrAcceptUserInt :
    Int
    -> Result String (Nat (In Nat1 (Nat100Plus a_)))
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 : Maybe (Nat (Min Nat5))


1234 |> Nat.isIntAtLeast nat5
--> Just (Nat 1234) : Maybe (Nat (Min Nat5))

The greater of 2 Nats.

Nat.theGreater
    between1And3
    (atLeast4 |> Nat.lowerMin nat1)
--> : Nat (Min Nat1)

The smaller of 2 Nats.

Nat.theSmaller
    (nat3 |> Nat.toMin)
    (atLeast4 |> Nat.lowerMin nat3)
--> Nat 3 : Nat (Min Nat3)

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.

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

9 |> Nat.intAtLeast nat3
--> Nat 9 : Nat (Min Nat3)


0 |> Nat.intAtLeast nat3
--> Nat 3 : Nat (Min Nat3)

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.add nat1
                >> Nat.lowerMin nat0
        )
        (Nat.toMin nat0)

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

Create a Nat (In ...) by clamping an Int 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 : Nat (In Nat3 (Nat12Plus a_))

0 |> Nat.intInRange nat3 nat12
--> Nat 3 : Nat (In Nat3 (Nat12Plus a_))

99 |> Nat.intInRange nat3 nat12
--> Nat 12 : Nat (In Nat3 (Nat12Plus a_))

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

Cap the Nat to at most a number.

between5And15
    |> Nat.atMost nat10 { lowest = nat5 }
--> : Nat (In Nat5 (Nat10Plus a_))


atLeast5 |> Nat.atMost nat10 { lowest = nat5 }
--> : Nat (In Nat5 (Nat10Plus a_))

lowest can be a number <= the minimum.

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 dividing by a Nat >= 1. x |> remainderBy d is at most d

atMost7 |> Nat.remainderBy nat3
--> Nat 1 : Nat (In 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)

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
]

Convert it to a Nat (In min max).

Nat.toIn nat4
--> : Nat (In Nat4 (Nat4Plus a_))

Example

[ in3To10, nat3 ]

Elm complains:

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

[ in3To10
, nat3 |> Nat.toIn
]

Convert a Nat (ArgIn min ...) to a Nat (Min min).

between3And10 |> Nat.toMin
--> : Nat (Min Nat4)

There is only 1 situation you should use this.

To make these the same type.

[ atLeast1, between1And10 ]

Elm complains:

But all the previous elements in the list are: Nat (Min Nat1)

[ atLeast1
, between1And10 |> Nat.toMin
]

Make it fit into functions with require a higher maximum.

You should design type annotations as general as possible.

onlyAtMost18 : Nat (ArgIn min_ Nat18 ifN_)


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)