indique/elm-n-nat-type/5.0.1

elm-n-nat-type

How can you express numbers within a type?

This package enables you to do just that.

Let's look at how in an example: Implementing a NaturalNumber

module NaturalNumber exposing (NaturalNumber)

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

• Exact description.

  
  --we don't expose this constructor
  type NaturalNumber n
      = NaturalNumber Int
  
  one : NaturalNumber Nat1
  one =
      NaturalNumber 1
  
  two : NaturalNumber Nat2
  two =
      NaturalNumber 2
  
  ten : NaturalNumber Nat10
  ten =
      NaturalNumber 10
  
  takesOnlyExact1 : NaturalNumber Nat1

  • takesOnlyExact1 ten is a compile-time-error

• At least description.

  takesAtLeast2 : NaturalNumber (Nat2Plus maybeMore)

  • takesAtLeast2 one is a compile-time-error
  • takesAtLeast2 ten & takesAtLeast2 two work

This is already better then most Nat packages!

Say we now want to add an add & subtract function.

add1 : NaturalNumber n -> NaturalNumber (Nat1NatPlus n)
add1 naturalNumber =
    NaturalNumber (naturalNumber + 1)

add2 : NaturalNumber n -> NaturalNumber (Nat2NatPlus n)
add2 =
    add1 >> add1

subtract1 : NaturalNumber (Nat1Plus nMinus1) -> NaturalNumber nMinus1
subtract1 naturalNumber =
    NaturalNumber (naturalNumber - 1)

We have a typesafe subtract? That's neat.

You might also want a function, where one NaturalNat should be at least as big as another one.

unsafeInterval : NaturalNumber first -> NaturalNumber maybeMoreThanFirst -> Interval

We cannot promise that first DescribesADelta maybeMore Is maybeMoreThanFirst. Or can we?

→ Take a look at elm-n-type

This package, together with elm-n-type is the foundation of elm-n-nat, elm-nat-within, elm-n-array.

Take a closer look at those packages to see N.Nat.Type in action!

about a big limitation

Sadly, while experimenting with type aliases, I discovered that type aliases can only expand so much.

compilingGetsKilled : NaturalNumber (Nat100Plus N93)

If a type alias is not fully expanded after 192 tries, there seems to be a hard limit

• the compilation stops
• the elm-stuff can corrupt

This is really the factor holding this library down. 😞