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 working with type-level naturals should be defined in a separate library.



data Nat Source

(Kind) This is the kind of type-level natural numbers.

data Symbol Source

(Kind) 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 ~ 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.

Associated Types

type DemoteRep kparam :: *Source


fromSing :: Sing (a :: k) -> DemoteRep kparamSource

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.


(SingI k a, SingE k (KindOf k a)) => SingRep k a 

singByProxy :: SingI n => proxy n -> Sing nSource

A convenience function to create a singleton value, when we have a proxy argument in scope.

data SomeSing whereSource


SomeSing :: SingI (n :: k) => proxy n -> SomeSing (kp :: KindIs k) 

class kp ~ KindParam => ToSing kp whereSource

The class of function that can promote a representation value into a singleton. Like SingE, this class overloads based on a *kind*. The method returns Maybe because sometimes the representation type contains more values than are supported by the singletons.


toSing :: DemoteRep kp -> Maybe (SomeSing kp)Source

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

class (m <=? n) ~ True => m (<=) n Source

Comparison of type-level naturals.


~ Bool (<=? m n) True => m <= n 

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.

type family m (-) n :: NatSource

Subtraction of type-level naturals. Note that this operation is unspecified for some inputs.

Comparing for equality

data :~: whereSource

A type that provides evidence for equality between two types.


Refl :: a :~: a 


Show (:~: k a b) 

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.

data IsZero whereSource


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


Show (IsZero n) 

Matching on type-nats

data Nat1 Source

Unary implementation of natural numbers. Used both at the type and at the value level.


Succ Nat1 

type family FromNat1 n :: NatSource

Kind parameters

data KindIs a Source

(Kind) A kind useful for passing kinds as parameters.



type Demote a = DemoteRep (KindOf a)Source

A convenient name for the type used to representing the values for a particular singleton family. For example, Demote 2 ~ Integer, and also Demote 3 ~ Integer, but Demote Hello ~ String.

type KindOf a = (KindParam :: KindIs k)Source

A shortcut for naming the kind parameter corresponding to the kind of a some type. For example, KindOf Int ~ (KindParam :: KindIs *), but KindOf 2 ~ (KindParam :: KindIs Nat).