wiki:TypeNats/InductiveDefinitions

Version 10 (modified by diatchki, 2 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 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)