| 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 working 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 ~ KindParam => SingE kparam where
- class (SingI a, SingE (KindOf a)) => SingRep a
- singByProxy :: SingI n => proxy n -> Sing n
- data SomeSing where
- class kp ~ KindParam => ToSing kp where
- type SomeNat = SomeSing (KindParam :: KindIs Nat)
- type SomeSymbol = SomeSing (KindParam :: KindIs Symbol)
- withSing :: SingI a => (Sing a -> b) -> b
- singThat :: SingRep a => (Demote a -> Bool) -> Maybe (Sing a)
- class (m <=? n) ~ True => m (<=) n
- type family m (<=?) n :: Bool
- type family m (+) n :: Nat
- type family m (*) n :: Nat
- type family m (^) n :: Nat
- type family m (-) n :: Nat
- data :~: where
- eqSingNat :: Sing (m :: Nat) -> Sing (n :: Nat) -> Maybe (m :~: n)
- eqSingSym :: Sing (m :: Symbol) -> Sing (n :: Symbol) -> Maybe (m :~: n)
- isZero :: Sing n -> IsZero n
- data IsZero where
- data Nat1
- type family FromNat1 n :: Nat
- data KindIs a = KindParam
- type Demote a = DemoteRep (KindOf a)
- type KindOf a = (KindParam :: KindIs k)
Kinds
(Kind) This is the kind of type-level natural numbers.
(Kind) 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 ~ KindParam => SingE kparam 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 (KindOf a)) => SingRep a Source
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.
singByProxy :: SingI n => proxy n -> Sing nSource
A convenience function to create a singleton value, when we have a proxy argument in scope.
type SomeNat = SomeSing (KindParam :: KindIs Nat)Source
A definition of natural numbers in terms of singletons.
type SomeSymbol = SomeSing (KindParam :: KindIs Symbol)Source
A definition of strings in terms of singletons.
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 => (Demote a -> 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.
Functions on type nats
type family m (-) n :: NatSource
Subtraction of type-level naturals. Note that this operation is unspecified for some inputs.
Comparing for equality
A type that provides evidence for equality between two types.
eqSingNat :: Sing (m :: Nat) -> Sing (n :: Nat) -> Maybe (m :~: n)Source
Check if two type-natural singletons of potentially different types are indeed the same, by comparing their runtime representations.
eqSingSym :: Sing (m :: Symbol) -> Sing (n :: Symbol) -> Maybe (m :~: n)Source
Check if two symbol singletons of potentially different types are indeed the same, by comparing their runtime representations.
Destructing type-nat singletons.
Matching on type-nats
Unary implementation of natural numbers. Used both at the type and at the value level.