Singletons and induction schemes over GHC.TypeLits.Nat.
While the TypeLits interface provided by GHC does allow case-analysing the
values of the naturals (GHC.TypeLits.natVal), it does not facilitate writing
type-safe programs involving that AP, if one were to write:
case natVal (x :: Proxy n) of 0 -> foo x
In the RHS of this pattern match n is equal to 0 but this isn't something
GHC can reason about, as this is an ordinary pattern match on an Integer.
If the type of foo was Proxy 0 -> ... this wouldn't typecheck and one
would have to resort to unsafeCoerce. In order to make GHC infer something
like this, natVal needs to return a GADT that includes proofs about the
natural number it refers to, such that when pattern matching on that GADT the
proofs become available to the typechecker.
This package provides a handful of variants of such GADTs for overcoming this
type of issue, as well as functions to do typesafe induction on naturals
without resorting to manual GADT unpacking. The most basic form of induction -
Peano-style induction (P(0) and P(n) implies P(n + 1)) can be inefficient in
practice on large numbers, so this package also provides more efficient binary
and arbitrary-base induction schemes.
