| Copyright | (C) 2014 Richard Eisenberg |
|---|---|
| License | BSD-style (see LICENSE) |
| Maintainer | Richard Eisenberg (eir@cis.upenn.edu) |
| Stability | experimental |
| Portability | non-portable |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.Singletons.TypeLits
Description
Defines and exports singletons useful for the Nat and Symbol kinds. This exports the internal, unsafe constructors. Use Data.Singletons.TypeLits for a safe interface.
- data Nat :: *
- data Symbol :: *
- type SNat x = Sing x
- type SSymbol x = Sing x
- withKnownNat :: Sing n -> (KnownNat n => r) -> r
- withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r
- type family Error str :: k
- data ErrorSym0 l
- type ErrorSym1 t = Error t
- sError :: Sing (str :: Symbol) -> a
- class KnownNat n
- natVal :: KnownNat n => proxy n -> Integer
- class KnownSymbol n
- symbolVal :: KnownSymbol n => proxy n -> String
- type (:^) a b = a ^ b
- data (:^$) l
- data l :^$$ l
- type (:^$$$) t t = (:^) t t
Documentation
data Nat :: *
(Kind) This is the kind of type-level natural numbers.
Instances
data Symbol :: *
(Kind) This is the kind of type-level symbols.
Instances
data Sing Symbol where
| |
| type (==) Symbol a b = EqSymbol a b | |
| type (:==) Symbol a b = (==) Symbol a b Source | |
| type (:/=) Symbol x y = Not ((:==) Symbol x y) | |
| type Compare Symbol a b = CmpSymbol a b Source | |
| type (:<) Symbol arg0 arg1 | |
| type (:<=) Symbol arg0 arg1 | |
| type (:>) Symbol arg0 arg1 | |
| type (:>=) Symbol arg0 arg1 | |
| type Max Symbol arg0 arg1 | |
| type Min Symbol arg0 arg1 | |
| type DemoteRep Symbol (KProxy Symbol) = String Source |
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. This version is more poly-kinded for
easier use.
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
Minimal complete definition
natSing
class KnownSymbol n
This class gives the string associated with a type-level symbol. There are instances of the class for every concrete literal: "hello", etc.
Since: 4.7.0.0
Minimal complete definition
symbolSing
symbolVal :: KnownSymbol n => proxy n -> String
Since: 4.7.0.0