| Copyright | (C) 2014 Richard Eisenberg |
|---|---|
| License | BSD-style (see LICENSE) |
| Maintainer | Richard Eisenberg (rae@cs.brynmawr.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.
Synopsis
- data Nat :: *
- data Symbol :: *
- data family Sing (a :: k)
- type SNat (x :: Nat) = Sing x
- type SSymbol (x :: Symbol) = Sing x
- withKnownNat :: Sing n -> (KnownNat n => r) -> r
- withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r
- type family Error (str :: k0) :: k where ...
- sError :: Sing (str :: Symbol) -> a
- type family Undefined :: k where ...
- sUndefined :: a
- class KnownNat (n :: Nat)
- natVal :: KnownNat n => proxy n -> Natural
- class KnownSymbol (n :: Symbol)
- symbolVal :: KnownSymbol n => proxy n -> String
- type family (a :: Nat) ^ (b :: Nat) :: Nat where ...
- (%^) :: Sing a -> Sing b -> Sing (a ^ b)
- type (<>) a b = AppendSymbol a b
- (%<>) :: Sing a -> Sing b -> Sing (a <> b)
- type family Log2 (a :: Nat) :: Nat where ...
- sLog2 :: Sing x -> Sing (Log2 x)
- type family Div (a :: Nat) (b :: Nat) :: Nat where ...
- sDiv :: Sing x -> Sing y -> Sing (Div x y)
- type family Mod (a :: Nat) (b :: Nat) :: Nat where ...
- sMod :: Sing x -> Sing y -> Sing (Mod x y)
- type family DivMod (a :: Nat) (a :: Nat) :: (Nat, Nat) where ...
- sDivMod :: Sing x -> Sing y -> Sing (DivMod x y)
- type family Quot (a :: Nat) (a :: Nat) :: Nat where ...
- sQuot :: Sing x -> Sing y -> Sing (Quot x y)
- type family Rem (a :: Nat) (a :: Nat) :: Nat where ...
- sRem :: Sing x -> Sing y -> Sing (Rem x y)
- type family QuotRem (a :: Nat) (a :: Nat) :: (Nat, Nat) where ...
- sQuotRem :: Sing x -> Sing y -> Sing (QuotRem x y)
- data ErrorSym0 (l :: TyFun k06989586621679378680 k6989586621679378681)
- type ErrorSym1 (t :: k06989586621679378680) = Error t
- type UndefinedSym0 = Undefined
- data KnownNatSym0 (l :: TyFun Nat Constraint)
- type KnownNatSym1 (t :: Nat) = KnownNat t
- data KnownSymbolSym0 (l :: TyFun Symbol Constraint)
- type KnownSymbolSym1 (t :: Symbol) = KnownSymbol t
- data (^@#@$) (l :: TyFun Nat (TyFun Nat Nat -> Type))
- data (l :: Nat) ^@#@$$ (l :: TyFun Nat Nat)
- type (^@#@$$$) (t :: Nat) (t :: Nat) = (^) t t
- data (<>@#@$) l
- data (l :: Symbol) <>@#@$$ l
- type (<>@#@$$$) (t :: Symbol) (t :: Symbol) = (<>) t t
- data Log2Sym0 (l :: TyFun Nat Nat)
- type Log2Sym1 (t :: Nat) = Log2 t
- data DivSym0 (l :: TyFun Nat (TyFun Nat Nat -> Type))
- data DivSym1 (l :: Nat) (l :: TyFun Nat Nat)
- type DivSym2 (t :: Nat) (t :: Nat) = Div t t
- data ModSym0 (l :: TyFun Nat (TyFun Nat Nat -> Type))
- data ModSym1 (l :: Nat) (l :: TyFun Nat Nat)
- type ModSym2 (t :: Nat) (t :: Nat) = Mod t t
- data DivModSym0 (l :: TyFun Nat (TyFun Nat (Nat, Nat) -> Type))
- data DivModSym1 (l :: Nat) (l :: TyFun Nat (Nat, Nat))
- type DivModSym2 (t :: Nat) (t :: Nat) = DivMod t t
- data QuotSym0 (l :: TyFun Nat (TyFun Nat Nat -> Type))
- data QuotSym1 (l :: Nat) (l :: TyFun Nat Nat)
- type QuotSym2 (t :: Nat) (t :: Nat) = Quot t t
- data RemSym0 (l :: TyFun Nat (TyFun Nat Nat -> Type))
- data RemSym1 (l :: Nat) (l :: TyFun Nat Nat)
- type RemSym2 (t :: Nat) (t :: Nat) = Rem t t
- data QuotRemSym0 (l :: TyFun Nat (TyFun Nat (Nat, Nat) -> Type))
- data QuotRemSym1 (l :: Nat) (l :: TyFun Nat (Nat, Nat))
- type QuotRemSym2 (t :: Nat) (t :: Nat) = QuotRem t t
Documentation
(Kind) This is the kind of type-level natural numbers.
Instances
(Kind) This is the kind of type-level symbols. Declared here because class IP needs it
Instances
data family Sing (a :: k) Source #
The singleton kind-indexed data family.
Instances
| data Sing (z :: Bool) Source # | |
| data Sing (z :: Ordering) Source # | |
| data Sing (a :: Type) Source # | |
| data Sing (n :: Nat) Source # | |
| data Sing (n :: Symbol) Source # | |
| data Sing (z :: ()) Source # | |
| data Sing (z :: Void) Source # | |
| data Sing (z :: [a]) Source # | |
| data Sing (z :: Maybe a) Source # | |
| data Sing (z :: NonEmpty a) Source # | |
| data Sing (z :: Either a b) Source # | |
| data Sing (z :: (a, b)) Source # | |
| data Sing (f :: k1 ~> k2) Source # | |
| data Sing (z :: (a, b, c)) Source # | |
| data Sing (z :: (a, b, c, d)) Source # | |
| data Sing (z :: (a, b, c, d, e)) Source # | |
| data Sing (z :: (a, b, c, d, e, f)) Source # | |
| data Sing (z :: (a, b, c, d, e, f, g)) 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 :: k0) :: k where ... Source #
The promotion of error. This version is more poly-kinded for
easier use.
sUndefined :: a Source #
The singleton for undefined.
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 :: Symbol) #
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
type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8 #
Exponentiation of type-level naturals.
Since: 4.7.0.0
(%^) :: Sing a -> Sing b -> Sing (a ^ b) infixr 8 Source #
The singleton analogue of '(TL.^)' for Nats.
type (<>) a b = AppendSymbol a b infixr 6 Source #
The promoted analogue of '(<>)' for Symbols. This uses the special
AppendSymbol type family from GHC.TypeLits.
(%<>) :: Sing a -> Sing b -> Sing (a <> b) infixr 6 Source #
The singleton analogue of '(<>)' for Symbols.
type family Log2 (a :: Nat) :: Nat where ... #
Log base 2 (round down) of natural numbers.
Log 0 is undefined (i.e., it cannot be reduced).
Since: 4.11.0.0
type family Div (a :: Nat) (b :: Nat) :: Nat where ... infixl 7 #
Division (round down) of natural numbers.
Div x 0 is undefined (i.e., it cannot be reduced).
Since: 4.11.0.0
type family Mod (a :: Nat) (b :: Nat) :: Nat where ... infixl 7 #
Modulus of natural numbers.
Mod x 0 is undefined (i.e., it cannot be reduced).
Since: 4.11.0.0
type family QuotRem (a :: Nat) (a :: Nat) :: (Nat, Nat) where ... Source #
Equations
| QuotRem a_6989586621679397776 a_6989586621679397778 = Apply (Apply DivModSym0 a_6989586621679397776) a_6989586621679397778 |
Defunctionalization symbols
type UndefinedSym0 = Undefined Source #
data KnownNatSym0 (l :: TyFun Nat Constraint) Source #
Instances
| SuppressUnusedWarnings KnownNatSym0 Source # | |
Methods suppressUnusedWarnings :: () Source # | |
| type Apply KnownNatSym0 (l :: Nat) Source # | |
type KnownNatSym1 (t :: Nat) = KnownNat t Source #
data KnownSymbolSym0 (l :: TyFun Symbol Constraint) Source #
Instances
| SuppressUnusedWarnings KnownSymbolSym0 Source # | |
Methods suppressUnusedWarnings :: () Source # | |
| type Apply KnownSymbolSym0 (l :: Symbol) Source # | |
type KnownSymbolSym1 (t :: Symbol) = KnownSymbol t Source #
data DivModSym0 (l :: TyFun Nat (TyFun Nat (Nat, Nat) -> Type)) Source #
Instances
| SuppressUnusedWarnings DivModSym0 Source # | |
Methods suppressUnusedWarnings :: () Source # | |
| type Apply DivModSym0 (l :: Nat) Source # | |
data QuotRemSym0 (l :: TyFun Nat (TyFun Nat (Nat, Nat) -> Type)) Source #
Instances
| SuppressUnusedWarnings QuotRemSym0 Source # | |
Methods suppressUnusedWarnings :: () Source # | |
| type Apply QuotRemSym0 (l :: Nat) Source # | |
Orphan instances
| Eq Nat Source # | |
| Eq Symbol Source # | This bogus instance is helpful for people who want to define functions over Symbols that will only be used at the type level or as singletons. |
| Num Nat Source # | This bogus |
| Ord Nat Source # | |
| Ord Symbol Source # | |
| IsString Symbol Source # | |
Methods fromString :: String -> Symbol # | |