singletons-1.1.2.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.

Synopsis

Documentation

data Nat :: *

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

Instances

KnownNat n => SingI Nat n 
SingKind Nat (KProxy Nat) 
SDecide Nat (KProxy Nat) 
PEq Nat (KProxy Nat) 
SEq Nat (KProxy Nat) 
POrd Nat (KProxy Nat) 
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:^$$) 
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:*$$) 
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:-$$) 
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:+$$) 
SuppressUnusedWarnings (TyFun [Nat] Nat -> *) SumSym0 
SuppressUnusedWarnings (TyFun [Nat] Nat -> *) ProductSym0 
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:^$) 
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:*$) 
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:-$) 
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:+$) 
SuppressUnusedWarnings ((TyFun k Bool -> *) -> TyFun [k] (Maybe Nat) -> *) (FindIndexSym1 k) 
SuppressUnusedWarnings ((TyFun k Bool -> *) -> TyFun [k] [Nat] -> *) (FindIndicesSym1 k) 
SuppressUnusedWarnings ([k] -> TyFun Nat k -> *) ((:!!$$) k) 
SuppressUnusedWarnings (Nat -> TyFun [k] ((,) [k] [k]) -> *) (SplitAtSym1 k) 
SuppressUnusedWarnings (Nat -> TyFun [k] [k] -> *) (TakeSym1 k) 
SuppressUnusedWarnings (Nat -> TyFun [k] [k] -> *) (DropSym1 k) 
SuppressUnusedWarnings (Nat -> TyFun k [k] -> *) (ReplicateSym1 k) 
SuppressUnusedWarnings (k -> TyFun [k] (Maybe Nat) -> *) (ElemIndexSym1 k) 
SuppressUnusedWarnings (k -> TyFun [k] [Nat] -> *) (ElemIndicesSym1 k) 
SuppressUnusedWarnings (TyFun (TyFun k Bool -> *) (TyFun [k] (Maybe Nat) -> *) -> *) (FindIndexSym0 k) 
SuppressUnusedWarnings (TyFun (TyFun k Bool -> *) (TyFun [k] [Nat] -> *) -> *) (FindIndicesSym0 k) 
SuppressUnusedWarnings (TyFun [k] Nat -> *) (LengthSym0 k) 
SuppressUnusedWarnings (TyFun [k] (TyFun Nat k -> *) -> *) ((:!!$) k) 
SuppressUnusedWarnings (TyFun Nat (TyFun [k] ((,) [k] [k]) -> *) -> *) (SplitAtSym0 k) 
SuppressUnusedWarnings (TyFun Nat (TyFun [k] [k] -> *) -> *) (TakeSym0 k) 
SuppressUnusedWarnings (TyFun Nat (TyFun [k] [k] -> *) -> *) (DropSym0 k) 
SuppressUnusedWarnings (TyFun Nat (TyFun k [k] -> *) -> *) (ReplicateSym0 k) 
SuppressUnusedWarnings (TyFun k (TyFun [k] (Maybe Nat) -> *) -> *) (ElemIndexSym0 k) 
SuppressUnusedWarnings (TyFun k (TyFun [k] [Nat] -> *) -> *) (ElemIndicesSym0 k) 
data Sing Nat where 
type (==) Nat a b = EqNat a b 
type (:==) Nat a b = (==) Nat a b 
type Compare Nat a b = CmpNat a b 
type Apply Nat Nat ((:^$$) l1) l0 
type Apply Nat Nat ((:*$$) l1) l0 
type Apply Nat Nat ((:-$$) l1) l0 
type Apply Nat Nat ((:+$$) l1) l0 
type Apply k Nat ((:!!$$) k l1) l0 = (:!!$$$) k l1 l0 
type DemoteRep Nat (KProxy Nat) = Integer 
type Apply Nat [Nat] SumSym0 l0 = SumSym1 l0 
type Apply Nat [Nat] ProductSym0 l0 = ProductSym1 l0 
type Apply Nat [k] (LengthSym0 k) l0 = LengthSym1 k l0 
type Apply [Nat] [k] (ElemIndicesSym1 k l1) l0 = ElemIndicesSym2 k l1 l0 
type Apply [Nat] [k] (FindIndicesSym1 k l1) l0 = FindIndicesSym2 k l1 l0 
type Apply (Maybe Nat) [k] (ElemIndexSym1 k l1) l0 = ElemIndexSym2 k l1 l0 
type Apply (Maybe Nat) [k] (FindIndexSym1 k l1) l0 = FindIndexSym2 k l1 l0 
type Apply (TyFun Nat Nat -> *) Nat (:^$) l0 = (:^$$) l0 
type Apply (TyFun Nat Nat -> *) Nat (:*$) l0 = (:*$$) l0 
type Apply (TyFun Nat Nat -> *) Nat (:-$) l0 = (:-$$) l0 
type Apply (TyFun Nat Nat -> *) Nat (:+$) l0 = (:+$$) l0 
type Apply (TyFun [k] (Maybe Nat) -> *) k (ElemIndexSym0 k) l0 = ElemIndexSym1 k l0 
type Apply (TyFun [k] [Nat] -> *) k (ElemIndicesSym0 k) l0 = ElemIndicesSym1 k l0 
type Apply (TyFun [k] ((,) [k] [k]) -> *) Nat (SplitAtSym0 k) l0 = SplitAtSym1 k l0 
type Apply (TyFun [k] [k] -> *) Nat (TakeSym0 k) l0 = TakeSym1 k l0 
type Apply (TyFun [k] [k] -> *) Nat (DropSym0 k) l0 = DropSym1 k l0 
type Apply (TyFun k [k] -> *) Nat (ReplicateSym0 k) l0 = ReplicateSym1 k l0 
type Apply (TyFun Nat k -> *) [k] ((:!!$) k) l0 = (:!!$$) k l0 
type Apply (TyFun [k] (Maybe Nat) -> *) (TyFun k Bool -> *) (FindIndexSym0 k) l0 = FindIndexSym1 k l0 
type Apply (TyFun [k] [Nat] -> *) (TyFun k Bool -> *) (FindIndicesSym0 k) l0 = FindIndicesSym1 k l0 

data Symbol :: *

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

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

data ErrorSym0 t1 Source

Instances

type Apply k Symbol (ErrorSym0 Symbol k) a = Error k a 

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 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

type (:+) x y = x + y Source

type (:-) x y = x - y Source

type (:*) x y = x * y Source

type (:^) x y = x ^ y Source

data (:+$) l Source

Instances

data l :+$$ l Source

Instances

data (:-$) l Source

Instances

data l :-$$ l Source

Instances

data (:*$) l Source

Instances

data l :*$$ l Source

Instances

data (:^$) l Source

Instances

data l :^$$ l Source

Instances