Data.Singletons.TypeLits

Defines and exports singletons useful for the Nat and Symbol kinds.

Documentation

data Nat

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

Instances

KnownNat n => SingI Nat n

SingKind Nat (KProxy Nat)

SDecide Nat (KProxy Nat)

SEq Nat (KProxy Nat)

data Sing Nat where

• SNat :: KnownNat n => Sing Nat n

type (==) Nat a b = EqNat a b

type DemoteRep Nat (KProxy Nat) = Integer

data Symbol

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

Instances

KnownSymbol n => SingI Symbol n

SingKind Symbol (KProxy Symbol)

SDecide Symbol (KProxy Symbol)

SEq Symbol (KProxy Symbol)

data Sing Symbol where

• SSym :: KnownSymbol n => Sing Symbol n

type (==) Symbol a b = EqSymbol a b

type DemoteRep Symbol (KProxy Symbol) = String

type SNat x = Sing x

Kind-restricted synonym for Sing for Nats

type SSymbol x = Sing x

Kind-restricted synonym for Sing for Symbols

withKnownNat :: Sing n -> (KnownNat n => r) -> r

Given a singleton for Nat, call something requiring a KnownNat instance.

withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r

Given a singleton for Symbol, call something requiring a KnownSymbol instance.

type family Error str :: k

The promotion of error

sError :: Sing (str :: Symbol) -> a

The singleton for error

class KnownNat n

This class gives the integer associated with a type-level natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.

Since: 4.7.0.0

natVal :: KnownNat n => proxy n -> Integer

Since: 4.7.0.0

class KnownSymbol n

This class gives the integer associated with a type-level symbol. There are instances of the class for every concrete literal: "hello", etc.

Since: 4.7.0.0

symbolVal :: KnownSymbol n => proxy n -> String

Since: 4.7.0.0