base- Basic libraries

Safe HaskellNone




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 Source

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


data Symbol Source

This is the *kind* of type-level symbols.

Linking type and value level

data family Sing n Source

class SingI a whereSource

The class SingI provides a "smart" constructor for singleton types. There are built-in instances for the singleton types corresponding to type literals.


sing :: Sing aSource

The only value of type Sing a

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.


fromSing :: Sing (a :: k) -> repSource

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.


(SingI k a, SingE k (Kind k) rep) => SingRep k a rep 

type Kind = AnySource

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

Functions on type nats

class m (<=) n Source

Comparsion of type-level naturals.

type family m (<=?) n :: BoolSource

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.

data IsZero whereSource


IsZero :: IsZero 0 
IsSucc :: !(Sing n) -> IsZero (n + 1) 


Show (IsZero n) 

data IsEven whereSource


IsEvenZero :: IsEven 0 
IsEven :: !(Sing (n + 1)) -> IsEven ((2 * n) + 2) 
IsOdd :: !(Sing n) -> IsEven ((2 * n) + 1) 


Show (IsEven n)