Safe Haskell | None |
---|

This module is an internal GHC module. It declares the constants used in the implementation of type-level natural numbers. The programmer interface for workin with type-level naturals should be defined in a separate library.

- data Nat
- data Symbol
- data family Sing n
- class SingI a where
- class kparam ~ Kind => SingE kparam rep | kparam -> rep where
- class (SingI a, SingE (Kind :: k) rep) => SingRep a rep | a -> rep
- unsafeSingNat :: Integer -> Sing (n :: Nat)
- unsafeSingSymbol :: String -> Sing (n :: Symbol)
- type Kind = Any
- withSing :: SingI a => (Sing a -> b) -> b
- singThat :: SingRep a rep => (rep -> Bool) -> Maybe (Sing a)
- class m (<=) n
- type family m (<=?) n :: Bool
- type family m (+) n :: Nat
- type family m (*) n :: Nat
- type family m (^) n :: Nat
- isZero :: Sing n -> IsZero n
- data IsZero where
- isEven :: Sing n -> IsEven n
- data IsEven where

# Kinds

# Linking type and value level

The class `SingI`

provides a "smart" constructor for singleton types.
There are built-in instances for the singleton types corresponding
to type literals.

class kparam ~ Kind => SingE kparam rep | kparam -> rep whereSource

A class that converts singletons of a given kind into values of some representation type (i.e., we forget the extra information carried by the singletons, and convert them to ordinary values).

Note that `fromSing`

is overloaded based on the *kind* of the values
and not their type---all types of a given kind are processed by the
same instances.

class (SingI a, SingE (Kind :: k) rep) => SingRep a rep | a -> repSource

A convenience class, useful when we need to both introduce and eliminate a given singleton value. Users should never need to define instances of this classes.

unsafeSingNat :: Integer -> Sing (n :: Nat)Source

unsafeSingSymbol :: String -> Sing (n :: Symbol)Source

# Working with singletons

withSing :: SingI a => (Sing a -> b) -> bSource

A convenience function useful when we need to name a singleton value
multiple times. Without this function, each use of `sing`

could potentially
refer to a different singleton, and one has to use type signatures to
ensure that they are the same.

singThat :: SingRep a rep => (rep -> Bool) -> Maybe (Sing a)Source

A convenience function that names a singleton satisfying a certain
property. If the singleton does not satisfy the property, then the function
returns `Nothing`

. The property is expressed in terms of the underlying
representation of the singleton.