| Safe Haskell | None |
|---|
GHC.TypeLits
Contents
Description
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
This is the *kind* of type-level natural numbers.
This is the *kind* of type-level symbols.
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.