Copyright	(C) 2014 Jan Stolarek
License	BSD-style (see LICENSE)
Maintainer	Jan Stolarek (jan.stolarek@p.lodz.pl)
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.Prelude.Base

Contents

Basic functions
Defunctionalization symbols

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_1627752769 = Apply (Let1627752774GoSym3 k z a_1627752769) a_1627752769

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_1627752748 `[]` = `[]`
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

sOtherwise :: Sing (OtherwiseSym0 :: Bool) Source

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_1627752703 = 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_1627752666 = Apply (Apply (Apply (Apply Lambda_1627752671Sym0 f) g) a_1627752666) a_1627752666

(%:.) :: 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_1627752706 a_1627752708 = Apply (Apply ConstSym0 a_1627752706) a_1627752708

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_1627752629 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

type OtherwiseSym0 = Otherwise 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

type AsTypeOfSym2 t t = AsTypeOf t t 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