Version 8 (modified by diatchki, 5 years ago) (diff)


There is a new kind, Nat. It is completely separate from GHC's hierarchy of sub-kinds, so Nat is only a sub-kind of itself.

The inhabitants of Nat are an infinite family of (empty) types, corresponding to the natural numbers:

0, 1, 2, ... :: Nat

These types are linked to the value world by a small library with the following API:

module GHC.TypeNats where

Singleton Types

We relate type-level natural numbers to run-time values via a family of singleton types:

data Nat (n :: Nat)

nat          :: NatI n => Nat n
natToInteger :: Nat n -> Integer

The only "interesting" value of type Nat n is the number n. Technically, there is also an undefined element.

One may think of the smart constructor nat as being a method of a special built-in class:

class NatI n where
  nat :: Nat n

instance NatI 0 where nat = "singleton 0 value"
instance NatI 1 where nat = "singleton 1 value"
instance NatI 2 where nat = "singleton 2 value"

Type-Level Operations

type family m ^ n :: Nat
type family m * n :: Nat
type family m + n :: Nat
class m <= n

Natural Numbers

data Natural = forall n . Natural !(Nat n)

data NaturalInteger
  = Negative Natural
  | NonNegative Natural

toNaturalInteger :: Integer -> NaturalInteger

subNatural :: Natural -> Natural -> NaturalInteger