| 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.
- 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 t1
- sError :: Sing (str :: Symbol) -> a
- class KnownNat n
- natVal :: KnownNat n => proxy n -> Integer
- class KnownSymbol n
- symbolVal :: KnownSymbol n => proxy n -> String
- type (:+) x y = x + y
- type (:-) x y = x - y
- type (:*) x y = x * y
- type (:^) x y = x ^ y
- data (:+$) l
- data l :+$$ l
- data (:-$) l
- data l :-$$ l
- data (:*$) l
- data l :*$$ l
- data (:^$) l
- data l :^$$ l
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
| KnownSymbol n => SingI Symbol n | |
| SingKind Symbol (KProxy Symbol) | |
| SDecide Symbol (KProxy Symbol) | |
| PEq Symbol (KProxy Symbol) | |
| SEq Symbol (KProxy Symbol) | |
| POrd Symbol (KProxy Symbol) | |
data Sing Symbol where
| |
| type (==) Symbol a b = EqSymbol a b | |
| type (:==) Symbol a b = (==) Symbol a b | |
| type Compare Symbol a b = CmpSymbol a b | |
| type Apply k Symbol (ErrorSym0 Symbol k) a = Error k a | |
| type DemoteRep Symbol (KProxy Symbol) = String |
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.
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 integer 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