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 ... #

Equations

Foldr k z a_1627672661 = Apply (Let1627672666GoSym3 k z a_1627672661) a_1627672661

sFoldr :: forall (t :: TyFun a (TyFun b b -> Type) -> Type) (t :: b) (t :: [a]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t :: b) #

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

Equations

Map _z_1627672640 '[] = '[]
Map f ((:) x xs) = Apply (Apply (:$) (Apply f x)) (Apply (Apply MapSym0 f) xs)

sMap :: forall (t :: TyFun a b -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply MapSym0 t) t :: [b]) #

type family (a :: [a]) :++ (a :: [a]) :: [a] where ... infixr 5 #

Equations

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

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

type family Otherwise :: Bool where ... #

Equations

Otherwise = TrueSym0

sOtherwise :: Sing (OtherwiseSym0 :: Bool) #

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

Equations

Id x = x

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

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

Equations

Const x _z_1627672595 = x

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

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

Equations

(f :. g) a_1627672558 = Apply (Apply (Apply (Apply Lambda_1627672563Sym0 f) g) a_1627672558) a_1627672558

(%:.) :: forall (t :: TyFun b c -> Type) (t :: TyFun a b -> Type) (t :: a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply (:.$) t) t) t :: c) infixr 9 #

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

Instances

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

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

Instances

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

(%$) :: forall (f :: TyFun a b -> *) (x :: a). Sing f -> Sing x -> Sing ((($$) @@ f) @@ x) infixr 0 #

(%$!) :: forall (f :: TyFun a b -> *) (x :: a). Sing f -> Sing x -> Sing ((($!$) @@ f) @@ x) infixr 0 #

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

Equations

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

sFlip :: forall (t :: TyFun a (TyFun b c -> Type) -> Type) (t :: b) (t :: a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FlipSym0 t) t) t :: c) #

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

Equations

AsTypeOf a_1627672598 a_1627672600 = Apply (Apply ConstSym0 a_1627672598) a_1627672600

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

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

Equations

Seq _z_1627672521 x = x

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

Defunctionalization symbols

data FoldrSym0 (l :: TyFun (TyFun a1627672480 (TyFun b1627672481 b1627672481 -> Type) -> Type) (TyFun b1627672481 (TyFun [a1627672480] b1627672481 -> Type) -> Type)) #

Instances

SuppressUnusedWarnings (TyFun (TyFun a1627672480 (TyFun b1627672481 b1627672481 -> Type) -> Type) (TyFun b1627672481 (TyFun [a1627672480] b1627672481 -> Type) -> Type) -> *) (FoldrSym0 a1627672480 b1627672481) #
Methods suppressUnusedWarnings :: Proxy (FoldrSym0 a1627672480 b1627672481) t -> () #
type Apply (TyFun a1627672480 (TyFun b1627672481 b1627672481 -> Type) -> Type) (TyFun b1627672481 (TyFun [a1627672480] b1627672481 -> Type) -> Type) (FoldrSym0 a1627672480 b1627672481) l #
type Apply (TyFun a1627672480 (TyFun b1627672481 b1627672481 -> Type) -> Type) (TyFun b1627672481 (TyFun [a1627672480] b1627672481 -> Type) -> Type) (FoldrSym0 a1627672480 b1627672481) l = FoldrSym1 a1627672480 b1627672481 l

data FoldrSym1 (l :: TyFun a1627672480 (TyFun b1627672481 b1627672481 -> Type) -> Type) (l :: TyFun b1627672481 (TyFun [a1627672480] b1627672481 -> Type)) #

Instances

SuppressUnusedWarnings ((TyFun a1627672480 (TyFun b1627672481 b1627672481 -> Type) -> Type) -> TyFun b1627672481 (TyFun [a1627672480] b1627672481 -> Type) -> *) (FoldrSym1 a1627672480 b1627672481) #
Methods suppressUnusedWarnings :: Proxy (FoldrSym1 a1627672480 b1627672481) t -> () #
type Apply b1627672481 (TyFun [a1627672480] b1627672481 -> Type) (FoldrSym1 a1627672480 b1627672481 l1) l2 #
type Apply b1627672481 (TyFun [a1627672480] b1627672481 -> Type) (FoldrSym1 a1627672480 b1627672481 l1) l2 = FoldrSym2 a1627672480 b1627672481 l1 l2

data FoldrSym2 (l :: TyFun a1627672480 (TyFun b1627672481 b1627672481 -> Type) -> Type) (l :: b1627672481) (l :: TyFun [a1627672480] b1627672481) #

Instances

SuppressUnusedWarnings ((TyFun a1627672480 (TyFun b1627672481 b1627672481 -> Type) -> Type) -> b1627672481 -> TyFun [a1627672480] b1627672481 -> *) (FoldrSym2 a1627672480 b1627672481) #
Methods suppressUnusedWarnings :: Proxy (FoldrSym2 a1627672480 b1627672481) t -> () #
type Apply [a] b (FoldrSym2 a b l1 l2) l3 #
type Apply [a] b (FoldrSym2 a b l1 l2) l3 = Foldr a b l1 l2 l3

type FoldrSym3 (t :: TyFun a1627672480 (TyFun b1627672481 b1627672481 -> Type) -> Type) (t :: b1627672481) (t :: [a1627672480]) = Foldr t t t #

data MapSym0 (l :: TyFun (TyFun a1627672478 b1627672479 -> Type) (TyFun [a1627672478] [b1627672479] -> Type)) #

Instances

SuppressUnusedWarnings (TyFun (TyFun a1627672478 b1627672479 -> Type) (TyFun [a1627672478] [b1627672479] -> Type) -> *) (MapSym0 a1627672478 b1627672479) #
Methods suppressUnusedWarnings :: Proxy (MapSym0 a1627672478 b1627672479) t -> () #
type Apply (TyFun a1627672478 b1627672479 -> Type) (TyFun [a1627672478] [b1627672479] -> Type) (MapSym0 a1627672478 b1627672479) l #
type Apply (TyFun a1627672478 b1627672479 -> Type) (TyFun [a1627672478] [b1627672479] -> Type) (MapSym0 a1627672478 b1627672479) l = MapSym1 a1627672478 b1627672479 l

data MapSym1 (l :: TyFun a1627672478 b1627672479 -> Type) (l :: TyFun [a1627672478] [b1627672479]) #

Instances

SuppressUnusedWarnings ((TyFun a1627672478 b1627672479 -> Type) -> TyFun [a1627672478] [b1627672479] -> *) (MapSym1 a1627672478 b1627672479) #
Methods suppressUnusedWarnings :: Proxy (MapSym1 a1627672478 b1627672479) t -> () #
type Apply [a] [b] (MapSym1 a b l1) l2 #
type Apply [a] [b] (MapSym1 a b l1) l2 = Map a b l1 l2

type MapSym2 (t :: TyFun a1627672478 b1627672479 -> Type) (t :: [a1627672478]) = Map t t #

data (:++$) (l :: TyFun [a1627672477] (TyFun [a1627672477] [a1627672477] -> Type)) #

Instances

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

data (l :: [a1627672477]) :++$$ (l :: TyFun [a1627672477] [a1627672477]) #

Instances

SuppressUnusedWarnings ([a1627672477] -> TyFun [a1627672477] [a1627672477] -> *) ((:++$$) a1627672477) #
Methods suppressUnusedWarnings :: Proxy ((:++$$) a1627672477) t -> () #
type Apply [a] [a] ((:++$$) a l1) l2 #
type Apply [a] [a] ((:++$$) a l1) l2 = (:++) a l1 l2

type (:++$$$) (t :: [a1627672477]) (t :: [a1627672477]) = (:++) t t #

type OtherwiseSym0 = Otherwise #

data IdSym0 (l :: TyFun a1627672476 a1627672476) #

Instances

SuppressUnusedWarnings (TyFun a1627672476 a1627672476 -> *) (IdSym0 a1627672476) #
Methods suppressUnusedWarnings :: Proxy (IdSym0 a1627672476) t -> () #
type Apply a a (IdSym0 a) l #
type Apply a a (IdSym0 a) l = Id a l

type IdSym1 (t :: a1627672476) = Id t #

data ConstSym0 (l :: TyFun a1627672474 (TyFun b1627672475 a1627672474 -> Type)) #

Instances

SuppressUnusedWarnings (TyFun a1627672474 (TyFun b1627672475 a1627672474 -> Type) -> *) (ConstSym0 b1627672475 a1627672474) #
Methods suppressUnusedWarnings :: Proxy (ConstSym0 b1627672475 a1627672474) t -> () #
type Apply a1627672474 (TyFun b1627672475 a1627672474 -> Type) (ConstSym0 b1627672475 a1627672474) l #
type Apply a1627672474 (TyFun b1627672475 a1627672474 -> Type) (ConstSym0 b1627672475 a1627672474) l = ConstSym1 b1627672475 a1627672474 l

data ConstSym1 (l :: a1627672474) (l :: TyFun b1627672475 a1627672474) #

Instances

SuppressUnusedWarnings (a1627672474 -> TyFun b1627672475 a1627672474 -> *) (ConstSym1 b1627672475 a1627672474) #
Methods suppressUnusedWarnings :: Proxy (ConstSym1 b1627672475 a1627672474) t -> () #
type Apply b a (ConstSym1 b a l1) l2 #
type Apply b a (ConstSym1 b a l1) l2 = Const b a l1 l2

type ConstSym2 (t :: a1627672474) (t :: b1627672475) = Const t t #

data (:.$) (l :: TyFun (TyFun b1627672471 c1627672472 -> Type) (TyFun (TyFun a1627672473 b1627672471 -> Type) (TyFun a1627672473 c1627672472 -> Type) -> Type)) #

Instances

SuppressUnusedWarnings (TyFun (TyFun b1627672471 c1627672472 -> Type) (TyFun (TyFun a1627672473 b1627672471 -> Type) (TyFun a1627672473 c1627672472 -> Type) -> Type) -> *) ((:.$) b1627672471 a1627672473 c1627672472) #
Methods suppressUnusedWarnings :: Proxy ((b1627672471 :.$ a1627672473) c1627672472) t -> () #
type Apply (TyFun b1627672471 c1627672472 -> Type) (TyFun (TyFun a1627672473 b1627672471 -> Type) (TyFun a1627672473 c1627672472 -> Type) -> Type) ((:.$) b1627672471 a1627672473 c1627672472) l #
type Apply (TyFun b1627672471 c1627672472 -> Type) (TyFun (TyFun a1627672473 b1627672471 -> Type) (TyFun a1627672473 c1627672472 -> Type) -> Type) ((:.$) b1627672471 a1627672473 c1627672472) l = (:.$$) b1627672471 a1627672473 c1627672472 l

data (l :: TyFun b1627672471 c1627672472 -> Type) :.$$ (l :: TyFun (TyFun a1627672473 b1627672471 -> Type) (TyFun a1627672473 c1627672472 -> Type)) #

Instances

SuppressUnusedWarnings ((TyFun b1627672471 c1627672472 -> Type) -> TyFun (TyFun a1627672473 b1627672471 -> Type) (TyFun a1627672473 c1627672472 -> Type) -> *) ((:.$$) b1627672471 a1627672473 c1627672472) #
Methods suppressUnusedWarnings :: Proxy ((b1627672471 :.$$ a1627672473) c1627672472) t -> () #
type Apply (TyFun a1627672473 b1627672471 -> Type) (TyFun a1627672473 c1627672472 -> Type) ((:.$$) b1627672471 a1627672473 c1627672472 l1) l2 #
type Apply (TyFun a1627672473 b1627672471 -> Type) (TyFun a1627672473 c1627672472 -> Type) ((:.$$) b1627672471 a1627672473 c1627672472 l1) l2 = (:.$$$) b1627672471 a1627672473 c1627672472 l1 l2

data ((l :: TyFun b1627672471 c1627672472 -> Type) :.$$$ (l :: TyFun a1627672473 b1627672471 -> Type)) (l :: TyFun a1627672473 c1627672472) #

Instances

SuppressUnusedWarnings ((TyFun b1627672471 c1627672472 -> Type) -> (TyFun a1627672473 b1627672471 -> Type) -> TyFun a1627672473 c1627672472 -> *) ((:.$$$) b1627672471 a1627672473 c1627672472) #
Methods suppressUnusedWarnings :: Proxy ((b1627672471 :.$$$ a1627672473) c1627672472) t -> () #
type Apply a c ((:.$$$) b a c l1 l2) l3 #
type Apply a c ((:.$$$) b a c l1 l2) l3 = (:.) b a c l1 l2 l3

type (:.$$$$) (t :: TyFun b1627672471 c1627672472 -> Type) (t :: TyFun a1627672473 b1627672471 -> Type) (t :: a1627672473) = (:.) t t t #

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

Instances

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

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

Instances

type Apply a k (($$$) a k f) arg #
type Apply a k (($$$) a k f) arg = ($$$$) a k f arg

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

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

Instances

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

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

Instances

type Apply a k (($!$$) a k f) arg #
type Apply a k (($!$$) a k f) arg = ($!$$$) a k f arg

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

data FlipSym0 (l :: TyFun (TyFun a1627672468 (TyFun b1627672469 c1627672470 -> Type) -> Type) (TyFun b1627672469 (TyFun a1627672468 c1627672470 -> Type) -> Type)) #

Instances

SuppressUnusedWarnings (TyFun (TyFun a1627672468 (TyFun b1627672469 c1627672470 -> Type) -> Type) (TyFun b1627672469 (TyFun a1627672468 c1627672470 -> Type) -> Type) -> *) (FlipSym0 b1627672469 a1627672468 c1627672470) #
Methods suppressUnusedWarnings :: Proxy (FlipSym0 b1627672469 a1627672468 c1627672470) t -> () #
type Apply (TyFun a1627672468 (TyFun b1627672469 c1627672470 -> Type) -> Type) (TyFun b1627672469 (TyFun a1627672468 c1627672470 -> Type) -> Type) (FlipSym0 b1627672469 a1627672468 c1627672470) l #
type Apply (TyFun a1627672468 (TyFun b1627672469 c1627672470 -> Type) -> Type) (TyFun b1627672469 (TyFun a1627672468 c1627672470 -> Type) -> Type) (FlipSym0 b1627672469 a1627672468 c1627672470) l = FlipSym1 b1627672469 a1627672468 c1627672470 l

data FlipSym1 (l :: TyFun a1627672468 (TyFun b1627672469 c1627672470 -> Type) -> Type) (l :: TyFun b1627672469 (TyFun a1627672468 c1627672470 -> Type)) #

Instances

SuppressUnusedWarnings ((TyFun a1627672468 (TyFun b1627672469 c1627672470 -> Type) -> Type) -> TyFun b1627672469 (TyFun a1627672468 c1627672470 -> Type) -> *) (FlipSym1 b1627672469 a1627672468 c1627672470) #
Methods suppressUnusedWarnings :: Proxy (FlipSym1 b1627672469 a1627672468 c1627672470) t -> () #
type Apply b1627672469 (TyFun a1627672468 c1627672470 -> Type) (FlipSym1 b1627672469 a1627672468 c1627672470 l1) l2 #
type Apply b1627672469 (TyFun a1627672468 c1627672470 -> Type) (FlipSym1 b1627672469 a1627672468 c1627672470 l1) l2 = FlipSym2 b1627672469 a1627672468 c1627672470 l1 l2

data FlipSym2 (l :: TyFun a1627672468 (TyFun b1627672469 c1627672470 -> Type) -> Type) (l :: b1627672469) (l :: TyFun a1627672468 c1627672470) #

Instances

SuppressUnusedWarnings ((TyFun a1627672468 (TyFun b1627672469 c1627672470 -> Type) -> Type) -> b1627672469 -> TyFun a1627672468 c1627672470 -> *) (FlipSym2 b1627672469 a1627672468 c1627672470) #
Methods suppressUnusedWarnings :: Proxy (FlipSym2 b1627672469 a1627672468 c1627672470) t -> () #
type Apply a c (FlipSym2 b a c l1 l2) l3 #
type Apply a c (FlipSym2 b a c l1 l2) l3 = Flip b a c l1 l2 l3

type FlipSym3 (t :: TyFun a1627672468 (TyFun b1627672469 c1627672470 -> Type) -> Type) (t :: b1627672469) (t :: a1627672468) = Flip t t t #

data AsTypeOfSym0 (l :: TyFun a1627672467 (TyFun a1627672467 a1627672467 -> Type)) #

Instances

SuppressUnusedWarnings (TyFun a1627672467 (TyFun a1627672467 a1627672467 -> Type) -> *) (AsTypeOfSym0 a1627672467) #
Methods suppressUnusedWarnings :: Proxy (AsTypeOfSym0 a1627672467) t -> () #
type Apply a1627672467 (TyFun a1627672467 a1627672467 -> Type) (AsTypeOfSym0 a1627672467) l #
type Apply a1627672467 (TyFun a1627672467 a1627672467 -> Type) (AsTypeOfSym0 a1627672467) l = AsTypeOfSym1 a1627672467 l

data AsTypeOfSym1 (l :: a1627672467) (l :: TyFun a1627672467 a1627672467) #

Instances

SuppressUnusedWarnings (a1627672467 -> TyFun a1627672467 a1627672467 -> *) (AsTypeOfSym1 a1627672467) #
Methods suppressUnusedWarnings :: Proxy (AsTypeOfSym1 a1627672467) t -> () #
type Apply a a (AsTypeOfSym1 a l1) l2 #
type Apply a a (AsTypeOfSym1 a l1) l2 = AsTypeOf a l1 l2

type AsTypeOfSym2 (t :: a1627672467) (t :: a1627672467) = AsTypeOf t t #

data SeqSym0 (l :: TyFun a1627672465 (TyFun b1627672466 b1627672466 -> Type)) #

Instances

SuppressUnusedWarnings (TyFun a1627672465 (TyFun b1627672466 b1627672466 -> Type) -> *) (SeqSym0 a1627672465 b1627672466) #
Methods suppressUnusedWarnings :: Proxy (SeqSym0 a1627672465 b1627672466) t -> () #
type Apply a1627672465 (TyFun b1627672466 b1627672466 -> Type) (SeqSym0 a1627672465 b1627672466) l #
type Apply a1627672465 (TyFun b1627672466 b1627672466 -> Type) (SeqSym0 a1627672465 b1627672466) l = SeqSym1 a1627672465 b1627672466 l

data SeqSym1 (l :: a1627672465) (l :: TyFun b1627672466 b1627672466) #

Instances

SuppressUnusedWarnings (a1627672465 -> TyFun b1627672466 b1627672466 -> *) (SeqSym1 a1627672465 b1627672466) #
Methods suppressUnusedWarnings :: Proxy (SeqSym1 a1627672465 b1627672466) t -> () #
type Apply b b (SeqSym1 a b l1) l2 #
type Apply b b (SeqSym1 a b l1) l2 = Seq a b l1 l2

type SeqSym2 (t :: a1627672465) (t :: b1627672466) = Seq t t #