Version 12 (modified by diatchki, 3 years ago) (diff) |
---|

The module `GHC.TypeLits` provides two views on values of type `TNat`,
which make it possible to define inductive functions using `TNat` values.

## Checking for Zero (Unary Strucutre of Nat)

The first view provides the same functionality as the usual
Peano arithmetic definition of the natural numbers. It
is useful when using `TNat` to count something.

isZero :: TNat n -> IsZero n data IsZero :: Nat -> * where IsZero :: IsZero 0 IsSucc :: !(TNat n) -> IsZero (n + 1)

By using `isZero` we can check if a number is 0 or the successor
of another number. The interesting aspect of `isZero` is that
the result is typed: if `isZero x` returns `IsSucc y`,
then the type checker knows that the type of `y` is one smaller
than `x`.

## Checking for Evenness (Binary Structure of Nat)

The other view provides a more "bit-oriented" view of
the natural numbers, by allowing us to check if the least
significant bit of a number is 0 or 1. It is useful
when we use `TNat` values for splitting things
in half:

isEven :: TNat n -> IsEven n data IsEven a :: Nat -> * where IsEvenZero :: IsEven 0 IsEven :: !(TNat (n + 1)) -> IsEven (2 * (n + 1)) IsOdd :: !(TNat n) -> IsEven ((2 * n) + 1)