singletons-2.0.0.1: A framework for generating singleton types

Data.Singletons.Prelude.Base

Description

Implements singletonized versions of functions from `GHC.Base` module.

Because many of these definitions are produced by Template Haskell, it is not possible to create proper Haddock documentation. Please look up the corresponding operation in `Data.Tuple`. Also, please excuse the apparent repeated variable names. This is due to an interaction between Template Haskell and Haddock.

Synopsis

# Basic functions

type family Foldr a a a :: b Source

Equations

 Foldr k z a_1627631719 = Apply (Let1627631724GoSym3 k z a_1627631719) a_1627631719

sFoldr :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t :: b) Source

type family Map a a :: [b] Source

Equations

 Map _z_1627631698 `[]` = `[]` Map f ((:) x xs) = Apply (Apply (:\$) (Apply f x)) (Apply (Apply MapSym0 f) xs)

sMap :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply MapSym0 t) t :: [b]) Source

type family a :++ a :: [a] infixr 5 Source

Equations

 `[]` :++ ys = ys ((:) x xs) :++ ys = Apply (Apply (:\$) x) (Apply (Apply (:++\$) xs) ys)

(%:++) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:++\$) t) t :: [a]) infixr 5 Source

type family Otherwise :: Bool Source

Equations

 Otherwise = TrueSym0

type family Id a :: a Source

Equations

 Id x = x

sId :: forall t. Sing t -> Sing (Apply IdSym0 t :: a) Source

type family Const a a :: a Source

Equations

 Const x _z_1627631653 = x

sConst :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply ConstSym0 t) t :: a) Source

type family (a :. a) a :: c infixr 9 Source

Equations

 (f :. g) a_1627631616 = Apply (Apply (Apply (Apply Lambda_1627631621Sym0 f) g) a_1627631616) a_1627631616

(%:.) :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply (:.\$) t) t) t :: c) infixr 9 Source

type family f \$ x :: b infixr 0 Source

Instances

 type (\$) k k1 f x = (@@) k k1 f x Source

type family f \$! x :: b infixr 0 Source

Instances

 type (\$!) k k1 f x = (@@) k k1 f x Source

(%\$) :: forall f x. Sing f -> Sing x -> Sing (((\$\$) @@ f) @@ x) infixr 0 Source

(%\$!) :: forall f x. Sing f -> Sing x -> Sing (((\$!\$) @@ f) @@ x) infixr 0 Source

type family Flip a a a :: c Source

Equations

 Flip f x y = Apply (Apply f y) x

sFlip :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FlipSym0 t) t) t :: c) Source

type family AsTypeOf a a :: a Source

Equations

 AsTypeOf a_1627631656 a_1627631658 = Apply (Apply ConstSym0 a_1627631656) a_1627631658

sAsTypeOf :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply AsTypeOfSym0 t) t :: a) Source

type family Seq a a :: b infixr 0 Source

Equations

 Seq _z_1627631579 x = x

sSeq :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply SeqSym0 t) t :: b) infixr 0 Source

# Defunctionalization symbols

data FoldrSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun (TyFun k (TyFun k k -> *) -> *) (TyFun k (TyFun [k] k -> *) -> *) -> *) (FoldrSym0 k k) Source type Apply (TyFun k1 (TyFun [k] k1 -> *) -> *) (TyFun k (TyFun k1 k1 -> *) -> *) (FoldrSym0 k k1) l0 = FoldrSym1 k k1 l0 Source

data FoldrSym1 l l Source

Instances

 SuppressUnusedWarnings ((TyFun k (TyFun k k -> *) -> *) -> TyFun k (TyFun [k] k -> *) -> *) (FoldrSym1 k k) Source type Apply (TyFun [k1] k -> *) k (FoldrSym1 k1 k l1) l0 = FoldrSym2 k1 k l1 l0 Source

data FoldrSym2 l l l Source

Instances

 SuppressUnusedWarnings ((TyFun k (TyFun k k -> *) -> *) -> k -> TyFun [k] k -> *) (FoldrSym2 k k) Source type Apply k1 [k] (FoldrSym2 k k1 l1 l2) l0 = FoldrSym3 k k1 l1 l2 l0 Source

type FoldrSym3 t t t = Foldr t t t Source

data MapSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun (TyFun k k -> *) (TyFun [k] [k] -> *) -> *) (MapSym0 k k) Source type Apply (TyFun [k] [k1] -> *) (TyFun k k1 -> *) (MapSym0 k k1) l0 = MapSym1 k k1 l0 Source

data MapSym1 l l Source

Instances

 SuppressUnusedWarnings ((TyFun k k -> *) -> TyFun [k] [k] -> *) (MapSym1 k k) Source type Apply [k1] [k] (MapSym1 k k1 l1) l0 = MapSym2 k k1 l1 l0 Source

type MapSym2 t t = Map t t Source

data (:++\$) l Source

Instances

 SuppressUnusedWarnings (TyFun [k] (TyFun [k] [k] -> *) -> *) ((:++\$) k) Source type Apply (TyFun [k] [k] -> *) [k] ((:++\$) k) l0 = (:++\$\$) k l0 Source

data l :++\$\$ l Source

Instances

 SuppressUnusedWarnings ([k] -> TyFun [k] [k] -> *) ((:++\$\$) k) Source type Apply [k] [k] ((:++\$\$) k l1) l0 = (:++\$\$\$) k l1 l0 Source

type (:++\$\$\$) t t = (:++) t t Source

data IdSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun k k -> *) (IdSym0 k) Source type Apply k k (IdSym0 k) l0 = IdSym1 k l0 Source

type IdSym1 t = Id t Source

data ConstSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun k (TyFun k k -> *) -> *) (ConstSym0 k k) Source type Apply (TyFun k1 k -> *) k (ConstSym0 k k1) l0 = ConstSym1 k k1 l0 Source

data ConstSym1 l l Source

Instances

 SuppressUnusedWarnings (k -> TyFun k k -> *) (ConstSym1 k k) Source type Apply k1 k (ConstSym1 k1 k l1) l0 = ConstSym2 k1 k l1 l0 Source

type ConstSym2 t t = Const t t Source

data (:.\$) l Source

Instances

 SuppressUnusedWarnings (TyFun (TyFun k k -> *) (TyFun (TyFun k k -> *) (TyFun k k -> *) -> *) -> *) ((:.\$) k k k) Source type Apply (TyFun (TyFun k2 k -> *) (TyFun k2 k1 -> *) -> *) (TyFun k k1 -> *) ((:.\$) k k1 k2) l0 = (:.\$\$) k k1 k2 l0 Source

data l :.\$\$ l Source

Instances

 SuppressUnusedWarnings ((TyFun k k -> *) -> TyFun (TyFun k k -> *) (TyFun k k -> *) -> *) ((:.\$\$) k k k) Source type Apply (TyFun k k2 -> *) (TyFun k k1 -> *) ((:.\$\$) k1 k2 k l1) l0 = (:.\$\$\$) k1 k2 k l1 l0 Source

data (l :.\$\$\$ l) l Source

Instances

 SuppressUnusedWarnings ((TyFun k k -> *) -> (TyFun k k -> *) -> TyFun k k -> *) ((:.\$\$\$) k k k) Source type Apply k2 k ((:.\$\$\$) k1 k2 k l1 l2) l0 = (:.\$\$\$\$) k1 k2 k l1 l2 l0 Source

type (:.\$\$\$\$) t t t = (:.) t t t Source

data (\$\$) :: TyFun (TyFun a b -> *) (TyFun a b -> *) -> * Source

Instances

 type Apply (TyFun k k1 -> *) (TyFun k k1 -> *) ((\$\$) k k1) arg = (\$\$\$) k k1 arg Source

data (\$\$\$) :: (TyFun a b -> *) -> TyFun a b -> * Source

Instances

 type Apply k1 k ((\$\$\$) k k1 f) arg = (\$\$\$\$) k1 k f arg Source

type (\$\$\$\$) a b = (\$) a b Source

data (\$!\$) :: TyFun (TyFun a b -> *) (TyFun a b -> *) -> * Source

Instances

 type Apply (TyFun k k1 -> *) (TyFun k k1 -> *) ((\$!\$) k k1) arg = (\$!\$\$) k k1 arg Source

data (\$!\$\$) :: (TyFun a b -> *) -> TyFun a b -> * Source

Instances

 type Apply k1 k ((\$!\$\$) k k1 f) arg = (\$!\$\$\$) k1 k f arg Source

type (\$!\$\$\$) a b = (\$!) a b Source

data FlipSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun (TyFun k (TyFun k k -> *) -> *) (TyFun k (TyFun k k -> *) -> *) -> *) (FlipSym0 k k k) Source type Apply (TyFun k1 (TyFun k k2 -> *) -> *) (TyFun k (TyFun k1 k2 -> *) -> *) (FlipSym0 k k1 k2) l0 = FlipSym1 k k1 k2 l0 Source

data FlipSym1 l l Source

Instances

 SuppressUnusedWarnings ((TyFun k (TyFun k k -> *) -> *) -> TyFun k (TyFun k k -> *) -> *) (FlipSym1 k k k) Source type Apply (TyFun k1 k2 -> *) k (FlipSym1 k1 k k2 l1) l0 = FlipSym2 k1 k k2 l1 l0 Source

data FlipSym2 l l l Source

Instances

 SuppressUnusedWarnings ((TyFun k (TyFun k k -> *) -> *) -> k -> TyFun k k -> *) (FlipSym2 k k k) Source type Apply k2 k (FlipSym2 k k1 k2 l1 l2) l0 = FlipSym3 k k1 k2 l1 l2 l0 Source

type FlipSym3 t t t = Flip t t t Source

data AsTypeOfSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun k (TyFun k k -> *) -> *) (AsTypeOfSym0 k) Source type Apply (TyFun k k -> *) k (AsTypeOfSym0 k) l0 = AsTypeOfSym1 k l0 Source

data AsTypeOfSym1 l l Source

Instances

 SuppressUnusedWarnings (k -> TyFun k k -> *) (AsTypeOfSym1 k) Source type Apply k k (AsTypeOfSym1 k l1) l0 = AsTypeOfSym2 k l1 l0 Source

data SeqSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun k (TyFun k k -> *) -> *) (SeqSym0 k k) Source type Apply (TyFun k1 k1 -> *) k (SeqSym0 k k1) l0 = SeqSym1 k k1 l0 Source

data SeqSym1 l l Source

Instances

 SuppressUnusedWarnings (k -> TyFun k k -> *) (SeqSym1 k k) Source type Apply k k (SeqSym1 k1 k l1) l0 = SeqSym2 k1 k l1 l0 Source

type SeqSym2 t t = Seq t t Source