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_6989586621679703582 = Apply (Let6989586621679703587GoSym3 k z a_6989586621679703582) a_6989586621679703582 

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_6989586621679703561 '[] = '[] 
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_6989586621679703516 = 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_6989586621679703479 = Apply (Apply (Apply (Apply Lambda_6989586621679703484Sym0 f) g) a_6989586621679703479) a_6989586621679703479 

(%:.) :: 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_6989586621679703519 a_6989586621679703521 = Apply (Apply ConstSym0 a_6989586621679703519) a_6989586621679703521 

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_6989586621679703442 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 a6989586621679703401 (TyFun b6989586621679703402 b6989586621679703402 -> Type) -> Type) (TyFun b6989586621679703402 (TyFun [a6989586621679703401] b6989586621679703402 -> Type) -> Type) -> *) (FoldrSym0 a6989586621679703401 b6989586621679703402) # 

Methods

suppressUnusedWarnings :: Proxy (FoldrSym0 a6989586621679703401 b6989586621679703402) t -> () #

type Apply (TyFun a6989586621679703401 (TyFun b6989586621679703402 b6989586621679703402 -> Type) -> Type) (TyFun b6989586621679703402 (TyFun [a6989586621679703401] b6989586621679703402 -> Type) -> Type) (FoldrSym0 a6989586621679703401 b6989586621679703402) l0 # 
type Apply (TyFun a6989586621679703401 (TyFun b6989586621679703402 b6989586621679703402 -> Type) -> Type) (TyFun b6989586621679703402 (TyFun [a6989586621679703401] b6989586621679703402 -> Type) -> Type) (FoldrSym0 a6989586621679703401 b6989586621679703402) l0 = FoldrSym1 a6989586621679703401 b6989586621679703402 l0

data FoldrSym1 l l #

Instances

SuppressUnusedWarnings ((TyFun a6989586621679703401 (TyFun b6989586621679703402 b6989586621679703402 -> Type) -> Type) -> TyFun b6989586621679703402 (TyFun [a6989586621679703401] b6989586621679703402 -> Type) -> *) (FoldrSym1 a6989586621679703401 b6989586621679703402) # 

Methods

suppressUnusedWarnings :: Proxy (FoldrSym1 a6989586621679703401 b6989586621679703402) t -> () #

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

data FoldrSym2 l l l #

Instances

SuppressUnusedWarnings ((TyFun a6989586621679703401 (TyFun b6989586621679703402 b6989586621679703402 -> Type) -> Type) -> b6989586621679703402 -> TyFun [a6989586621679703401] b6989586621679703402 -> *) (FoldrSym2 a6989586621679703401 b6989586621679703402) # 

Methods

suppressUnusedWarnings :: Proxy (FoldrSym2 a6989586621679703401 b6989586621679703402) t -> () #

type Apply [a6989586621679703401] b6989586621679703402 (FoldrSym2 a6989586621679703401 b6989586621679703402 l1 l0) l2 # 
type Apply [a6989586621679703401] b6989586621679703402 (FoldrSym2 a6989586621679703401 b6989586621679703402 l1 l0) l2 = FoldrSym3 a6989586621679703401 b6989586621679703402 l1 l0 l2

type FoldrSym3 t t t = Foldr t t t #

data MapSym0 l #

Instances

SuppressUnusedWarnings (TyFun (TyFun a6989586621679703399 b6989586621679703400 -> Type) (TyFun [a6989586621679703399] [b6989586621679703400] -> Type) -> *) (MapSym0 a6989586621679703399 b6989586621679703400) # 

Methods

suppressUnusedWarnings :: Proxy (MapSym0 a6989586621679703399 b6989586621679703400) t -> () #

type Apply (TyFun a6989586621679703399 b6989586621679703400 -> Type) (TyFun [a6989586621679703399] [b6989586621679703400] -> Type) (MapSym0 a6989586621679703399 b6989586621679703400) l0 # 
type Apply (TyFun a6989586621679703399 b6989586621679703400 -> Type) (TyFun [a6989586621679703399] [b6989586621679703400] -> Type) (MapSym0 a6989586621679703399 b6989586621679703400) l0 = MapSym1 a6989586621679703399 b6989586621679703400 l0

data MapSym1 l l #

Instances

SuppressUnusedWarnings ((TyFun a6989586621679703399 b6989586621679703400 -> Type) -> TyFun [a6989586621679703399] [b6989586621679703400] -> *) (MapSym1 a6989586621679703399 b6989586621679703400) # 

Methods

suppressUnusedWarnings :: Proxy (MapSym1 a6989586621679703399 b6989586621679703400) t -> () #

type Apply [a6989586621679703399] [b6989586621679703400] (MapSym1 a6989586621679703399 b6989586621679703400 l0) l1 # 
type Apply [a6989586621679703399] [b6989586621679703400] (MapSym1 a6989586621679703399 b6989586621679703400 l0) l1 = MapSym2 a6989586621679703399 b6989586621679703400 l0 l1

type MapSym2 t t = Map t t #

data (:++$) l #

Instances

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

Methods

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

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

data l :++$$ l #

Instances

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

Methods

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

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

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

data IdSym0 l #

Instances

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

Methods

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

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

type IdSym1 t = Id t #

data ConstSym0 l #

Instances

SuppressUnusedWarnings (TyFun a6989586621679703395 (TyFun b6989586621679703396 a6989586621679703395 -> Type) -> *) (ConstSym0 b6989586621679703396 a6989586621679703395) # 

Methods

suppressUnusedWarnings :: Proxy (ConstSym0 b6989586621679703396 a6989586621679703395) t -> () #

type Apply a6989586621679703395 (TyFun b6989586621679703396 a6989586621679703395 -> Type) (ConstSym0 b6989586621679703396 a6989586621679703395) l0 # 
type Apply a6989586621679703395 (TyFun b6989586621679703396 a6989586621679703395 -> Type) (ConstSym0 b6989586621679703396 a6989586621679703395) l0 = ConstSym1 b6989586621679703396 a6989586621679703395 l0

data ConstSym1 l l #

Instances

SuppressUnusedWarnings (a6989586621679703395 -> TyFun b6989586621679703396 a6989586621679703395 -> *) (ConstSym1 b6989586621679703396 a6989586621679703395) # 

Methods

suppressUnusedWarnings :: Proxy (ConstSym1 b6989586621679703396 a6989586621679703395) t -> () #

type Apply b6989586621679703396 a6989586621679703395 (ConstSym1 b6989586621679703396 a6989586621679703395 l0) l1 # 
type Apply b6989586621679703396 a6989586621679703395 (ConstSym1 b6989586621679703396 a6989586621679703395 l0) l1 = ConstSym2 b6989586621679703396 a6989586621679703395 l0 l1

type ConstSym2 t t = Const t t #

data (:.$) l #

Instances

SuppressUnusedWarnings (TyFun (TyFun b6989586621679703392 c6989586621679703393 -> Type) (TyFun (TyFun a6989586621679703394 b6989586621679703392 -> Type) (TyFun a6989586621679703394 c6989586621679703393 -> Type) -> Type) -> *) ((:.$) b6989586621679703392 a6989586621679703394 c6989586621679703393) # 

Methods

suppressUnusedWarnings :: Proxy ((b6989586621679703392 :.$ a6989586621679703394) c6989586621679703393) t -> () #

type Apply (TyFun b6989586621679703392 c6989586621679703393 -> Type) (TyFun (TyFun a6989586621679703394 b6989586621679703392 -> Type) (TyFun a6989586621679703394 c6989586621679703393 -> Type) -> Type) ((:.$) b6989586621679703392 a6989586621679703394 c6989586621679703393) l0 # 
type Apply (TyFun b6989586621679703392 c6989586621679703393 -> Type) (TyFun (TyFun a6989586621679703394 b6989586621679703392 -> Type) (TyFun a6989586621679703394 c6989586621679703393 -> Type) -> Type) ((:.$) b6989586621679703392 a6989586621679703394 c6989586621679703393) l0 = (:.$$) a6989586621679703394 b6989586621679703392 c6989586621679703393 l0

data l :.$$ l #

Instances

SuppressUnusedWarnings ((TyFun b6989586621679703392 c6989586621679703393 -> Type) -> TyFun (TyFun a6989586621679703394 b6989586621679703392 -> Type) (TyFun a6989586621679703394 c6989586621679703393 -> Type) -> *) ((:.$$) a6989586621679703394 b6989586621679703392 c6989586621679703393) # 

Methods

suppressUnusedWarnings :: Proxy ((a6989586621679703394 :.$$ b6989586621679703392) c6989586621679703393) t -> () #

type Apply (TyFun a6989586621679703394 b6989586621679703392 -> Type) (TyFun a6989586621679703394 c6989586621679703393 -> Type) ((:.$$) a6989586621679703394 b6989586621679703392 c6989586621679703393 l0) l1 # 
type Apply (TyFun a6989586621679703394 b6989586621679703392 -> Type) (TyFun a6989586621679703394 c6989586621679703393 -> Type) ((:.$$) a6989586621679703394 b6989586621679703392 c6989586621679703393 l0) l1 = (:.$$$) a6989586621679703394 b6989586621679703392 c6989586621679703393 l0 l1

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

Instances

SuppressUnusedWarnings ((TyFun b6989586621679703392 c6989586621679703393 -> Type) -> (TyFun a6989586621679703394 b6989586621679703392 -> Type) -> TyFun a6989586621679703394 c6989586621679703393 -> *) ((:.$$$) a6989586621679703394 b6989586621679703392 c6989586621679703393) # 

Methods

suppressUnusedWarnings :: Proxy ((a6989586621679703394 :.$$$ b6989586621679703392) c6989586621679703393) t -> () #

type Apply a6989586621679703394 c6989586621679703393 ((:.$$$) a6989586621679703394 b6989586621679703392 c6989586621679703393 l1 l0) l2 # 
type Apply a6989586621679703394 c6989586621679703393 ((:.$$$) a6989586621679703394 b6989586621679703392 c6989586621679703393 l1 l0) l2 = (:.$$$$) a6989586621679703394 b6989586621679703392 c6989586621679703393 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 a6989586621679703389 (TyFun b6989586621679703390 c6989586621679703391 -> Type) -> Type) (TyFun b6989586621679703390 (TyFun a6989586621679703389 c6989586621679703391 -> Type) -> Type) -> *) (FlipSym0 b6989586621679703390 a6989586621679703389 c6989586621679703391) # 

Methods

suppressUnusedWarnings :: Proxy (FlipSym0 b6989586621679703390 a6989586621679703389 c6989586621679703391) t -> () #

type Apply (TyFun a6989586621679703389 (TyFun b6989586621679703390 c6989586621679703391 -> Type) -> Type) (TyFun b6989586621679703390 (TyFun a6989586621679703389 c6989586621679703391 -> Type) -> Type) (FlipSym0 b6989586621679703390 a6989586621679703389 c6989586621679703391) l0 # 
type Apply (TyFun a6989586621679703389 (TyFun b6989586621679703390 c6989586621679703391 -> Type) -> Type) (TyFun b6989586621679703390 (TyFun a6989586621679703389 c6989586621679703391 -> Type) -> Type) (FlipSym0 b6989586621679703390 a6989586621679703389 c6989586621679703391) l0 = FlipSym1 a6989586621679703389 b6989586621679703390 c6989586621679703391 l0

data FlipSym1 l l #

Instances

SuppressUnusedWarnings ((TyFun a6989586621679703389 (TyFun b6989586621679703390 c6989586621679703391 -> Type) -> Type) -> TyFun b6989586621679703390 (TyFun a6989586621679703389 c6989586621679703391 -> Type) -> *) (FlipSym1 a6989586621679703389 b6989586621679703390 c6989586621679703391) # 

Methods

suppressUnusedWarnings :: Proxy (FlipSym1 a6989586621679703389 b6989586621679703390 c6989586621679703391) t -> () #

type Apply b6989586621679703390 (TyFun a6989586621679703389 c6989586621679703391 -> Type) (FlipSym1 a6989586621679703389 b6989586621679703390 c6989586621679703391 l0) l1 # 
type Apply b6989586621679703390 (TyFun a6989586621679703389 c6989586621679703391 -> Type) (FlipSym1 a6989586621679703389 b6989586621679703390 c6989586621679703391 l0) l1 = FlipSym2 a6989586621679703389 b6989586621679703390 c6989586621679703391 l0 l1

data FlipSym2 l l l #

Instances

SuppressUnusedWarnings ((TyFun a6989586621679703389 (TyFun b6989586621679703390 c6989586621679703391 -> Type) -> Type) -> b6989586621679703390 -> TyFun a6989586621679703389 c6989586621679703391 -> *) (FlipSym2 a6989586621679703389 b6989586621679703390 c6989586621679703391) # 

Methods

suppressUnusedWarnings :: Proxy (FlipSym2 a6989586621679703389 b6989586621679703390 c6989586621679703391) t -> () #

type Apply a6989586621679703389 c6989586621679703391 (FlipSym2 a6989586621679703389 b6989586621679703390 c6989586621679703391 l1 l0) l2 # 
type Apply a6989586621679703389 c6989586621679703391 (FlipSym2 a6989586621679703389 b6989586621679703390 c6989586621679703391 l1 l0) l2 = FlipSym3 a6989586621679703389 b6989586621679703390 c6989586621679703391 l1 l0 l2

type FlipSym3 t t t = Flip t t t #

data AsTypeOfSym0 l #

Instances

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

Methods

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

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

data AsTypeOfSym1 l l #

Instances

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

Methods

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

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

type AsTypeOfSym2 t t = AsTypeOf t t #

data SeqSym0 l #

Instances

SuppressUnusedWarnings (TyFun a6989586621679703386 (TyFun b6989586621679703387 b6989586621679703387 -> Type) -> *) (SeqSym0 a6989586621679703386 b6989586621679703387) # 

Methods

suppressUnusedWarnings :: Proxy (SeqSym0 a6989586621679703386 b6989586621679703387) t -> () #

type Apply a6989586621679703386 (TyFun b6989586621679703387 b6989586621679703387 -> Type) (SeqSym0 a6989586621679703386 b6989586621679703387) l0 # 
type Apply a6989586621679703386 (TyFun b6989586621679703387 b6989586621679703387 -> Type) (SeqSym0 a6989586621679703386 b6989586621679703387) l0 = SeqSym1 b6989586621679703387 a6989586621679703386 l0

data SeqSym1 l l #

Instances

SuppressUnusedWarnings (a6989586621679703386 -> TyFun b6989586621679703387 b6989586621679703387 -> *) (SeqSym1 b6989586621679703387 a6989586621679703386) # 

Methods

suppressUnusedWarnings :: Proxy (SeqSym1 b6989586621679703387 a6989586621679703386) t -> () #

type Apply b6989586621679703387 b6989586621679703387 (SeqSym1 b6989586621679703387 a6989586621679703386 l0) l1 # 
type Apply b6989586621679703387 b6989586621679703387 (SeqSym1 b6989586621679703387 a6989586621679703386 l0) l1 = SeqSym2 b6989586621679703387 a6989586621679703386 l0 l1

type SeqSym2 t t = Seq t t #