Copyright | (C) 2014 Richard Eisenberg |
---|---|

License | BSD-style (see LICENSE) |

Maintainer | Richard Eisenberg (eir@cis.upenn.edu) |

Stability | experimental |

Portability | non-portable |

Safe Haskell | None |

Language | Haskell2010 |

Defines and exports singletons useful for the Nat and Symbol kinds.

- data Nat
- data Symbol
- type SNat x = Sing x
- type SSymbol x = Sing x
- withKnownNat :: Sing n -> (KnownNat n => r) -> r
- withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r
- type family Error str :: k
- sError :: Sing (str :: Symbol) -> a
- class KnownNat n
- natVal :: KnownNat n => proxy n -> Integer
- class KnownSymbol n
- symbolVal :: KnownSymbol n => proxy n -> String

# Documentation

data Nat

(Kind) This is the kind of type-level natural numbers.

data Symbol

(Kind) This is the kind of type-level symbols.

withKnownNat :: Sing n -> (KnownNat n => r) -> r Source

Given a singleton for `Nat`

, call something requiring a
`KnownNat`

instance.

withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r Source

Given a singleton for `Symbol`

, call something requiring
a `KnownSymbol`

instance.

class KnownNat n

This class gives the integer associated with a type-level natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.

*Since: 4.7.0.0*

class KnownSymbol n

This class gives the integer associated with a type-level symbol. There are instances of the class for every concrete literal: "hello", etc.

*Since: 4.7.0.0*

symbolVal :: KnownSymbol n => proxy n -> String

*Since: 4.7.0.0*