singletons-2.0.1: 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. 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 (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 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 [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 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 

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

data l :^$$ l Source

Instances

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