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 :: TyFun a (TyFun b b -> Type) -> Type) (a :: b) (a :: [a]) :: b where ... Source #

Equations

Foldr k z a_1627796838 = Apply (Let1627796843GoSym3 k z a_1627796838) a_1627796838

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 :: TyFun a b -> Type) (a :: [a]) :: [b] where ... Source #

Equations

Map _z_1627796817 '[] = '[]
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 :: [a]) :: [a] where ... 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 where ... Source #

Equations

Otherwise = TrueSym0

sOtherwise :: Sing (OtherwiseSym0 :: Bool) Source #

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

Equations

Id x = x

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

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

Equations

Const x _z_1627796772 = x

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

type family ((a :: TyFun b c -> Type) :. (a :: TyFun a b -> Type)) (a :: a) :: c where ... infixr 9 Source #

Equations

(f :. g) a_1627796735 = Apply (Apply (Apply (Apply Lambda_1627796740Sym0 f) g) a_1627796735) a_1627796735

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

type family (f :: TyFun a b -> *) $ (x :: a) :: b infixr 0 Source #

Instances

type ($) k1 k2 f x Source #
type ($) k1 k2 f x = (@@) k1 k2 f x

type family (f :: TyFun a b -> *) $! (x :: a) :: b infixr 0 Source #

Instances

type ($!) k1 k2 f x Source #
type ($!) k1 k2 f x = (@@) k1 k2 f x

(%$) :: 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 :: TyFun a (TyFun b c -> Type) -> Type) (a :: b) (a :: a) :: c where ... 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 :: a) :: a where ... Source #

Equations

AsTypeOf a_1627796775 a_1627796777 = Apply (Apply ConstSym0 a_1627796775) a_1627796777

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

type family Seq (a :: a) (a :: b) :: b where ... infixr 0 Source #

Equations

Seq _z_1627796698 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 a1627796657 (TyFun b1627796658 b1627796658 -> Type) -> Type) (TyFun b1627796658 (TyFun [a1627796657] b1627796658 -> Type) -> Type) -> *) (FoldrSym0 a1627796657 b1627796658) Source #
Methods suppressUnusedWarnings :: Proxy (FoldrSym0 a1627796657 b1627796658) t -> () Source #
type Apply (TyFun a1627796657 (TyFun b1627796658 b1627796658 -> Type) -> Type) (TyFun b1627796658 (TyFun [a1627796657] b1627796658 -> Type) -> Type) (FoldrSym0 a1627796657 b1627796658) l0 Source #
type Apply (TyFun a1627796657 (TyFun b1627796658 b1627796658 -> Type) -> Type) (TyFun b1627796658 (TyFun [a1627796657] b1627796658 -> Type) -> Type) (FoldrSym0 a1627796657 b1627796658) l0 = FoldrSym1 a1627796657 b1627796658 l0

data FoldrSym1 l l Source #

Instances

SuppressUnusedWarnings ((TyFun a1627796657 (TyFun b1627796658 b1627796658 -> Type) -> Type) -> TyFun b1627796658 (TyFun [a1627796657] b1627796658 -> Type) -> *) (FoldrSym1 a1627796657 b1627796658) Source #
Methods suppressUnusedWarnings :: Proxy (FoldrSym1 a1627796657 b1627796658) t -> () Source #
type Apply b1627796658 (TyFun [a1627796657] b1627796658 -> Type) (FoldrSym1 a1627796657 b1627796658 l1) l0 Source #
type Apply b1627796658 (TyFun [a1627796657] b1627796658 -> Type) (FoldrSym1 a1627796657 b1627796658 l1) l0 = FoldrSym2 a1627796657 b1627796658 l1 l0

data FoldrSym2 l l l Source #

Instances

SuppressUnusedWarnings ((TyFun a1627796657 (TyFun b1627796658 b1627796658 -> Type) -> Type) -> b1627796658 -> TyFun [a1627796657] b1627796658 -> *) (FoldrSym2 a1627796657 b1627796658) Source #
Methods suppressUnusedWarnings :: Proxy (FoldrSym2 a1627796657 b1627796658) t -> () Source #
type Apply [a1627796657] b1627796658 (FoldrSym2 a1627796657 b1627796658 l1 l2) l0 Source #
type Apply [a1627796657] b1627796658 (FoldrSym2 a1627796657 b1627796658 l1 l2) l0 = FoldrSym3 a1627796657 b1627796658 l1 l2 l0

type FoldrSym3 t t t = Foldr t t t Source #

data MapSym0 l Source #

Instances

SuppressUnusedWarnings (TyFun (TyFun a1627796655 b1627796656 -> Type) (TyFun [a1627796655] [b1627796656] -> Type) -> *) (MapSym0 a1627796655 b1627796656) Source #
Methods suppressUnusedWarnings :: Proxy (MapSym0 a1627796655 b1627796656) t -> () Source #
type Apply (TyFun a1627796655 b1627796656 -> Type) (TyFun [a1627796655] [b1627796656] -> Type) (MapSym0 a1627796655 b1627796656) l0 Source #
type Apply (TyFun a1627796655 b1627796656 -> Type) (TyFun [a1627796655] [b1627796656] -> Type) (MapSym0 a1627796655 b1627796656) l0 = MapSym1 a1627796655 b1627796656 l0

data MapSym1 l l Source #

Instances

SuppressUnusedWarnings ((TyFun a1627796655 b1627796656 -> Type) -> TyFun [a1627796655] [b1627796656] -> *) (MapSym1 a1627796655 b1627796656) Source #
Methods suppressUnusedWarnings :: Proxy (MapSym1 a1627796655 b1627796656) t -> () Source #
type Apply [a1627796655] [b1627796656] (MapSym1 a1627796655 b1627796656 l1) l0 Source #
type Apply [a1627796655] [b1627796656] (MapSym1 a1627796655 b1627796656 l1) l0 = MapSym2 a1627796655 b1627796656 l1 l0

type MapSym2 t t = Map t t Source #

data (:++$) l Source #

Instances

SuppressUnusedWarnings (TyFun [a1627796654] (TyFun [a1627796654] [a1627796654] -> Type) -> *) ((:++$) a1627796654) Source #
Methods suppressUnusedWarnings :: Proxy ((:++$) a1627796654) t -> () Source #
type Apply [a1627796654] (TyFun [a1627796654] [a1627796654] -> Type) ((:++$) a1627796654) l0 Source #
type Apply [a1627796654] (TyFun [a1627796654] [a1627796654] -> Type) ((:++$) a1627796654) l0 = (:++$$) a1627796654 l0

data l :++$$ l Source #

Instances

SuppressUnusedWarnings ([a1627796654] -> TyFun [a1627796654] [a1627796654] -> *) ((:++$$) a1627796654) Source #
Methods suppressUnusedWarnings :: Proxy ((:++$$) a1627796654) t -> () Source #
type Apply [a1627796654] [a1627796654] ((:++$$) a1627796654 l1) l0 Source #
type Apply [a1627796654] [a1627796654] ((:++$$) a1627796654 l1) l0 = (:++$$$) a1627796654 l1 l0

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

type OtherwiseSym0 = Otherwise Source #

data IdSym0 l Source #

Instances

SuppressUnusedWarnings (TyFun a1627796653 a1627796653 -> *) (IdSym0 a1627796653) Source #
Methods suppressUnusedWarnings :: Proxy (IdSym0 a1627796653) t -> () Source #
type Apply a1627796653 a1627796653 (IdSym0 a1627796653) l0 Source #
type Apply a1627796653 a1627796653 (IdSym0 a1627796653) l0 = IdSym1 a1627796653 l0

type IdSym1 t = Id t Source #

data ConstSym0 l Source #

Instances

SuppressUnusedWarnings (TyFun a1627796651 (TyFun b1627796652 a1627796651 -> Type) -> *) (ConstSym0 b1627796652 a1627796651) Source #
Methods suppressUnusedWarnings :: Proxy (ConstSym0 b1627796652 a1627796651) t -> () Source #
type Apply a1627796651 (TyFun b1627796652 a1627796651 -> Type) (ConstSym0 b1627796652 a1627796651) l0 Source #
type Apply a1627796651 (TyFun b1627796652 a1627796651 -> Type) (ConstSym0 b1627796652 a1627796651) l0 = ConstSym1 b1627796652 a1627796651 l0

data ConstSym1 l l Source #

Instances

SuppressUnusedWarnings (a1627796651 -> TyFun b1627796652 a1627796651 -> *) (ConstSym1 b1627796652 a1627796651) Source #
Methods suppressUnusedWarnings :: Proxy (ConstSym1 b1627796652 a1627796651) t -> () Source #
type Apply b1627796652 a1627796651 (ConstSym1 b1627796652 a1627796651 l1) l0 Source #
type Apply b1627796652 a1627796651 (ConstSym1 b1627796652 a1627796651 l1) l0 = ConstSym2 a1627796651 b1627796652 l1 l0

type ConstSym2 t t = Const t t Source #

data (:.$) l Source #

Instances

SuppressUnusedWarnings (TyFun (TyFun b1627796648 c1627796649 -> Type) (TyFun (TyFun a1627796650 b1627796648 -> Type) (TyFun a1627796650 c1627796649 -> Type) -> Type) -> *) ((:.$) b1627796648 a1627796650 c1627796649) Source #
Methods suppressUnusedWarnings :: Proxy ((b1627796648 :.$ a1627796650) c1627796649) t -> () Source #
type Apply (TyFun b1627796648 c1627796649 -> Type) (TyFun (TyFun a1627796650 b1627796648 -> Type) (TyFun a1627796650 c1627796649 -> Type) -> Type) ((:.$) b1627796648 a1627796650 c1627796649) l0 Source #
type Apply (TyFun b1627796648 c1627796649 -> Type) (TyFun (TyFun a1627796650 b1627796648 -> Type) (TyFun a1627796650 c1627796649 -> Type) -> Type) ((:.$) b1627796648 a1627796650 c1627796649) l0 = (:.$$) a1627796650 b1627796648 c1627796649 l0

data l :.$$ l Source #

Instances

SuppressUnusedWarnings ((TyFun b1627796648 c1627796649 -> Type) -> TyFun (TyFun a1627796650 b1627796648 -> Type) (TyFun a1627796650 c1627796649 -> Type) -> *) ((:.$$) a1627796650 b1627796648 c1627796649) Source #
Methods suppressUnusedWarnings :: Proxy ((a1627796650 :.$$ b1627796648) c1627796649) t -> () Source #
type Apply (TyFun a1627796650 b1627796648 -> Type) (TyFun a1627796650 c1627796649 -> Type) ((:.$$) a1627796650 b1627796648 c1627796649 l1) l0 Source #
type Apply (TyFun a1627796650 b1627796648 -> Type) (TyFun a1627796650 c1627796649 -> Type) ((:.$$) a1627796650 b1627796648 c1627796649 l1) l0 = (:.$$$) a1627796650 b1627796648 c1627796649 l1 l0

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

Instances

SuppressUnusedWarnings ((TyFun b1627796648 c1627796649 -> Type) -> (TyFun a1627796650 b1627796648 -> Type) -> TyFun a1627796650 c1627796649 -> *) ((:.$$$) a1627796650 b1627796648 c1627796649) Source #
Methods suppressUnusedWarnings :: Proxy ((a1627796650 :.$$$ b1627796648) c1627796649) t -> () Source #
type Apply a1627796650 c1627796649 ((:.$$$) a1627796650 b1627796648 c1627796649 l1 l2) l0 Source #
type Apply a1627796650 c1627796649 ((:.$$$) a1627796650 b1627796648 c1627796649 l1 l2) l0 = (:.$$$$) b1627796648 c1627796649 a1627796650 l1 l2 l0

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

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

Instances

type Apply (TyFun a b -> ) (TyFun a b -> ) (($$) a b) arg Source #
type Apply (TyFun a b -> ) (TyFun a b -> ) (($$) a b) arg = ($$$) a b arg

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

Instances

type Apply a b (($$$) a b f) arg Source #
type Apply a b (($$$) a b f) arg = ($$$$) a b f arg

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

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

Instances

type Apply (TyFun a b -> ) (TyFun a b -> ) (($!$) a b) arg Source #
type Apply (TyFun a b -> ) (TyFun a b -> ) (($!$) a b) arg = ($!$$) a b arg

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

Instances

type Apply a b (($!$$) a b f) arg Source #
type Apply a b (($!$$) a b f) arg = ($!$$$) a b f arg

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

data FlipSym0 l Source #

Instances

SuppressUnusedWarnings (TyFun (TyFun a1627796645 (TyFun b1627796646 c1627796647 -> Type) -> Type) (TyFun b1627796646 (TyFun a1627796645 c1627796647 -> Type) -> Type) -> *) (FlipSym0 b1627796646 a1627796645 c1627796647) Source #
Methods suppressUnusedWarnings :: Proxy (FlipSym0 b1627796646 a1627796645 c1627796647) t -> () Source #
type Apply (TyFun a1627796645 (TyFun b1627796646 c1627796647 -> Type) -> Type) (TyFun b1627796646 (TyFun a1627796645 c1627796647 -> Type) -> Type) (FlipSym0 b1627796646 a1627796645 c1627796647) l0 Source #
type Apply (TyFun a1627796645 (TyFun b1627796646 c1627796647 -> Type) -> Type) (TyFun b1627796646 (TyFun a1627796645 c1627796647 -> Type) -> Type) (FlipSym0 b1627796646 a1627796645 c1627796647) l0 = FlipSym1 a1627796645 b1627796646 c1627796647 l0

data FlipSym1 l l Source #

Instances

SuppressUnusedWarnings ((TyFun a1627796645 (TyFun b1627796646 c1627796647 -> Type) -> Type) -> TyFun b1627796646 (TyFun a1627796645 c1627796647 -> Type) -> *) (FlipSym1 a1627796645 b1627796646 c1627796647) Source #
Methods suppressUnusedWarnings :: Proxy (FlipSym1 a1627796645 b1627796646 c1627796647) t -> () Source #
type Apply b1627796646 (TyFun a1627796645 c1627796647 -> Type) (FlipSym1 a1627796645 b1627796646 c1627796647 l1) l0 Source #
type Apply b1627796646 (TyFun a1627796645 c1627796647 -> Type) (FlipSym1 a1627796645 b1627796646 c1627796647 l1) l0 = FlipSym2 a1627796645 b1627796646 c1627796647 l1 l0

data FlipSym2 l l l Source #

Instances

SuppressUnusedWarnings ((TyFun a1627796645 (TyFun b1627796646 c1627796647 -> Type) -> Type) -> b1627796646 -> TyFun a1627796645 c1627796647 -> *) (FlipSym2 a1627796645 b1627796646 c1627796647) Source #
Methods suppressUnusedWarnings :: Proxy (FlipSym2 a1627796645 b1627796646 c1627796647) t -> () Source #
type Apply a1627796645 c1627796647 (FlipSym2 a1627796645 b1627796646 c1627796647 l1 l2) l0 Source #
type Apply a1627796645 c1627796647 (FlipSym2 a1627796645 b1627796646 c1627796647 l1 l2) l0 = FlipSym3 a1627796645 b1627796646 c1627796647 l1 l2 l0

type FlipSym3 t t t = Flip t t t Source #

data AsTypeOfSym0 l Source #

Instances

SuppressUnusedWarnings (TyFun a1627796644 (TyFun a1627796644 a1627796644 -> Type) -> *) (AsTypeOfSym0 a1627796644) Source #
Methods suppressUnusedWarnings :: Proxy (AsTypeOfSym0 a1627796644) t -> () Source #
type Apply a1627796644 (TyFun a1627796644 a1627796644 -> Type) (AsTypeOfSym0 a1627796644) l0 Source #
type Apply a1627796644 (TyFun a1627796644 a1627796644 -> Type) (AsTypeOfSym0 a1627796644) l0 = AsTypeOfSym1 a1627796644 l0

data AsTypeOfSym1 l l Source #

Instances

SuppressUnusedWarnings (a1627796644 -> TyFun a1627796644 a1627796644 -> *) (AsTypeOfSym1 a1627796644) Source #
Methods suppressUnusedWarnings :: Proxy (AsTypeOfSym1 a1627796644) t -> () Source #
type Apply a1627796644 a1627796644 (AsTypeOfSym1 a1627796644 l1) l0 Source #
type Apply a1627796644 a1627796644 (AsTypeOfSym1 a1627796644 l1) l0 = AsTypeOfSym2 a1627796644 l1 l0

type AsTypeOfSym2 t t = AsTypeOf t t Source #

data SeqSym0 l Source #

Instances

SuppressUnusedWarnings (TyFun a1627796642 (TyFun b1627796643 b1627796643 -> Type) -> *) (SeqSym0 a1627796642 b1627796643) Source #
Methods suppressUnusedWarnings :: Proxy (SeqSym0 a1627796642 b1627796643) t -> () Source #
type Apply a1627796642 (TyFun b1627796643 b1627796643 -> Type) (SeqSym0 a1627796642 b1627796643) l0 Source #
type Apply a1627796642 (TyFun b1627796643 b1627796643 -> Type) (SeqSym0 a1627796642 b1627796643) l0 = SeqSym1 b1627796643 a1627796642 l0

data SeqSym1 l l Source #

Instances

SuppressUnusedWarnings (a1627796642 -> TyFun b1627796643 b1627796643 -> *) (SeqSym1 b1627796643 a1627796642) Source #
Methods suppressUnusedWarnings :: Proxy (SeqSym1 b1627796643 a1627796642) t -> () Source #
type Apply b1627796643 b1627796643 (SeqSym1 b1627796643 a1627796642 l1) l0 Source #
type Apply b1627796643 b1627796643 (SeqSym1 b1627796643 a1627796642 l1) l0 = SeqSym2 a1627796642 b1627796643 l1 l0

type SeqSym2 t t = Seq t t Source #