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 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.