... | @@ -13,19 +13,38 @@ These types are linked to the value world by a small library with the following |
... | @@ -13,19 +13,38 @@ These types are linked to the value world by a small library with the following |
|
|
|
|
|
```wiki
|
|
```wiki
|
|
module GHC.TypeNats where
|
|
module GHC.TypeNats where
|
|
|
|
```
|
|
|
|
|
|
data Nat (n :: Nat) -- Abstract "singleton" types.
|
|
## Basic Operations
|
|
|
|
|
|
natToInteger :: Nat n -> Integer -- Convert a singleton to an integer.
|
|
```wiki
|
|
integerToNat :: Integer -> (forall n. Nat n -> a) -> a -- Convert an integer into a singleton.
|
|
data Nat n
|
|
|
|
|
|
class TypeNat n where
|
|
class TypeNat n where
|
|
nat :: Nat n -- A value in a "singleton" type.
|
|
nat :: Nat n
|
|
|
|
|
|
|
|
natToInteger :: Nat n -> Integer
|
|
|
|
```
|
|
|
|
|
|
|
|
## Type-Level Operations
|
|
|
|
|
|
|
|
```wiki
|
|
|
|
type family m ^ n :: Nat
|
|
|
|
type family m * n :: Nat
|
|
|
|
type family m + n :: Nat
|
|
|
|
class m <= n
|
|
|
|
```
|
|
|
|
|
|
|
|
## Natural Numbers
|
|
|
|
|
|
|
|
```wiki
|
|
|
|
data Natural = forall n . Natural !(Nat n)
|
|
|
|
|
|
|
|
data NaturalInteger
|
|
|
|
= Negative Natural
|
|
|
|
| NonNegative Natural
|
|
|
|
|
|
instance TypeNat 0
|
|
toNaturalInteger :: Integer -> NaturalInteger
|
|
instance TypeNat 1
|
|
|
|
instance TypeNat 2
|
|
|
|
...
|
|
|
|
|
|
|
|
-- property: natToInteger (nat :: Nat n) == n
|
|
subNatural :: Natural -> Natural -> NaturalInteger
|
|
``` |
|
``` |
|
|
|
\ No newline at end of file |