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
Linking type and value level
SingI provides a "smart" constructor for singleton types.
There are built-in instances for the singleton types corresponding
to type literals.
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).
fromSing is overloaded based on the kind of the values
and not their type---all types of a given kind are processed by the
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.
Working with singletons
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.
A convenience function that names a singleton satisfying a certain
property. If the singleton does not satisfy the property, then the function
Nothing. The property is expressed in terms of the underlying
representation of the singleton.