singletons-0.10.0: A framework for generating singleton types

Copyright(C) 2014 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRichard Eisenberg (eir@cis.upenn.edu)
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Singletons.TypeLits

Description

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

Synopsis

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

type SNat x = Sing x Source

Kind-restricted synonym for Sing for Nats

type SSymbol x = Sing x Source

Kind-restricted synonym for Sing for Symbols

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

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

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

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

type family Error str :: k Source

The promotion of error

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

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