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.

Synopsis

Documentation

data Nat :: *

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

Instances

SNum Nat (KProxy Nat) Source
PNum Nat (KProxy Nat) Source
SEnum Nat (KProxy Nat) Source
PEnum Nat (KProxy Nat) Source
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:^$$) Source
SuppressUnusedWarnings (TyFun [Nat] Nat -> *) SumSym0 Source
SuppressUnusedWarnings (TyFun [Nat] Nat -> *) ProductSym0 Source
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> ) -> ) (:^$) Source
SuppressUnusedWarnings ((TyFun k Bool -> ) -> TyFun [k] (Maybe Nat) -> ) (FindIndexSym1 k) Source
SuppressUnusedWarnings ((TyFun k Bool -> ) -> TyFun [k] [Nat] -> ) (FindIndicesSym1 k) Source
SuppressUnusedWarnings ([k] -> TyFun Nat k -> *) ((:!!$$) k) Source
SuppressUnusedWarnings (Nat -> TyFun [k] ((,) [k] [k]) -> *) (SplitAtSym1 k) Source
SuppressUnusedWarnings (Nat -> TyFun [k] [k] -> *) (TakeSym1 k) Source
SuppressUnusedWarnings (Nat -> TyFun [k] [k] -> *) (DropSym1 k) Source
SuppressUnusedWarnings (Nat -> TyFun k [k] -> *) (ReplicateSym1 k) Source
SuppressUnusedWarnings (k -> TyFun [k] (Maybe Nat) -> *) (ElemIndexSym1 k) Source
SuppressUnusedWarnings (k -> TyFun [k] [Nat] -> *) (ElemIndicesSym1 k) Source
SuppressUnusedWarnings (TyFun (TyFun k Bool -> ) (TyFun [k] (Maybe Nat) -> ) -> *) (FindIndexSym0 k) Source
SuppressUnusedWarnings (TyFun (TyFun k Bool -> ) (TyFun [k] [Nat] -> ) -> *) (FindIndicesSym0 k) Source
SuppressUnusedWarnings (TyFun [k] Nat -> *) (LengthSym0 k) Source
SuppressUnusedWarnings (TyFun [k] (TyFun Nat k -> ) -> ) ((:!!$) k) Source
SuppressUnusedWarnings (TyFun Nat (TyFun [k] ((,) [k] [k]) -> ) -> ) (SplitAtSym0 k) Source
SuppressUnusedWarnings (TyFun Nat (TyFun [k] [k] -> ) -> ) (TakeSym0 k) Source
SuppressUnusedWarnings (TyFun Nat (TyFun [k] [k] -> ) -> ) (DropSym0 k) Source
SuppressUnusedWarnings (TyFun Nat (TyFun k [k] -> ) -> ) (ReplicateSym0 k) Source
SuppressUnusedWarnings (TyFun Nat k -> *) (FromIntegerSym0 k) Source
SuppressUnusedWarnings (TyFun Nat k -> *) (ToEnumSym0 k) Source
SuppressUnusedWarnings (TyFun k Nat -> *) (FromEnumSym0 k) Source
SuppressUnusedWarnings (TyFun k (TyFun [k] (Maybe Nat) -> ) -> ) (ElemIndexSym0 k) Source
SuppressUnusedWarnings (TyFun k (TyFun [k] [Nat] -> ) -> ) (ElemIndicesSym0 k) Source
data Sing Nat where SNat :: KnownNat n => Sing Nat n Source
type Negate Nat a = Error Nat Symbol "Cannot negate a natural number" Source
type Abs Nat a = a Source
type Signum Nat a Source
type FromInteger Nat a = a Source
type Succ Nat a0 Source
type Pred Nat a0 Source
type ToEnum Nat a0 Source
type FromEnum Nat a0 Source
type (==) Nat a b = EqNat a b
type (:==) Nat a b = (==) Nat a b Source
type (:/=) Nat x y = Not ((:==) Nat x y)
type Compare Nat a b = CmpNat a b Source
type (:<) Nat arg0 arg1
type (:<=) Nat arg0 arg1
type (:>) Nat arg0 arg1
type (:>=) Nat arg0 arg1
type Max Nat arg0 arg1
type Min Nat arg0 arg1
type (:+) Nat a b = (+) a b Source
type (:-) Nat a b = (-) a b Source
type (:) Nat a b = a b Source
type EnumFromTo Nat a0 a1 Source
type EnumFromThenTo Nat a0 a1 a2 Source
type Apply Nat Nat ((:^$$) l1) l0 = (:^$$$) l1 l0 Source
type Apply Nat k (FromEnumSym0 k) l0 = FromEnumSym1 k l0 Source
type Apply k Nat (FromIntegerSym0 k) l0 = FromIntegerSym1 k l0 Source
type Apply k Nat (ToEnumSym0 k) l0 = ToEnumSym1 k l0 Source
type Apply k Nat ((:!!$$) k l1) l0 = (:!!$$$) k l1 l0 Source
type DemoteRep Nat (KProxy Nat) = Integer Source
type Apply Nat [Nat] SumSym0 l0 = SumSym1 l0 Source
type Apply Nat [Nat] ProductSym0 l0 = ProductSym1 l0 Source
type Apply Nat [k] (LengthSym0 k) l0 = LengthSym1 k l0 Source
type Apply [Nat] [k] (ElemIndicesSym1 k l1) l0 = ElemIndicesSym2 k l1 l0 Source
type Apply [Nat] [k] (FindIndicesSym1 k l1) l0 = FindIndicesSym2 k l1 l0 Source
type Apply (Maybe Nat) [k] (ElemIndexSym1 k l1) l0 = ElemIndexSym2 k l1 l0 Source
type Apply (Maybe Nat) [k] (FindIndexSym1 k l1) l0 = FindIndexSym2 k l1 l0 Source
type Apply (TyFun Nat Nat -> *) Nat (:^$) l0 = (:^$$) l0 Source
type Apply (TyFun [k] (Maybe Nat) -> *) k (ElemIndexSym0 k) l0 = ElemIndexSym1 k l0 Source
type Apply (TyFun [k] [Nat] -> *) k (ElemIndicesSym0 k) l0 = ElemIndicesSym1 k l0 Source
type Apply (TyFun [k] ((,) [k] [k]) -> *) Nat (SplitAtSym0 k) l0 = SplitAtSym1 k l0 Source
type Apply (TyFun [k] [k] -> *) Nat (TakeSym0 k) l0 = TakeSym1 k l0 Source
type Apply (TyFun [k] [k] -> *) Nat (DropSym0 k) l0 = DropSym1 k l0 Source
type Apply (TyFun k [k] -> *) Nat (ReplicateSym0 k) l0 = ReplicateSym1 k l0 Source
type Apply (TyFun Nat k -> *) [k] ((:!!$) k) l0 = (:!!$$) k l0 Source
type Apply (TyFun [k] (Maybe Nat) -> ) (TyFun k Bool -> ) (FindIndexSym0 k) l0 = FindIndexSym1 k l0 Source
type Apply (TyFun [k] [Nat] -> ) (TyFun k Bool -> ) (FindIndicesSym0 k) l0 = FindIndicesSym1 k l0 Source

data Symbol :: *

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

Instances

data Sing Symbol where SSym :: KnownSymbol n => Sing Symbol n Source
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

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. This version is more poly-kinded for easier use.

data ErrorSym0 l Source

Instances

SuppressUnusedWarnings (TyFun k k -> *) (ErrorSym0 k k) Source
type Apply k k1 (ErrorSym0 k k1) l0 = ErrorSym1 k1 k l0 Source

type ErrorSym1 t = Error t Source

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

Minimal complete definition

natSing

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

Since: 4.7.0.0

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

type (:^) a b = a ^ b infixr 8 Source

data (:^$) l Source

Instances

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> ) -> ) (:^$) Source
type Apply (TyFun Nat Nat -> *) Nat (:^$) l0 = (:^$$) l0 Source

data l :^$$ l Source

Instances

SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:^$$) Source
type Apply Nat Nat ((:^$$) l1) l0 = (:^$$$) l1 l0 Source

type (:^$$$) t t = (:^) t t Source