GHC.TypeLits (original) (raw)

Contents

• Kinds
• Linking type and value level
• Working with singletons
• Functions on type nats
• Destructing type-nats.

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.

Synopsis

• data Nat
• data Symbol
• data family Sing n
• class SingI a where
  • sing :: Sing a
• class kparam ~ Kind => SingE kparam rep | kparam -> rep where
  • fromSing :: Sing (a :: k) -> rep
• 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](/packages/archive/
  //doc/html/GHC-Prim.html#t: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
  • IsZero :: IsZero 0
  • IsSucc :: !(Sing n) -> IsZero (n + 1)
• isEven :: Sing n -> IsEven n
• data IsEven where
  • IsEvenZero :: IsEven 0
  • IsEven :: !(Sing (n + 1)) -> IsEven ((2 * n) + 2)
  • IsOdd :: !(Sing n) -> IsEven ((2 * n) + 1)

Kinds

data Nat Source

This is the *kind* of type-level natural numbers.

Linking type and value level

class SingI a whereSource

The class [SingI](GHC-TypeLits.html#t: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](GHC-TypeLits.html#v: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.

type Kind = [Any](/packages/archive/
//doc/html/GHC-Prim.html#t:Any)Source

A type synonym useful for passing kinds as parameters.

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](GHC-TypeLits.html#v: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](Data-Maybe.html#v:Nothing). The property is expressed in terms of the underlying representation of the singleton.

Functions on type nats

class m (<=) n Source

Comparsion of type-level naturals.

type family m (+) n :: NatSource

Addition of type-level naturals.

type family m (*) n :: NatSource

Multiplication of type-level naturals.

type family m (^) n :: NatSource

Exponentiation of type-level naturals.

Destructing type-nats.