singletons-2.2: A framework for generating singleton types

Copyright(C) 2014 Jan Stolarek
LicenseBSD-style (see LICENSE)
MaintainerJan Stolarek (jan.stolarek@p.lodz.pl)
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Singletons.Prelude.Base

Contents

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_6989586621679482720 = Apply (Let6989586621679482725GoSym3 k z a_6989586621679482720) a_6989586621679482720 

sFoldr :: forall t t t. 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_6989586621679482699 '[] = '[] 
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]) #

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 t. Sing t -> Sing t -> Sing (Apply (Apply (:++$) t) t :: [a]) infixr 5 #

type family Otherwise :: Bool where ... #

Equations

Otherwise = TrueSym0 

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

Equations

Id x = x 

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

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

Equations

Const x _z_6989586621679482654 = x 

sConst :: forall t t. 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_6989586621679482617 = Apply (Apply (Apply (Apply Lambda_6989586621679482622Sym0 f) g) a_6989586621679482617) a_6989586621679482617 

(%:.) :: forall t t t. 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 k2 f x # 
type ($) k1 k2 f x = (@@) k1 k2 f x

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

Instances

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

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

(%$!) :: forall f x. 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 t t. 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_6989586621679482657 a_6989586621679482659 = Apply (Apply ConstSym0 a_6989586621679482657) a_6989586621679482659 

sAsTypeOf :: forall t t. 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_6989586621679482580 x = x 

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

Defunctionalization symbols

data FoldrSym0 l #

Instances

SuppressUnusedWarnings (TyFun (TyFun a6989586621679482539 (TyFun b6989586621679482540 b6989586621679482540 -> Type) -> Type) (TyFun b6989586621679482540 (TyFun [a6989586621679482539] b6989586621679482540 -> Type) -> Type) -> *) (FoldrSym0 a6989586621679482539 b6989586621679482540) # 

Methods

suppressUnusedWarnings :: Proxy (FoldrSym0 a6989586621679482539 b6989586621679482540) t -> () #

type Apply (TyFun a6989586621679482539 (TyFun b6989586621679482540 b6989586621679482540 -> Type) -> Type) (TyFun b6989586621679482540 (TyFun [a6989586621679482539] b6989586621679482540 -> Type) -> Type) (FoldrSym0 a6989586621679482539 b6989586621679482540) l0 # 
type Apply (TyFun a6989586621679482539 (TyFun b6989586621679482540 b6989586621679482540 -> Type) -> Type) (TyFun b6989586621679482540 (TyFun [a6989586621679482539] b6989586621679482540 -> Type) -> Type) (FoldrSym0 a6989586621679482539 b6989586621679482540) l0 = FoldrSym1 a6989586621679482539 b6989586621679482540 l0

data FoldrSym1 l l #

Instances

SuppressUnusedWarnings ((TyFun a6989586621679482539 (TyFun b6989586621679482540 b6989586621679482540 -> Type) -> Type) -> TyFun b6989586621679482540 (TyFun [a6989586621679482539] b6989586621679482540 -> Type) -> *) (FoldrSym1 a6989586621679482539 b6989586621679482540) # 

Methods

suppressUnusedWarnings :: Proxy (FoldrSym1 a6989586621679482539 b6989586621679482540) t -> () #

type Apply b6989586621679482540 (TyFun [a6989586621679482539] b6989586621679482540 -> Type) (FoldrSym1 a6989586621679482539 b6989586621679482540 l0) l1 # 
type Apply b6989586621679482540 (TyFun [a6989586621679482539] b6989586621679482540 -> Type) (FoldrSym1 a6989586621679482539 b6989586621679482540 l0) l1 = FoldrSym2 a6989586621679482539 b6989586621679482540 l0 l1

data FoldrSym2 l l l #

Instances

SuppressUnusedWarnings ((TyFun a6989586621679482539 (TyFun b6989586621679482540 b6989586621679482540 -> Type) -> Type) -> b6989586621679482540 -> TyFun [a6989586621679482539] b6989586621679482540 -> *) (FoldrSym2 a6989586621679482539 b6989586621679482540) # 

Methods

suppressUnusedWarnings :: Proxy (FoldrSym2 a6989586621679482539 b6989586621679482540) t -> () #

type Apply [a6989586621679482539] b6989586621679482540 (FoldrSym2 a6989586621679482539 b6989586621679482540 l1 l0) l2 # 
type Apply [a6989586621679482539] b6989586621679482540 (FoldrSym2 a6989586621679482539 b6989586621679482540 l1 l0) l2 = FoldrSym3 a6989586621679482539 b6989586621679482540 l1 l0 l2

type FoldrSym3 t t t = Foldr t t t #

data MapSym0 l #

Instances

SuppressUnusedWarnings (TyFun (TyFun a6989586621679482537 b6989586621679482538 -> Type) (TyFun [a6989586621679482537] [b6989586621679482538] -> Type) -> *) (MapSym0 a6989586621679482537 b6989586621679482538) # 

Methods

suppressUnusedWarnings :: Proxy (MapSym0 a6989586621679482537 b6989586621679482538) t -> () #

type Apply (TyFun a6989586621679482537 b6989586621679482538 -> Type) (TyFun [a6989586621679482537] [b6989586621679482538] -> Type) (MapSym0 a6989586621679482537 b6989586621679482538) l0 # 
type Apply (TyFun a6989586621679482537 b6989586621679482538 -> Type) (TyFun [a6989586621679482537] [b6989586621679482538] -> Type) (MapSym0 a6989586621679482537 b6989586621679482538) l0 = MapSym1 a6989586621679482537 b6989586621679482538 l0

data MapSym1 l l #

Instances

SuppressUnusedWarnings ((TyFun a6989586621679482537 b6989586621679482538 -> Type) -> TyFun [a6989586621679482537] [b6989586621679482538] -> *) (MapSym1 a6989586621679482537 b6989586621679482538) # 

Methods

suppressUnusedWarnings :: Proxy (MapSym1 a6989586621679482537 b6989586621679482538) t -> () #

type Apply [a6989586621679482537] [b6989586621679482538] (MapSym1 a6989586621679482537 b6989586621679482538 l0) l1 # 
type Apply [a6989586621679482537] [b6989586621679482538] (MapSym1 a6989586621679482537 b6989586621679482538 l0) l1 = MapSym2 a6989586621679482537 b6989586621679482538 l0 l1

type MapSym2 t t = Map t t #

data (:++$) l #

Instances

SuppressUnusedWarnings (TyFun [a6989586621679482536] (TyFun [a6989586621679482536] [a6989586621679482536] -> Type) -> *) ((:++$) a6989586621679482536) # 

Methods

suppressUnusedWarnings :: Proxy ((:++$) a6989586621679482536) t -> () #

type Apply [a6989586621679482536] (TyFun [a6989586621679482536] [a6989586621679482536] -> Type) ((:++$) a6989586621679482536) l0 # 
type Apply [a6989586621679482536] (TyFun [a6989586621679482536] [a6989586621679482536] -> Type) ((:++$) a6989586621679482536) l0 = (:++$$) a6989586621679482536 l0

data l :++$$ l #

Instances

SuppressUnusedWarnings ([a6989586621679482536] -> TyFun [a6989586621679482536] [a6989586621679482536] -> *) ((:++$$) a6989586621679482536) # 

Methods

suppressUnusedWarnings :: Proxy ((:++$$) a6989586621679482536) t -> () #

type Apply [a6989586621679482536] [a6989586621679482536] ((:++$$) a6989586621679482536 l0) l1 # 
type Apply [a6989586621679482536] [a6989586621679482536] ((:++$$) a6989586621679482536 l0) l1 = (:++$$$) a6989586621679482536 l0 l1

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

data IdSym0 l #

Instances

SuppressUnusedWarnings (TyFun a6989586621679482535 a6989586621679482535 -> *) (IdSym0 a6989586621679482535) # 

Methods

suppressUnusedWarnings :: Proxy (IdSym0 a6989586621679482535) t -> () #

type Apply a6989586621679482535 a6989586621679482535 (IdSym0 a6989586621679482535) l0 # 
type Apply a6989586621679482535 a6989586621679482535 (IdSym0 a6989586621679482535) l0 = IdSym1 a6989586621679482535 l0

type IdSym1 t = Id t #

data ConstSym0 l #

Instances

SuppressUnusedWarnings (TyFun a6989586621679482533 (TyFun b6989586621679482534 a6989586621679482533 -> Type) -> *) (ConstSym0 b6989586621679482534 a6989586621679482533) # 

Methods

suppressUnusedWarnings :: Proxy (ConstSym0 b6989586621679482534 a6989586621679482533) t -> () #

type Apply a6989586621679482533 (TyFun b6989586621679482534 a6989586621679482533 -> Type) (ConstSym0 b6989586621679482534 a6989586621679482533) l0 # 
type Apply a6989586621679482533 (TyFun b6989586621679482534 a6989586621679482533 -> Type) (ConstSym0 b6989586621679482534 a6989586621679482533) l0 = ConstSym1 b6989586621679482534 a6989586621679482533 l0

data ConstSym1 l l #

Instances

SuppressUnusedWarnings (a6989586621679482533 -> TyFun b6989586621679482534 a6989586621679482533 -> *) (ConstSym1 b6989586621679482534 a6989586621679482533) # 

Methods

suppressUnusedWarnings :: Proxy (ConstSym1 b6989586621679482534 a6989586621679482533) t -> () #

type Apply b6989586621679482534 a6989586621679482533 (ConstSym1 b6989586621679482534 a6989586621679482533 l0) l1 # 
type Apply b6989586621679482534 a6989586621679482533 (ConstSym1 b6989586621679482534 a6989586621679482533 l0) l1 = ConstSym2 b6989586621679482534 a6989586621679482533 l0 l1

type ConstSym2 t t = Const t t #

data (:.$) l #

Instances

SuppressUnusedWarnings (TyFun (TyFun b6989586621679482530 c6989586621679482531 -> Type) (TyFun (TyFun a6989586621679482532 b6989586621679482530 -> Type) (TyFun a6989586621679482532 c6989586621679482531 -> Type) -> Type) -> *) ((:.$) b6989586621679482530 a6989586621679482532 c6989586621679482531) # 

Methods

suppressUnusedWarnings :: Proxy ((b6989586621679482530 :.$ a6989586621679482532) c6989586621679482531) t -> () #

type Apply (TyFun b6989586621679482530 c6989586621679482531 -> Type) (TyFun (TyFun a6989586621679482532 b6989586621679482530 -> Type) (TyFun a6989586621679482532 c6989586621679482531 -> Type) -> Type) ((:.$) b6989586621679482530 a6989586621679482532 c6989586621679482531) l0 # 
type Apply (TyFun b6989586621679482530 c6989586621679482531 -> Type) (TyFun (TyFun a6989586621679482532 b6989586621679482530 -> Type) (TyFun a6989586621679482532 c6989586621679482531 -> Type) -> Type) ((:.$) b6989586621679482530 a6989586621679482532 c6989586621679482531) l0 = (:.$$) a6989586621679482532 b6989586621679482530 c6989586621679482531 l0

data l :.$$ l #

Instances

SuppressUnusedWarnings ((TyFun b6989586621679482530 c6989586621679482531 -> Type) -> TyFun (TyFun a6989586621679482532 b6989586621679482530 -> Type) (TyFun a6989586621679482532 c6989586621679482531 -> Type) -> *) ((:.$$) a6989586621679482532 b6989586621679482530 c6989586621679482531) # 

Methods

suppressUnusedWarnings :: Proxy ((a6989586621679482532 :.$$ b6989586621679482530) c6989586621679482531) t -> () #

type Apply (TyFun a6989586621679482532 b6989586621679482530 -> Type) (TyFun a6989586621679482532 c6989586621679482531 -> Type) ((:.$$) a6989586621679482532 b6989586621679482530 c6989586621679482531 l0) l1 # 
type Apply (TyFun a6989586621679482532 b6989586621679482530 -> Type) (TyFun a6989586621679482532 c6989586621679482531 -> Type) ((:.$$) a6989586621679482532 b6989586621679482530 c6989586621679482531 l0) l1 = (:.$$$) a6989586621679482532 b6989586621679482530 c6989586621679482531 l0 l1

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

Instances

SuppressUnusedWarnings ((TyFun b6989586621679482530 c6989586621679482531 -> Type) -> (TyFun a6989586621679482532 b6989586621679482530 -> Type) -> TyFun a6989586621679482532 c6989586621679482531 -> *) ((:.$$$) a6989586621679482532 b6989586621679482530 c6989586621679482531) # 

Methods

suppressUnusedWarnings :: Proxy ((a6989586621679482532 :.$$$ b6989586621679482530) c6989586621679482531) t -> () #

type Apply a6989586621679482532 c6989586621679482531 ((:.$$$) a6989586621679482532 b6989586621679482530 c6989586621679482531 l1 l0) l2 # 
type Apply a6989586621679482532 c6989586621679482531 ((:.$$$) a6989586621679482532 b6989586621679482530 c6989586621679482531 l1 l0) l2 = (:.$$$$) a6989586621679482532 b6989586621679482530 c6989586621679482531 l1 l0 l2

type (:.$$$$) t t t = (:.) 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 b (($$$) a b f) arg # 
type Apply a b (($$$) a b f) arg = ($$$$) a b 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 b (($!$$) a b f) arg # 
type Apply a b (($!$$) a b f) arg = ($!$$$) a b f arg

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

data FlipSym0 l #

Instances

SuppressUnusedWarnings (TyFun (TyFun a6989586621679482527 (TyFun b6989586621679482528 c6989586621679482529 -> Type) -> Type) (TyFun b6989586621679482528 (TyFun a6989586621679482527 c6989586621679482529 -> Type) -> Type) -> *) (FlipSym0 b6989586621679482528 a6989586621679482527 c6989586621679482529) # 

Methods

suppressUnusedWarnings :: Proxy (FlipSym0 b6989586621679482528 a6989586621679482527 c6989586621679482529) t -> () #

type Apply (TyFun a6989586621679482527 (TyFun b6989586621679482528 c6989586621679482529 -> Type) -> Type) (TyFun b6989586621679482528 (TyFun a6989586621679482527 c6989586621679482529 -> Type) -> Type) (FlipSym0 b6989586621679482528 a6989586621679482527 c6989586621679482529) l0 # 
type Apply (TyFun a6989586621679482527 (TyFun b6989586621679482528 c6989586621679482529 -> Type) -> Type) (TyFun b6989586621679482528 (TyFun a6989586621679482527 c6989586621679482529 -> Type) -> Type) (FlipSym0 b6989586621679482528 a6989586621679482527 c6989586621679482529) l0 = FlipSym1 a6989586621679482527 b6989586621679482528 c6989586621679482529 l0

data FlipSym1 l l #

Instances

SuppressUnusedWarnings ((TyFun a6989586621679482527 (TyFun b6989586621679482528 c6989586621679482529 -> Type) -> Type) -> TyFun b6989586621679482528 (TyFun a6989586621679482527 c6989586621679482529 -> Type) -> *) (FlipSym1 a6989586621679482527 b6989586621679482528 c6989586621679482529) # 

Methods

suppressUnusedWarnings :: Proxy (FlipSym1 a6989586621679482527 b6989586621679482528 c6989586621679482529) t -> () #

type Apply b6989586621679482528 (TyFun a6989586621679482527 c6989586621679482529 -> Type) (FlipSym1 a6989586621679482527 b6989586621679482528 c6989586621679482529 l0) l1 # 
type Apply b6989586621679482528 (TyFun a6989586621679482527 c6989586621679482529 -> Type) (FlipSym1 a6989586621679482527 b6989586621679482528 c6989586621679482529 l0) l1 = FlipSym2 a6989586621679482527 b6989586621679482528 c6989586621679482529 l0 l1

data FlipSym2 l l l #

Instances

SuppressUnusedWarnings ((TyFun a6989586621679482527 (TyFun b6989586621679482528 c6989586621679482529 -> Type) -> Type) -> b6989586621679482528 -> TyFun a6989586621679482527 c6989586621679482529 -> *) (FlipSym2 a6989586621679482527 b6989586621679482528 c6989586621679482529) # 

Methods

suppressUnusedWarnings :: Proxy (FlipSym2 a6989586621679482527 b6989586621679482528 c6989586621679482529) t -> () #

type Apply a6989586621679482527 c6989586621679482529 (FlipSym2 a6989586621679482527 b6989586621679482528 c6989586621679482529 l1 l0) l2 # 
type Apply a6989586621679482527 c6989586621679482529 (FlipSym2 a6989586621679482527 b6989586621679482528 c6989586621679482529 l1 l0) l2 = FlipSym3 a6989586621679482527 b6989586621679482528 c6989586621679482529 l1 l0 l2

type FlipSym3 t t t = Flip t t t #

data AsTypeOfSym0 l #

Instances

SuppressUnusedWarnings (TyFun a6989586621679482526 (TyFun a6989586621679482526 a6989586621679482526 -> Type) -> *) (AsTypeOfSym0 a6989586621679482526) # 

Methods

suppressUnusedWarnings :: Proxy (AsTypeOfSym0 a6989586621679482526) t -> () #

type Apply a6989586621679482526 (TyFun a6989586621679482526 a6989586621679482526 -> Type) (AsTypeOfSym0 a6989586621679482526) l0 # 
type Apply a6989586621679482526 (TyFun a6989586621679482526 a6989586621679482526 -> Type) (AsTypeOfSym0 a6989586621679482526) l0 = AsTypeOfSym1 a6989586621679482526 l0

data AsTypeOfSym1 l l #

Instances

SuppressUnusedWarnings (a6989586621679482526 -> TyFun a6989586621679482526 a6989586621679482526 -> *) (AsTypeOfSym1 a6989586621679482526) # 

Methods

suppressUnusedWarnings :: Proxy (AsTypeOfSym1 a6989586621679482526) t -> () #

type Apply a6989586621679482526 a6989586621679482526 (AsTypeOfSym1 a6989586621679482526 l0) l1 # 
type Apply a6989586621679482526 a6989586621679482526 (AsTypeOfSym1 a6989586621679482526 l0) l1 = AsTypeOfSym2 a6989586621679482526 l0 l1

type AsTypeOfSym2 t t = AsTypeOf t t #

data SeqSym0 l #

Instances

SuppressUnusedWarnings (TyFun a6989586621679482524 (TyFun b6989586621679482525 b6989586621679482525 -> Type) -> *) (SeqSym0 a6989586621679482524 b6989586621679482525) # 

Methods

suppressUnusedWarnings :: Proxy (SeqSym0 a6989586621679482524 b6989586621679482525) t -> () #

type Apply a6989586621679482524 (TyFun b6989586621679482525 b6989586621679482525 -> Type) (SeqSym0 a6989586621679482524 b6989586621679482525) l0 # 
type Apply a6989586621679482524 (TyFun b6989586621679482525 b6989586621679482525 -> Type) (SeqSym0 a6989586621679482524 b6989586621679482525) l0 = SeqSym1 b6989586621679482525 a6989586621679482524 l0

data SeqSym1 l l #

Instances

SuppressUnusedWarnings (a6989586621679482524 -> TyFun b6989586621679482525 b6989586621679482525 -> *) (SeqSym1 b6989586621679482525 a6989586621679482524) # 

Methods

suppressUnusedWarnings :: Proxy (SeqSym1 b6989586621679482525 a6989586621679482524) t -> () #

type Apply b6989586621679482525 b6989586621679482525 (SeqSym1 b6989586621679482525 a6989586621679482524 l0) l1 # 
type Apply b6989586621679482525 b6989586621679482525 (SeqSym1 b6989586621679482525 a6989586621679482524 l0) l1 = SeqSym2 b6989586621679482525 a6989586621679482524 l0 l1

type SeqSym2 t t = Seq t t #