singletons-2.2: 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

Contents

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 # 
SEnum Nat # 
PNum Nat (Proxy * Nat) # 

Associated Types

type ((Proxy * Nat) :+ (arg :: Proxy * Nat)) (arg :: Proxy * Nat) :: a #

type ((Proxy * Nat) :- (arg :: Proxy * Nat)) (arg :: Proxy * Nat) :: a #

type ((Proxy * Nat) :* (arg :: Proxy * Nat)) (arg :: Proxy * Nat) :: a #

type Negate (Proxy * Nat) (arg :: Proxy * Nat) :: a #

type Abs (Proxy * Nat) (arg :: Proxy * Nat) :: a #

type Signum (Proxy * Nat) (arg :: Proxy * Nat) :: a #

type FromInteger (Proxy * Nat) (arg :: Nat) :: a #

PEnum Nat (Proxy * Nat) # 

Associated Types

type Succ (Proxy * Nat) (arg :: Proxy * Nat) :: a #

type Pred (Proxy * Nat) (arg :: Proxy * Nat) :: a #

type ToEnum (Proxy * Nat) (arg :: Nat) :: a #

type FromEnum (Proxy * Nat) (arg :: Proxy * Nat) :: Nat #

type EnumFromTo (Proxy * Nat) (arg :: Proxy * Nat) (arg :: Proxy * Nat) :: [a] #

type EnumFromThenTo (Proxy * Nat) (arg :: Proxy * Nat) (arg :: Proxy * Nat) (arg :: Proxy * Nat) :: [a] #

SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:^$$) # 
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:^$) # 
SuppressUnusedWarnings ((TyFun a6989586621679796322 Bool -> Type) -> TyFun [a6989586621679796322] (Maybe Nat) -> *) (FindIndexSym1 a6989586621679796322) # 

Methods

suppressUnusedWarnings :: Proxy (FindIndexSym1 a6989586621679796322) t -> () #

SuppressUnusedWarnings ((TyFun a6989586621679796321 Bool -> Type) -> TyFun [a6989586621679796321] [Nat] -> *) (FindIndicesSym1 a6989586621679796321) # 

Methods

suppressUnusedWarnings :: Proxy (FindIndicesSym1 a6989586621679796321) t -> () #

SuppressUnusedWarnings ([a6989586621679796295] -> TyFun Nat a6989586621679796295 -> *) ((:!!$$) a6989586621679796295) # 

Methods

suppressUnusedWarnings :: Proxy ((:!!$$) a6989586621679796295) t -> () #

SuppressUnusedWarnings (Nat -> TyFun [a6989586621679796311] ([a6989586621679796311], [a6989586621679796311]) -> *) (SplitAtSym1 a6989586621679796311) # 

Methods

suppressUnusedWarnings :: Proxy (SplitAtSym1 a6989586621679796311) t -> () #

SuppressUnusedWarnings (Nat -> TyFun [a6989586621679796313] [a6989586621679796313] -> *) (TakeSym1 a6989586621679796313) # 

Methods

suppressUnusedWarnings :: Proxy (TakeSym1 a6989586621679796313) t -> () #

SuppressUnusedWarnings (Nat -> TyFun [a6989586621679796312] [a6989586621679796312] -> *) (DropSym1 a6989586621679796312) # 

Methods

suppressUnusedWarnings :: Proxy (DropSym1 a6989586621679796312) t -> () #

SuppressUnusedWarnings (Nat -> TyFun a6989586621679796297 [a6989586621679796297] -> *) (ReplicateSym1 a6989586621679796297) # 

Methods

suppressUnusedWarnings :: Proxy (ReplicateSym1 a6989586621679796297) t -> () #

SuppressUnusedWarnings (a6989586621679796324 -> TyFun [a6989586621679796324] (Maybe Nat) -> *) (ElemIndexSym1 a6989586621679796324) # 

Methods

suppressUnusedWarnings :: Proxy (ElemIndexSym1 a6989586621679796324) t -> () #

SuppressUnusedWarnings (a6989586621679796323 -> TyFun [a6989586621679796323] [Nat] -> *) (ElemIndicesSym1 a6989586621679796323) # 

Methods

suppressUnusedWarnings :: Proxy (ElemIndicesSym1 a6989586621679796323) t -> () #

SuppressUnusedWarnings (TyFun (TyFun a6989586621679796322 Bool -> Type) (TyFun [a6989586621679796322] (Maybe Nat) -> Type) -> *) (FindIndexSym0 a6989586621679796322) # 

Methods

suppressUnusedWarnings :: Proxy (FindIndexSym0 a6989586621679796322) t -> () #

SuppressUnusedWarnings (TyFun (TyFun a6989586621679796321 Bool -> Type) (TyFun [a6989586621679796321] [Nat] -> Type) -> *) (FindIndicesSym0 a6989586621679796321) # 

Methods

suppressUnusedWarnings :: Proxy (FindIndicesSym0 a6989586621679796321) t -> () #

SuppressUnusedWarnings (TyFun [a6989586621679796298] Nat -> *) (LengthSym0 a6989586621679796298) # 

Methods

suppressUnusedWarnings :: Proxy (LengthSym0 a6989586621679796298) t -> () #

SuppressUnusedWarnings (TyFun [a6989586621679796295] (TyFun Nat a6989586621679796295 -> Type) -> *) ((:!!$) a6989586621679796295) # 

Methods

suppressUnusedWarnings :: Proxy ((:!!$) a6989586621679796295) t -> () #

SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679796311] ([a6989586621679796311], [a6989586621679796311]) -> Type) -> *) (SplitAtSym0 a6989586621679796311) # 

Methods

suppressUnusedWarnings :: Proxy (SplitAtSym0 a6989586621679796311) t -> () #

SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679796313] [a6989586621679796313] -> Type) -> *) (TakeSym0 a6989586621679796313) # 

Methods

suppressUnusedWarnings :: Proxy (TakeSym0 a6989586621679796313) t -> () #

SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679796312] [a6989586621679796312] -> Type) -> *) (DropSym0 a6989586621679796312) # 

Methods

suppressUnusedWarnings :: Proxy (DropSym0 a6989586621679796312) t -> () #

SuppressUnusedWarnings (TyFun Nat (TyFun a6989586621679796297 [a6989586621679796297] -> Type) -> *) (ReplicateSym0 a6989586621679796297) # 

Methods

suppressUnusedWarnings :: Proxy (ReplicateSym0 a6989586621679796297) t -> () #

SuppressUnusedWarnings (TyFun Nat a6989586621679685236 -> *) (FromIntegerSym0 a6989586621679685236) # 

Methods

suppressUnusedWarnings :: Proxy (FromIntegerSym0 a6989586621679685236) t -> () #

SuppressUnusedWarnings (TyFun Nat a6989586621679697496 -> *) (ToEnumSym0 a6989586621679697496) # 

Methods

suppressUnusedWarnings :: Proxy (ToEnumSym0 a6989586621679697496) t -> () #

SuppressUnusedWarnings (TyFun a6989586621679697496 Nat -> *) (FromEnumSym0 a6989586621679697496) # 

Methods

suppressUnusedWarnings :: Proxy (FromEnumSym0 a6989586621679697496) t -> () #

SuppressUnusedWarnings (TyFun a6989586621679796324 (TyFun [a6989586621679796324] (Maybe Nat) -> Type) -> *) (ElemIndexSym0 a6989586621679796324) # 

Methods

suppressUnusedWarnings :: Proxy (ElemIndexSym0 a6989586621679796324) t -> () #

SuppressUnusedWarnings (TyFun a6989586621679796323 (TyFun [a6989586621679796323] [Nat] -> Type) -> *) (ElemIndicesSym0 a6989586621679796323) # 

Methods

suppressUnusedWarnings :: Proxy (ElemIndicesSym0 a6989586621679796323) t -> () #

type DemoteRep Nat # 
data Sing Nat # 
data Sing Nat where
type Negate Nat a # 
type Negate Nat a = Error Nat Symbol "Cannot negate a natural number"
type Abs Nat a # 
type Abs Nat a = a
type Signum Nat a # 
type Signum Nat a
type FromInteger Nat a # 
type FromInteger Nat a = a
type Succ Nat a0 # 
type Succ Nat a0
type Pred Nat a0 # 
type Pred Nat a0
type ToEnum Nat a0 # 
type ToEnum Nat a0
type FromEnum Nat a0 # 
type FromEnum Nat a0
type (==) Nat a b 
type (==) Nat a b = EqNat a b
type (:==) Nat a b # 
type (:==) Nat a b = (==) Nat a b
type (:/=) Nat x y # 
type (:/=) Nat x y = Not ((:==) Nat x y)
type Compare Nat a b # 
type Compare Nat a b = CmpNat a b
type (:<) Nat arg0 arg1 # 
type (:<) Nat arg0 arg1
type (:<=) Nat arg0 arg1 # 
type (:<=) Nat arg0 arg1
type (:>) Nat arg0 arg1 # 
type (:>) Nat arg0 arg1
type (:>=) Nat arg0 arg1 # 
type (:>=) Nat arg0 arg1
type Max Nat arg0 arg1 # 
type Max Nat arg0 arg1
type Min Nat arg0 arg1 # 
type Min Nat arg0 arg1
type (:+) Nat a b # 
type (:+) Nat a b = (+) a b
type (:-) Nat a b # 
type (:-) Nat a b = (-) a b
type (:*) Nat a b # 
type (:*) Nat a b = * a b
type EnumFromTo Nat a1 a0 # 
type EnumFromTo Nat a1 a0
type EnumFromThenTo Nat a2 a1 a0 # 
type EnumFromThenTo Nat a2 a1 a0
type Apply Nat Nat ((:^$$) l1) l0 # 
type Apply Nat Nat ((:^$$) l1) l0 = (:^$$$) l1 l0
type Apply Nat k2 (FromIntegerSym0 k2) l0 # 
type Apply Nat k2 (FromIntegerSym0 k2) l0 = FromIntegerSym1 k2 l0
type Apply Nat k2 (ToEnumSym0 k2) l0 # 
type Apply Nat k2 (ToEnumSym0 k2) l0 = ToEnumSym1 k2 l0
type Apply a6989586621679697496 Nat (FromEnumSym0 a6989586621679697496) l0 # 
type Apply a6989586621679697496 Nat (FromEnumSym0 a6989586621679697496) l0 = FromEnumSym1 a6989586621679697496 l0
type Apply Nat a6989586621679796295 ((:!!$$) a6989586621679796295 l0) l1 # 
type Apply Nat a6989586621679796295 ((:!!$$) a6989586621679796295 l0) l1 = (:!!$$$) a6989586621679796295 l0 l1
type Apply Nat (TyFun Nat Nat -> *) (:^$) l0 # 
type Apply Nat (TyFun Nat Nat -> *) (:^$) l0 = (:^$$) l0
type Apply Nat (TyFun [a6989586621679796311] ([a6989586621679796311], [a6989586621679796311]) -> Type) (SplitAtSym0 a6989586621679796311) l0 # 
type Apply Nat (TyFun [a6989586621679796311] ([a6989586621679796311], [a6989586621679796311]) -> Type) (SplitAtSym0 a6989586621679796311) l0 = SplitAtSym1 a6989586621679796311 l0
type Apply Nat (TyFun [a6989586621679796313] [a6989586621679796313] -> Type) (TakeSym0 a6989586621679796313) l0 # 
type Apply Nat (TyFun [a6989586621679796313] [a6989586621679796313] -> Type) (TakeSym0 a6989586621679796313) l0 = TakeSym1 a6989586621679796313 l0
type Apply Nat (TyFun [a6989586621679796312] [a6989586621679796312] -> Type) (DropSym0 a6989586621679796312) l0 # 
type Apply Nat (TyFun [a6989586621679796312] [a6989586621679796312] -> Type) (DropSym0 a6989586621679796312) l0 = DropSym1 a6989586621679796312 l0
type Apply Nat (TyFun a6989586621679796297 [a6989586621679796297] -> Type) (ReplicateSym0 a6989586621679796297) l0 # 
type Apply Nat (TyFun a6989586621679796297 [a6989586621679796297] -> Type) (ReplicateSym0 a6989586621679796297) l0 = ReplicateSym1 a6989586621679796297 l0
type Apply a6989586621679796324 (TyFun [a6989586621679796324] (Maybe Nat) -> Type) (ElemIndexSym0 a6989586621679796324) l0 # 
type Apply a6989586621679796324 (TyFun [a6989586621679796324] (Maybe Nat) -> Type) (ElemIndexSym0 a6989586621679796324) l0 = ElemIndexSym1 a6989586621679796324 l0
type Apply a6989586621679796323 (TyFun [a6989586621679796323] [Nat] -> Type) (ElemIndicesSym0 a6989586621679796323) l0 # 
type Apply a6989586621679796323 (TyFun [a6989586621679796323] [Nat] -> Type) (ElemIndicesSym0 a6989586621679796323) l0 = ElemIndicesSym1 a6989586621679796323 l0
type Apply [a6989586621679796298] Nat (LengthSym0 a6989586621679796298) l0 # 
type Apply [a6989586621679796298] Nat (LengthSym0 a6989586621679796298) l0 = LengthSym1 a6989586621679796298 l0
type Apply [a6989586621679796324] (Maybe Nat) (ElemIndexSym1 a6989586621679796324 l0) l1 # 
type Apply [a6989586621679796324] (Maybe Nat) (ElemIndexSym1 a6989586621679796324 l0) l1 = ElemIndexSym2 a6989586621679796324 l0 l1
type Apply [a6989586621679796322] (Maybe Nat) (FindIndexSym1 a6989586621679796322 l0) l1 # 
type Apply [a6989586621679796322] (Maybe Nat) (FindIndexSym1 a6989586621679796322 l0) l1 = FindIndexSym2 a6989586621679796322 l0 l1
type Apply [a6989586621679796323] [Nat] (ElemIndicesSym1 a6989586621679796323 l0) l1 # 
type Apply [a6989586621679796323] [Nat] (ElemIndicesSym1 a6989586621679796323 l0) l1 = ElemIndicesSym2 a6989586621679796323 l0 l1
type Apply [a6989586621679796321] [Nat] (FindIndicesSym1 a6989586621679796321 l0) l1 # 
type Apply [a6989586621679796321] [Nat] (FindIndicesSym1 a6989586621679796321 l0) l1 = FindIndicesSym2 a6989586621679796321 l0 l1
type Apply [a6989586621679796295] (TyFun Nat a6989586621679796295 -> Type) ((:!!$) a6989586621679796295) l0 # 
type Apply [a6989586621679796295] (TyFun Nat a6989586621679796295 -> Type) ((:!!$) a6989586621679796295) l0 = (:!!$$) a6989586621679796295 l0
type Apply (TyFun a6989586621679796322 Bool -> Type) (TyFun [a6989586621679796322] (Maybe Nat) -> Type) (FindIndexSym0 a6989586621679796322) l0 # 
type Apply (TyFun a6989586621679796322 Bool -> Type) (TyFun [a6989586621679796322] (Maybe Nat) -> Type) (FindIndexSym0 a6989586621679796322) l0 = FindIndexSym1 a6989586621679796322 l0
type Apply (TyFun a6989586621679796321 Bool -> Type) (TyFun [a6989586621679796321] [Nat] -> Type) (FindIndicesSym0 a6989586621679796321) l0 # 
type Apply (TyFun a6989586621679796321 Bool -> Type) (TyFun [a6989586621679796321] [Nat] -> Type) (FindIndicesSym0 a6989586621679796321) l0 = FindIndicesSym1 a6989586621679796321 l0

data Symbol :: * #

(Kind) This is the kind of type-level symbols. Declared here because class IP needs it

Instances

KnownSymbol a => SingI Symbol a 

Methods

sing :: Sing a a

SingKind Symbol (KProxy Symbol) 

Associated Types

type DemoteRep (KProxy Symbol) (kparam :: KProxy (KProxy Symbol)) :: *

Methods

fromSing :: Sing (KProxy Symbol) a -> DemoteRep (KProxy Symbol) kparam

data Sing Symbol 
data Sing Symbol where
type DemoteRep Symbol # 
data Sing Symbol # 
data Sing Symbol where
type (==) Symbol a b 
type (==) Symbol a b = EqSymbol a b
type (:==) Symbol a b # 
type (:==) Symbol a b = (==) Symbol a b
type (:/=) Symbol x y # 
type (:/=) Symbol x y = Not ((:==) Symbol x y)
type Compare Symbol a b # 
type Compare Symbol a b = CmpSymbol a b
type (:<) Symbol arg0 arg1 # 
type (:<) Symbol arg0 arg1
type (:<=) Symbol arg0 arg1 # 
type (:<=) Symbol arg0 arg1
type (:>) Symbol arg0 arg1 # 
type (:>) Symbol arg0 arg1
type (:>=) Symbol arg0 arg1 # 
type (:>=) Symbol arg0 arg1
type Max Symbol arg0 arg1 # 
type Max Symbol arg0 arg1
type Min Symbol arg0 arg1 # 
type Min Symbol arg0 arg1
type DemoteRep Symbol (KProxy Symbol) 
type DemoteRep Symbol (KProxy Symbol) = String

data family Sing (a :: k) #

The singleton kind-indexed data family.

Instances

data Sing Bool # 
data Sing Bool where
data Sing Ordering # 
data Sing * # 
data Sing * where
data Sing Nat # 
data Sing Nat where
data Sing Symbol # 
data Sing Symbol where
data Sing () # 
data Sing () where
data Sing [a0] # 
data Sing [a0] where
data Sing (Maybe a0) # 
data Sing (Maybe a0) where
data Sing (NonEmpty a0) # 
data Sing (NonEmpty a0) where
data Sing (Either a0 b0) # 
data Sing (Either a0 b0) where
data Sing (a0, b0) # 
data Sing (a0, b0) where
data Sing ((~>) k1 k2) # 
data Sing ((~>) k1 k2) = SLambda {}
data Sing (a0, b0, c0) # 
data Sing (a0, b0, c0) where
data Sing (a0, b0, c0, d0) # 
data Sing (a0, b0, c0, d0) where
data Sing (a0, b0, c0, d0, e0) # 
data Sing (a0, b0, c0, d0, e0) where
data Sing (a0, b0, c0, d0, e0, f0) # 
data Sing (a0, b0, c0, d0, e0, f0) where
data Sing (a0, b0, c0, d0, e0, f0, g0) # 
data Sing (a0, b0, c0, d0, e0, f0, g0) where

type SNat x = Sing x #

Kind-restricted synonym for Sing for Nats

type SSymbol x = Sing x #

Kind-restricted synonym for Sing for Symbols

withKnownNat :: Sing n -> (KnownNat n => r) -> r #

Given a singleton for Nat, call something requiring a KnownNat instance.

withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r #

Given a singleton for Symbol, call something requiring a KnownSymbol instance.

type family Error (str :: k0) :: k #

The promotion of error. This version is more poly-kinded for easier use.

data ErrorSym0 l #

Instances

SuppressUnusedWarnings (TyFun k06989586621679675033 k6989586621679675035 -> *) (ErrorSym0 k06989586621679675033 k6989586621679675035) # 

Methods

suppressUnusedWarnings :: Proxy (ErrorSym0 k06989586621679675033 k6989586621679675035) t -> () #

type Apply k06989586621679675033 k2 (ErrorSym0 k06989586621679675033 k2) l0 # 
type Apply k06989586621679675033 k2 (ErrorSym0 k06989586621679675033 k2) l0 = ErrorSym1 k2 k06989586621679675033 l0

type ErrorSym1 t = Error t #

sError :: Sing (str :: Symbol) -> a #

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 #

data (:^$) l #

Instances

data l :^$$ l #

Instances

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

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

Orphan instances

Num Nat # 

Methods

(+) :: Nat -> Nat -> Nat #

(-) :: Nat -> Nat -> Nat #

(*) :: Nat -> Nat -> Nat #

negate :: Nat -> Nat #

abs :: Nat -> Nat #

signum :: Nat -> Nat #

fromInteger :: Integer -> Nat #