indique/elm-nat-in-range/1.0.0

elm-nat-in-range

Current attempts of represening natural numbers >= 0 only have quite lose promises.

• If you know that your Nat is >= 3, why can't you subtract 1 or 2 or 3?

MinNat & InNat ensure that a Nat is within a minimum (& maximum)!

• MinNat only knows what a nat at least is: ⨯[✓✓✓✓✓✓✓...
• InNat knows the range a nat is in: ⨯⨯[✓✓✓]⨯⨯...

A strict Nat type, where the actual value is present in the type is NNat.

Setup

elm install indique/elm-n-type
elm install indique/elm-n-nat-type
elm install indique/elm-n-nat
elm install indique/elm-nat-in-range

import MinNat exposing (MinNat)
import InNat exposing (InNat)
import NNat exposing (NNat)
import NNats exposing (..) --nat0 to nat192

import N.Type exposing (..)
import N.Nat.Type exposing (..)
    --Nat0 to Nat192 & Nat0Plus to Nat192Plus

2 examples

color

rgb : Float -> Float -> Float -> Color

This is common, but the one implementing the function has to handle the case where a value is not between 0 and 1.

rgbPer100 :
    InNat redMin Nat100
    -> InNat greenMin Nat100
    -> InNat blueMin Nat100
    -> Color

Here, the one using this function must make sure to you that the numbers are actually between 0 and 100.

They can prove it by

• clamping

  grey float =
      let
          from0To100 =
              (float * 100) |> floor
                  |> InNat.intInRange nat0 nat100 --easy
      in
      rgbPer100 from0To100 from0To100 from0To100

• already knowing

  nat100
  -- of type NNat Nat100
  -- → We know the EXACT value
      |> InNat.n
      -- → it must also be in range 100 to 100 + ...
  red =
    rgbPer100 (nat100 |> InNat.n)
        (nat0 |> InNat.n) (nat0 |> InNat.n)
        -- 👍

• checking

  isUserIntANat : Int -> Maybe (MinNat Nat0)
  isUserIntANat =
      MinNat.isAtLeast nat0
          { equalOrGreater = Just
          , less = \_-> Nothing
          }

• There are more ways, but this is enough to understand the idea 🙂.

factorial

intFactorial : Int -> Int
intFactorial x =
    if x == 0 then
        1

    else
        x * intFactorial (x - 1)

This forms an infinite loop if we call intFactorial -1...

Let's disallow negative numbers here!

natFactorial : MinNat Nat0 -> MinNat Nat1

Says: for every natural number n >= 0, n! >= 1.

natFactorial =
    MinNat.isAtLeast nat1
        { min = nat0 } -- the minimum of the x
        { less = \_ -> MinNat.n nat1 -- x < 1 ? → then 1
        , equalOrGreater = -- x >= 1 ?
            \oneOrGreater -> --we now know it is a MinNat Nat1
                oneOrGreater
                    |> MinNat.mul
                        (natFactorial
                            (oneOrGreater |> MinNat.subN nat1)
                            -- so we can safely subtract 1 👍
                        )
        }

As the minimum is allowed to be anything >= 0:

factorial : MinNat min -> MinNat Nat1
factorial =
    MinNat.lowerMin nat0 >> natFactorial

→ factorial (MinNat.n nat4) |> MinNat.toInt --> 24

→ There is no way to put a negative in.

We can do even better. We know that !19 is already bigger than the maximum safe Int 2^53 - 1.

safeFactorial : InNat min N18Nat -> MinNat Nat1
safeFactorial =
    MinNat.fromIn >> factorial

tips

• keep as much type information as possible and drop it only where you don't need it.

  squaresTo10 =
      InNat.range nat0 nat10
          --nats from 0 to 10
          |> List.map
              (MinNat.dropMax
                  --we can no longer compute the maximum
                  >> MinNat.toPower 2
                  --we can't compute the exact minimum
                  --but we know its at least Nat0
              )

• keep your function annotations as general as possibleInstead of accepting only values where you know the values exact

  rgb : NNat (N red Is (Difference inverseRed To Nat100)) --...

  accept values that are somewhere in a range.

  rgb : InNat redMin Nat100 --...

Take a look at elm-n-array to see InNat in action!