Copyright | Copyright (c) 2014 Kenneth Foner |
---|---|

Maintainer | kenneth.foner@gmail.com |

Stability | experimental |

Portability | non-portable |

Safe Haskell | Safe-Inferred |

Language | Haskell2010 |

This module defines GADT type witnesses for Peano-style natural numbers.

- data Zero
- data Succ n
- data Natural n where
- class ReifyNatural n where
- reifyNatural :: Natural n

- type family LessThanOrEqual a b
- type (<=) a b = LessThanOrEqual a b ~ True
- type family LessThan a b
- type (<) a b = LessThan a b ~ True
- type family x + y
- type family x - y
- plus :: Natural a -> Natural b -> Natural (a + b)
- minus :: b <= a => Natural a -> Natural b -> Natural (a - b)

# Documentation

ReifyNatural n => ReifyNatural (Succ n) |

Natural numbers paired with type-level natural numbers. These terms act as witnesses of a particular natural.

class ReifyNatural n where Source

Given a context expecting a particular natural, we can manufacture it from the aether.

reifyNatural :: Natural n Source

ReifyNatural Zero | |

ReifyNatural n => ReifyNatural (Succ n) |

type family LessThanOrEqual a b Source

Type level less-than-or-equal test.

LessThanOrEqual Zero Zero = True | |

LessThanOrEqual Zero (Succ m) = True | |

LessThanOrEqual (Succ n) (Succ m) = LessThanOrEqual n m | |

LessThanOrEqual x y = False |

type (<=) a b = LessThanOrEqual a b ~ True Source

This constraint is a more succinct way of requiring that `a`

be less than or equal to `b`

.

type (<) a b = LessThan a b ~ True Source

This constraint is a more succinct way of requiring that `a`

be less than `b`

.