singletons-1.1.2: A framework for generating singleton types

Copyright (C) 2014 Jan Stolarek BSD-style (see LICENSE) Jan Stolarek (jan.stolarek@p.lodz.pl) experimental non-portable None Haskell2010

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_1627559874 = Apply (Let_1627559879GoSym3 k z a_1627559874) a_1627559874

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

type family Map a a :: [b] Source

Equations

 Map z `[]` = `[]` 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) Source

type family a :++ a :: [a] 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) Source

type family Id a :: a Source

Equations

 Id x = x

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

type family Const a a :: a Source

Equations

 Const x z = x

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

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

Equations

 (f :. g) a_1627559774 = Apply (Apply (Apply (Apply Lambda_1627559779Sym0 f) g) a_1627559774) a_1627559774

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

type family f \$ x :: b Source

Instances

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

type family f \$! x :: b Source

Instances

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

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

(%\$!) :: forall f x. Sing f -> Sing x -> Sing (((\$!\$) @@ f) @@ x) 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) Source

type family AsTypeOf a a :: a Source

Equations

 AsTypeOf a_1627559813 a_1627559815 = Apply (Apply ConstSym0 a_1627559813) a_1627559815

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

type family Seq a a :: b Source

Equations

 Seq z x = x

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

# Defunctionalization symbols

data FoldrSym0 l Source

Instances

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

data FoldrSym1 l l Source

Instances

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

data FoldrSym2 l l l Source

Instances

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

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) type Apply (TyFun [k] [k1] -> *) (TyFun k k1 -> *) (MapSym0 k k1) l0 = MapSym1 k k1 l0

data MapSym1 l l Source

Instances

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

type MapSym2 t t = Map t t Source

data (:++\$) l Source

Instances

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

data l :++\$\$ l Source

Instances

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

data IdSym0 l Source

Instances

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

type IdSym1 t = Id t Source

data ConstSym0 l Source

Instances

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

data ConstSym1 l l Source

Instances

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

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) type Apply (TyFun (TyFun k2 k -> *) (TyFun k2 k1 -> *) -> *) (TyFun k k1 -> *) ((:.\$) k k1 k2) l0 = (:.\$\$) k k1 k2 l0

data l :.\$\$ l Source

Instances

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

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

Instances

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

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

Instances

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

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

Instances

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

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

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

Instances

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

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) type Apply (TyFun k1 (TyFun k k2 -> *) -> *) (TyFun k (TyFun k1 k2 -> *) -> *) (FlipSym0 k k1 k2) l0 = FlipSym1 k k1 k2 l0

data FlipSym1 l l Source

Instances

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

data FlipSym2 l l l Source

Instances

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

data AsTypeOfSym0 l Source

Instances

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

data AsTypeOfSym1 l l Source

Instances

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

data SeqSym0 l Source

Instances

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

data SeqSym1 l l Source

Instances

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

type SeqSym2 t t = Seq t t Source