Version 9 (modified by diatchki, 6 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 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 then `x`.

## Checking for Evenness (Binary Structure of Nat)

The other view provides a more "bit-oriented" view of the natural numbers, by allowing is 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)
```