Data.Singletons.Prelude

Basic singleton definitions

data family Sing (a :: k)

Singleton type synonyms

type SBool

type SList

type SMaybe

type SEither

type SOrdering

type STuple0

type STuple2

type STuple3

type STuple4

type STuple5

type STuple6

type STuple7

Functions working with Bool

type family If k (cond :: Bool) (tru :: k) (fls :: k) :: k where ...

sIf

type family Not (a :: Bool) :: Bool where ...

sNot

type family (a :: Bool) :&& (a :: Bool) :: Bool where ...

type family (a :: Bool) :|| (a :: Bool) :: Bool where ...

(%:&&)

(%:||)

type family Otherwise :: Bool where ...

sOtherwise

Error reporting

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

data ErrorSym0 l

sError

Singleton equality

Singleton comparisons

Singleton Enum and Bounded

Singletons numbers

Miscellaneous functions

type family Id (a :: a) :: a where ...

sId

type family Const (a :: a) (a :: b) :: a where ...

sConst

type family ((a :: TyFun b c -> Type) :. (a :: TyFun a b -> Type)) (a :: a) :: c where ...

(%:.)

type family (f :: TyFun a b -> *) $ (x :: a) :: b

(%$)

type family (f :: TyFun a b -> *) $! (x :: a) :: b

(%$!)

type family Flip (a :: TyFun a (TyFun b c -> Type) -> Type) (a :: b) (a :: a) :: c where ...

sFlip

type family AsTypeOf (a :: a) (a :: a) :: a where ...

sAsTypeOf

type family Seq (a :: a) (a :: b) :: b where ...

sSeq

List operations

type family Map (a :: TyFun a b -> Type) (a :: [a]) :: [b] where ...

sMap

type family (a :: [a]) :++ (a :: [a]) :: [a] where ...

(%:++)

type family Head (a :: [a]) :: a where ...

sHead

type family Last (a :: [a]) :: a where ...

sLast

type family Tail (a :: [a]) :: [a] where ...

sTail

type family Init (a :: [a]) :: [a] where ...

sInit

type family Null (a :: [a]) :: Bool where ...

sNull

type family Reverse (a :: [a]) :: [a] where ...

sReverse

Reducing lists (folds)

type family Foldl (a :: TyFun b (TyFun a b -> Type) -> Type) (a :: b) (a :: [a]) :: b where ...

sFoldl

type family Foldl1 (a :: TyFun a (TyFun a a -> Type) -> Type) (a :: [a]) :: a where ...

sFoldl1

type family Foldr (a :: TyFun a (TyFun b b -> Type) -> Type) (a :: b) (a :: [a]) :: b where ...

sFoldr

type family Foldr1 (a :: TyFun a (TyFun a a -> Type) -> Type) (a :: [a]) :: a where ...

sFoldr1

Special folds

type family And (a :: [Bool]) :: Bool where ...

sAnd

type family Or (a :: [Bool]) :: Bool where ...

sOr

type family Any_ (a :: TyFun a Bool -> Type) (a :: [a]) :: Bool where ...

sAny_

type family All (a :: TyFun a Bool -> Type) (a :: [a]) :: Bool where ...

sAll

type family Concat (a :: [[a]]) :: [a] where ...

sConcat

type family ConcatMap (a :: TyFun a [b] -> Type) (a :: [a]) :: [b] where ...

sConcatMap

Scans

type family Scanl (a :: TyFun b (TyFun a b -> Type) -> Type) (a :: b) (a :: [a]) :: [b] where ...

sScanl

type family Scanl1 (a :: TyFun a (TyFun a a -> Type) -> Type) (a :: [a]) :: [a] where ...

sScanl1

type family Scanr (a :: TyFun a (TyFun b b -> Type) -> Type) (a :: b) (a :: [a]) :: [b] where ...

sScanr

type family Scanr1 (a :: TyFun a (TyFun a a -> Type) -> Type) (a :: [a]) :: [a] where ...

sScanr1

Searching lists

type family Elem (a :: a) (a :: [a]) :: Bool where ...

sElem

type family NotElem (a :: a) (a :: [a]) :: Bool where ...

sNotElem

type family Lookup (a :: a) (a :: [(a, b)]) :: Maybe b where ...

sLookup

Zipping and unzipping lists

type family Zip (a :: [a]) (a :: [b]) :: [(a, b)] where ...

sZip

type family Zip3 (a :: [a]) (a :: [b]) (a :: [c]) :: [(a, b, c)] where ...

sZip3

type family ZipWith (a :: TyFun a (TyFun b c -> Type) -> Type) (a :: [a]) (a :: [b]) :: [c] where ...

sZipWith

type family ZipWith3 (a :: TyFun a (TyFun b (TyFun c d -> Type) -> Type) -> Type) (a :: [a]) (a :: [b]) (a :: [c]) :: [d] where ...

sZipWith3

type family Unzip (a :: [(a, b)]) :: ([a], [b]) where ...

sUnzip

type family Unzip3 (a :: [(a, b, c)]) :: ([a], [b], [c]) where ...

sUnzip3

Other datatypes

type family Maybe_ (a :: b) (a :: TyFun a b -> Type) (a :: Maybe a) :: b where ...

sMaybe_

type family Either_ (a :: TyFun a c -> Type) (a :: TyFun b c -> Type) (a :: Either a b) :: c where ...

sEither_

type family Fst (a :: (a, b)) :: a where ...

sFst

type family Snd (a :: (a, b)) :: b where ...

sSnd

type family Curry (a :: TyFun (a, b) c -> Type) (a :: a) (a :: b) :: c where ...

sCurry

type family Uncurry (a :: TyFun a (TyFun b c -> Type) -> Type) (a :: (a, b)) :: c where ...

sUncurry

data Symbol

Other functions

either_

maybe_

bool_

any_

Defunctionalization symbols

type FalseSym0

type TrueSym0

data NotSym0 l

type NotSym1 t

data (:&&$) l

data l :&&$$ l

type t :&&$$$ t

data (:||$) l

data l :||$$ l

type t :||$$$ t

type OtherwiseSym0

type NothingSym0

data JustSym0 l

type JustSym1 t

data Maybe_Sym0 l

data Maybe_Sym1 l l

data Maybe_Sym2 l l l

type Maybe_Sym3 t t t

data LeftSym0 l

type LeftSym1 t

data RightSym0 l

type RightSym1 t

data Either_Sym0 l

data Either_Sym1 l l

data Either_Sym2 l l l

type Either_Sym3 t t t

type Tuple0Sym0

data Tuple2Sym0 l

data Tuple2Sym1 l l

type Tuple2Sym2 t t

data Tuple3Sym0 l

data Tuple3Sym1 l l

data Tuple3Sym2 l l l

type Tuple3Sym3 t t t

data Tuple4Sym0 l

data Tuple4Sym1 l l

data Tuple4Sym2 l l l

data Tuple4Sym3 l l l l

type Tuple4Sym4 t t t t

data Tuple5Sym0 l

data Tuple5Sym1 l l

data Tuple5Sym2 l l l

data Tuple5Sym3 l l l l

data Tuple5Sym4 l l l l l

type Tuple5Sym5 t t t t t

data Tuple6Sym0 l

data Tuple6Sym1 l l

data Tuple6Sym2 l l l

data Tuple6Sym3 l l l l

data Tuple6Sym4 l l l l l

data Tuple6Sym5 l l l l l l

type Tuple6Sym6 t t t t t t

data Tuple7Sym0 l

data Tuple7Sym1 l l

data Tuple7Sym2 l l l

data Tuple7Sym3 l l l l

data Tuple7Sym4 l l l l l

data Tuple7Sym5 l l l l l l

data Tuple7Sym6 l l l l l l l

type Tuple7Sym7 t t t t t t t

data FstSym0 l

type FstSym1 t

data SndSym0 l

type SndSym1 t

data CurrySym0 l

data CurrySym1 l l

data CurrySym2 l l l

type CurrySym3 t t t

data UncurrySym0 l

data UncurrySym1 l l

type UncurrySym2 t t

data IdSym0 l

type IdSym1 t

data ConstSym0 l

data ConstSym1 l l

type ConstSym2 t t

data (:.$) l

data l :.$$ l

data (l :.$$$ l) l

data ($$)

data ($$$)

type a $$$$ b

data ($!$)

data ($!$$)

type a $!$$$ b

data FlipSym0 l

data FlipSym1 l l

data FlipSym2 l l l

data AsTypeOfSym0 l

data AsTypeOfSym1 l l

type AsTypeOfSym2 t t

data SeqSym0 l

data SeqSym1 l l

type SeqSym2 t t

data (:$) l

data l :$$ l

type t :$$$ t

type NilSym0

data MapSym0 l

data MapSym1 l l

type MapSym2 t t

data ReverseSym0 l

type ReverseSym1 t

data l :++$$ l

data (:++$) l

data HeadSym0 l

type HeadSym1 t

data LastSym0 l

type LastSym1 t

data TailSym0 l

type TailSym1 t

data InitSym0 l

type InitSym1 t

data NullSym0 l

type NullSym1 t

data FoldlSym0 l

data FoldlSym1 l l

data FoldlSym2 l l l

type FoldlSym3 t t t

data Foldl1Sym0 l

data Foldl1Sym1 l l

type Foldl1Sym2 t t

data FoldrSym0 l

data FoldrSym1 l l

data FoldrSym2 l l l

type FoldrSym3 t t t

data Foldr1Sym0 l

data Foldr1Sym1 l l

type Foldr1Sym2 t t

data ConcatSym0 l

type ConcatSym1 t

data ConcatMapSym0 l

data ConcatMapSym1 l l

type ConcatMapSym2 t t

data AndSym0 l

type AndSym1 t

data OrSym0 l

type OrSym1 t

data Any_Sym0 l

data Any_Sym1 l l

type Any_Sym2 t t

data AllSym0 l

data AllSym1 l l

type AllSym2 t t

data ScanlSym0 l

data ScanlSym1 l l

data ScanlSym2 l l l

type ScanlSym3 t t t

data Scanl1Sym0 l

data Scanl1Sym1 l l

type Scanl1Sym2 t t

data ScanrSym0 l

data ScanrSym1 l l

data ScanrSym2 l l l

type ScanrSym3 t t t

data Scanr1Sym0 l

data Scanr1Sym1 l l

type Scanr1Sym2 t t

data ElemSym0 l

data ElemSym1 l l

type ElemSym2 t t

data NotElemSym0 l

data NotElemSym1 l l

type NotElemSym2 t t

data ZipSym0 l

data ZipSym1 l l

type ZipSym2 t t

data Zip3Sym0 l

data Zip3Sym1 l l

data Zip3Sym2 l l l

type Zip3Sym3 t t t

data ZipWithSym0 l

data ZipWithSym1 l l

data ZipWithSym2 l l l

type ZipWithSym3 t t t

data ZipWith3Sym0 l

data ZipWith3Sym1 l l

data ZipWith3Sym2 l l l

data ZipWith3Sym3 l l l l

data UnzipSym0 l

type UnzipSym1 t