This is an alternative site for discovering Elm packages. You may be looking for the official Elm package site instead.
Synonyms for type-level natural-numbers in Elm
version 1.0.0
license BSD3
native-modules False
elm-version 0.17.1 <= v < 0.18.0
Tag 1.0.0
Committed At 2016-08-21 02:29:58 UTC
elm-lang/core 4.0.5 <= v < 5.0.0 4.0.5




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)