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 a6989586621679997031 Bool -> Type) -> TyFun [a6989586621679997031] (Maybe Nat) -> *) (FindIndexSym1 a6989586621679997031) # 

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

suppressUnusedWarnings :: Proxy (ElemIndicesSym0 a6989586621679997032) 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 a6989586621679883002 Nat (FromEnumSym0 a6989586621679883002) l0 # 
type Apply a6989586621679883002 Nat (FromEnumSym0 a6989586621679883002) l0 = FromEnumSym1 a6989586621679883002 l0
type Apply Nat a6989586621679997004 ((:!!$$) a6989586621679997004 l0) l1 # 
type Apply Nat a6989586621679997004 ((:!!$$) a6989586621679997004 l0) l1 = (:!!$$$) a6989586621679997004 l0 l1
type Apply Nat (TyFun Nat Nat -> *) (:^$) l0 # 
type Apply Nat (TyFun Nat Nat -> *) (:^$) l0 = (:^$$) l0
type Apply Nat (TyFun [a6989586621679997020] ([a6989586621679997020], [a6989586621679997020]) -> Type) (SplitAtSym0 a6989586621679997020) l0 # 
type Apply Nat (TyFun [a6989586621679997020] ([a6989586621679997020], [a6989586621679997020]) -> Type) (SplitAtSym0 a6989586621679997020) l0 = SplitAtSym1 a6989586621679997020 l0
type Apply Nat (TyFun [a6989586621679997022] [a6989586621679997022] -> Type) (TakeSym0 a6989586621679997022) l0 # 
type Apply Nat (TyFun [a6989586621679997022] [a6989586621679997022] -> Type) (TakeSym0 a6989586621679997022) l0 = TakeSym1 a6989586621679997022 l0
type Apply Nat (TyFun [a6989586621679997021] [a6989586621679997021] -> Type) (DropSym0 a6989586621679997021) l0 # 
type Apply Nat (TyFun [a6989586621679997021] [a6989586621679997021] -> Type) (DropSym0 a6989586621679997021) l0 = DropSym1 a6989586621679997021 l0
type Apply Nat (TyFun a6989586621679997006 [a6989586621679997006] -> Type) (ReplicateSym0 a6989586621679997006) l0 # 
type Apply Nat (TyFun a6989586621679997006 [a6989586621679997006] -> Type) (ReplicateSym0 a6989586621679997006) l0 = ReplicateSym1 a6989586621679997006 l0
type Apply a6989586621679997033 (TyFun [a6989586621679997033] (Maybe Nat) -> Type) (ElemIndexSym0 a6989586621679997033) l0 # 
type Apply a6989586621679997033 (TyFun [a6989586621679997033] (Maybe Nat) -> Type) (ElemIndexSym0 a6989586621679997033) l0 = ElemIndexSym1 a6989586621679997033 l0
type Apply a6989586621679997032 (TyFun [a6989586621679997032] [Nat] -> Type) (ElemIndicesSym0 a6989586621679997032) l0 # 
type Apply a6989586621679997032 (TyFun [a6989586621679997032] [Nat] -> Type) (ElemIndicesSym0 a6989586621679997032) l0 = ElemIndicesSym1 a6989586621679997032 l0
type Apply [a6989586621679997007] Nat (LengthSym0 a6989586621679997007) l0 # 
type Apply [a6989586621679997007] Nat (LengthSym0 a6989586621679997007) l0 = LengthSym1 a6989586621679997007 l0
type Apply [a6989586621679997033] (Maybe Nat) (ElemIndexSym1 a6989586621679997033 l0) l1 # 
type Apply [a6989586621679997033] (Maybe Nat) (ElemIndexSym1 a6989586621679997033 l0) l1 = ElemIndexSym2 a6989586621679997033 l0 l1
type Apply [a6989586621679997031] (Maybe Nat) (FindIndexSym1 a6989586621679997031 l0) l1 # 
type Apply [a6989586621679997031] (Maybe Nat) (FindIndexSym1 a6989586621679997031 l0) l1 = FindIndexSym2 a6989586621679997031 l0 l1
type Apply [a6989586621679997032] [Nat] (ElemIndicesSym1 a6989586621679997032 l0) l1 # 
type Apply [a6989586621679997032] [Nat] (ElemIndicesSym1 a6989586621679997032 l0) l1 = ElemIndicesSym2 a6989586621679997032 l0 l1
type Apply [a6989586621679997030] [Nat] (FindIndicesSym1 a6989586621679997030 l0) l1 # 
type Apply [a6989586621679997030] [Nat] (FindIndicesSym1 a6989586621679997030 l0) l1 = FindIndicesSym2 a6989586621679997030 l0 l1
type Apply [a6989586621679997004] (TyFun Nat a6989586621679997004 -> Type) ((:!!$) a6989586621679997004) l0 # 
type Apply [a6989586621679997004] (TyFun Nat a6989586621679997004 -> Type) ((:!!$) a6989586621679997004) l0 = (:!!$$) a6989586621679997004 l0
type Apply (TyFun a6989586621679997031 Bool -> Type) (TyFun [a6989586621679997031] (Maybe Nat) -> Type) (FindIndexSym0 a6989586621679997031) l0 # 
type Apply (TyFun a6989586621679997031 Bool -> Type) (TyFun [a6989586621679997031] (Maybe Nat) -> Type) (FindIndexSym0 a6989586621679997031) l0 = FindIndexSym1 a6989586621679997031 l0
type Apply (TyFun a6989586621679997030 Bool -> Type) (TyFun [a6989586621679997030] [Nat] -> Type) (FindIndicesSym0 a6989586621679997030) l0 # 
type Apply (TyFun a6989586621679997030 Bool -> Type) (TyFun [a6989586621679997030] [Nat] -> Type) (FindIndicesSym0 a6989586621679997030) l0 = FindIndicesSym1 a6989586621679997030 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 k06989586621679857097 k6989586621679857099 -> *) (ErrorSym0 k06989586621679857097 k6989586621679857099) # 

Methods

suppressUnusedWarnings :: Proxy (ErrorSym0 k06989586621679857097 k6989586621679857099) t -> () #

type Apply k06989586621679857097 k2 (ErrorSym0 k06989586621679857097 k2) l0 # 
type Apply k06989586621679857097 k2 (ErrorSym0 k06989586621679857097 k2) l0 = ErrorSym1 k2 k06989586621679857097 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 #