Helpers for type-level natural-numbers in Elm.
These are useful when describing things like multi-dimensional arrays or lists of fixed length, ensuring that a certain number of elements exist.
These aren't very useful on their own, but you can use them as tags to provide a type-safe API for an underlying function that is safe, but can't be proven safe by the compiler.
See the safelist library for an example of this.
Was formerly elm-typenats, but changed to meet the new naming guidelines.
Example: integers whose values are stored in the type
import TypeNat exposing (Zero, OnePlus)
-- Our parameterized by a type-level number
-- Usually you won't want to export the constructor,
-- so you can restrict the types of values we create
type SingleInt n = SingleInt Int
-- We make fake-constructors for our parameterized type
-- This allows us to ensure the values match the type
singleZero : SingleInt Zero
singleZero = SingleInt 0
singleOnePlus : SingleInt n -> SingleInt (OnePlus n)
singleOnePlus (SingleInt n) = SingleInt (n+1)