indique/elm-n-nat-type/3.0.0

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 Nat.Type exposing (..)

• Exact description.

  
  --we don't expose this constructor
  type NaturalNumber n
      = NaturalNumber Int
  
  one : NaturalNumber N1Nat
  one =
      NaturalNumber 1
  
  two : NaturalNumber N2Nat
  two =
      NaturalNumber 2
  
  ten : NaturalNumber N10Nat
  ten =
      NaturalNumber 10
  
  takesOnlyExact1 : NaturalNumber N1Nat

  • takesOnlyExact1 ten is a compile-time-error

• At least description.

  takesAtLeast2 : NaturalNumber (N2NatPlus 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 (N1NatPlus n)
add1 naturalNumber =
    NaturalNumber (naturalNumber + 1)

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

subtract1 : NaturalNumber (N1Plus 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.

compilingProcessGetsKilled
    : NaturalNumber (N192NatPlus N1Nat)

If a type alias is not fully expanded after 192 tries, there seems to be a hard limit and the compilation stops.

This is really the factor holding this library down. 😞