| 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
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.
- type family Foldr (a :: TyFun a (TyFun b b -> Type) -> Type) (a :: b) (a :: [a]) :: b where ...
- 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 ...
- 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 ...
- (%:++) :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (:++$) t) t :: [a])
- type family Otherwise :: Bool where ...
- sOtherwise :: Sing (OtherwiseSym0 :: Bool)
- type family Id (a :: a) :: a where ...
- sId :: forall (t :: a). Sing t -> Sing (Apply IdSym0 t :: a)
- type family Const (a :: a) (a :: b) :: a where ...
- 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 ...
- (%:.) :: 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)
- type family (f :: TyFun a b -> *) $ (x :: a) :: b
- type family (f :: TyFun a b -> *) $! (x :: a) :: b
- (%$) :: forall (f :: TyFun a b -> *) (x :: a). Sing f -> Sing x -> Sing ((($$) @@ f) @@ x)
- (%$!) :: forall (f :: TyFun a b -> *) (x :: a). Sing f -> Sing x -> Sing ((($!$) @@ f) @@ x)
- type family Flip (a :: TyFun a (TyFun b c -> Type) -> Type) (a :: b) (a :: a) :: c where ...
- 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 ...
- 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 ...
- sSeq :: forall (t :: a) (t :: b). Sing t -> Sing t -> Sing (Apply (Apply SeqSym0 t) t :: b)
- data FoldrSym0 (l :: TyFun (TyFun a6989586621679292517 (TyFun b6989586621679292518 b6989586621679292518 -> Type) -> Type) (TyFun b6989586621679292518 (TyFun [a6989586621679292517] b6989586621679292518 -> Type) -> Type))
- data FoldrSym1 (l :: TyFun a6989586621679292517 (TyFun b6989586621679292518 b6989586621679292518 -> Type) -> Type) (l :: TyFun b6989586621679292518 (TyFun [a6989586621679292517] b6989586621679292518 -> Type))
- data FoldrSym2 (l :: TyFun a6989586621679292517 (TyFun b6989586621679292518 b6989586621679292518 -> Type) -> Type) (l :: b6989586621679292518) (l :: TyFun [a6989586621679292517] b6989586621679292518)
- type FoldrSym3 (t :: TyFun a6989586621679292517 (TyFun b6989586621679292518 b6989586621679292518 -> Type) -> Type) (t :: b6989586621679292518) (t :: [a6989586621679292517]) = Foldr t t t
- data MapSym0 (l :: TyFun (TyFun a6989586621679292515 b6989586621679292516 -> Type) (TyFun [a6989586621679292515] [b6989586621679292516] -> Type))
- data MapSym1 (l :: TyFun a6989586621679292515 b6989586621679292516 -> Type) (l :: TyFun [a6989586621679292515] [b6989586621679292516])
- type MapSym2 (t :: TyFun a6989586621679292515 b6989586621679292516 -> Type) (t :: [a6989586621679292515]) = Map t t
- data (:++$) (l :: TyFun [a6989586621679292514] (TyFun [a6989586621679292514] [a6989586621679292514] -> Type))
- data (l :: [a6989586621679292514]) :++$$ (l :: TyFun [a6989586621679292514] [a6989586621679292514])
- type (:++$$$) (t :: [a6989586621679292514]) (t :: [a6989586621679292514]) = (:++) t t
- type OtherwiseSym0 = Otherwise
- data IdSym0 (l :: TyFun a6989586621679292513 a6989586621679292513)
- type IdSym1 (t :: a6989586621679292513) = Id t
- data ConstSym0 (l :: TyFun a6989586621679292511 (TyFun b6989586621679292512 a6989586621679292511 -> Type))
- data ConstSym1 (l :: a6989586621679292511) (l :: TyFun b6989586621679292512 a6989586621679292511)
- type ConstSym2 (t :: a6989586621679292511) (t :: b6989586621679292512) = Const t t
- data (:.$) (l :: TyFun (TyFun b6989586621679292508 c6989586621679292509 -> Type) (TyFun (TyFun a6989586621679292510 b6989586621679292508 -> Type) (TyFun a6989586621679292510 c6989586621679292509 -> Type) -> Type))
- data (l :: TyFun b6989586621679292508 c6989586621679292509 -> Type) :.$$ (l :: TyFun (TyFun a6989586621679292510 b6989586621679292508 -> Type) (TyFun a6989586621679292510 c6989586621679292509 -> Type))
- data ((l :: TyFun b6989586621679292508 c6989586621679292509 -> Type) :.$$$ (l :: TyFun a6989586621679292510 b6989586621679292508 -> Type)) (l :: TyFun a6989586621679292510 c6989586621679292509)
- type (:.$$$$) (t :: TyFun b6989586621679292508 c6989586621679292509 -> Type) (t :: TyFun a6989586621679292510 b6989586621679292508 -> Type) (t :: a6989586621679292510) = (:.) t t t
- data ($$) :: TyFun (TyFun a b -> *) (TyFun a b -> *) -> *
- data ($$$) :: (TyFun a b -> *) -> TyFun a b -> *
- type ($$$$) a b = ($) a b
- data ($!$) :: TyFun (TyFun a b -> *) (TyFun a b -> *) -> *
- data ($!$$) :: (TyFun a b -> *) -> TyFun a b -> *
- type ($!$$$) a b = ($!) a b
- data FlipSym0 (l :: TyFun (TyFun a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) (TyFun b6989586621679292506 (TyFun a6989586621679292505 c6989586621679292507 -> Type) -> Type))
- data FlipSym1 (l :: TyFun a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) (l :: TyFun b6989586621679292506 (TyFun a6989586621679292505 c6989586621679292507 -> Type))
- data FlipSym2 (l :: TyFun a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) (l :: b6989586621679292506) (l :: TyFun a6989586621679292505 c6989586621679292507)
- type FlipSym3 (t :: TyFun a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) (t :: b6989586621679292506) (t :: a6989586621679292505) = Flip t t t
- data AsTypeOfSym0 (l :: TyFun a6989586621679292504 (TyFun a6989586621679292504 a6989586621679292504 -> Type))
- data AsTypeOfSym1 (l :: a6989586621679292504) (l :: TyFun a6989586621679292504 a6989586621679292504)
- type AsTypeOfSym2 (t :: a6989586621679292504) (t :: a6989586621679292504) = AsTypeOf t t
- data SeqSym0 (l :: TyFun a6989586621679292502 (TyFun b6989586621679292503 b6989586621679292503 -> Type))
- data SeqSym1 (l :: a6989586621679292502) (l :: TyFun b6989586621679292503 b6989586621679292503)
- type SeqSym2 (t :: a6989586621679292502) (t :: b6989586621679292503) = Seq t t
Basic functions
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) #
sMap :: forall (t :: TyFun a b -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply MapSym0 t) t :: [b]) #
(%:++) :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (:++$) t) t :: [a]) infixr 5 #
sOtherwise :: Sing (OtherwiseSym0 :: Bool) #
type family ((a :: TyFun b c -> Type) :. (a :: TyFun a b -> Type)) (a :: a) :: c where ... infixr 9 #
(%:.) :: 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 #
(%$) :: 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 #
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) #
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_6989586621679292558 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 a6989586621679292517 (TyFun b6989586621679292518 b6989586621679292518 -> Type) -> Type) (TyFun b6989586621679292518 (TyFun [a6989586621679292517] b6989586621679292518 -> Type) -> Type)) #
Instances
| SuppressUnusedWarnings (TyFun (TyFun a6989586621679292517 (TyFun b6989586621679292518 b6989586621679292518 -> Type) -> Type) (TyFun b6989586621679292518 (TyFun [a6989586621679292517] b6989586621679292518 -> Type) -> Type) -> *) (FoldrSym0 a6989586621679292517 b6989586621679292518) # | |
| type Apply (TyFun a6989586621679292517 (TyFun b6989586621679292518 b6989586621679292518 -> Type) -> Type) (TyFun b6989586621679292518 (TyFun [a6989586621679292517] b6989586621679292518 -> Type) -> Type) (FoldrSym0 a6989586621679292517 b6989586621679292518) l # | |
data FoldrSym1 (l :: TyFun a6989586621679292517 (TyFun b6989586621679292518 b6989586621679292518 -> Type) -> Type) (l :: TyFun b6989586621679292518 (TyFun [a6989586621679292517] b6989586621679292518 -> Type)) #
Instances
| SuppressUnusedWarnings ((TyFun a6989586621679292517 (TyFun b6989586621679292518 b6989586621679292518 -> Type) -> Type) -> TyFun b6989586621679292518 (TyFun [a6989586621679292517] b6989586621679292518 -> Type) -> *) (FoldrSym1 a6989586621679292517 b6989586621679292518) # | |
| type Apply b6989586621679292518 (TyFun [a6989586621679292517] b6989586621679292518 -> Type) (FoldrSym1 a6989586621679292517 b6989586621679292518 l1) l2 # | |
data FoldrSym2 (l :: TyFun a6989586621679292517 (TyFun b6989586621679292518 b6989586621679292518 -> Type) -> Type) (l :: b6989586621679292518) (l :: TyFun [a6989586621679292517] b6989586621679292518) #
Instances
| SuppressUnusedWarnings ((TyFun a6989586621679292517 (TyFun b6989586621679292518 b6989586621679292518 -> Type) -> Type) -> b6989586621679292518 -> TyFun [a6989586621679292517] b6989586621679292518 -> *) (FoldrSym2 a6989586621679292517 b6989586621679292518) # | |
| type Apply [a] b (FoldrSym2 a b l1 l2) l3 # | |
type FoldrSym3 (t :: TyFun a6989586621679292517 (TyFun b6989586621679292518 b6989586621679292518 -> Type) -> Type) (t :: b6989586621679292518) (t :: [a6989586621679292517]) = Foldr t t t #
data MapSym0 (l :: TyFun (TyFun a6989586621679292515 b6989586621679292516 -> Type) (TyFun [a6989586621679292515] [b6989586621679292516] -> Type)) #
Instances
| SuppressUnusedWarnings (TyFun (TyFun a6989586621679292515 b6989586621679292516 -> Type) (TyFun [a6989586621679292515] [b6989586621679292516] -> Type) -> *) (MapSym0 a6989586621679292515 b6989586621679292516) # | |
| type Apply (TyFun a6989586621679292515 b6989586621679292516 -> Type) (TyFun [a6989586621679292515] [b6989586621679292516] -> Type) (MapSym0 a6989586621679292515 b6989586621679292516) l # | |
data MapSym1 (l :: TyFun a6989586621679292515 b6989586621679292516 -> Type) (l :: TyFun [a6989586621679292515] [b6989586621679292516]) #
type MapSym2 (t :: TyFun a6989586621679292515 b6989586621679292516 -> Type) (t :: [a6989586621679292515]) = Map t t #
data (:++$) (l :: TyFun [a6989586621679292514] (TyFun [a6989586621679292514] [a6989586621679292514] -> Type)) #
data (l :: [a6989586621679292514]) :++$$ (l :: TyFun [a6989586621679292514] [a6989586621679292514]) #
type OtherwiseSym0 = Otherwise #
data ConstSym0 (l :: TyFun a6989586621679292511 (TyFun b6989586621679292512 a6989586621679292511 -> Type)) #
Instances
| SuppressUnusedWarnings (TyFun a6989586621679292511 (TyFun b6989586621679292512 a6989586621679292511 -> Type) -> *) (ConstSym0 b6989586621679292512 a6989586621679292511) # | |
| type Apply a6989586621679292511 (TyFun b6989586621679292512 a6989586621679292511 -> Type) (ConstSym0 b6989586621679292512 a6989586621679292511) l # | |
data (:.$) (l :: TyFun (TyFun b6989586621679292508 c6989586621679292509 -> Type) (TyFun (TyFun a6989586621679292510 b6989586621679292508 -> Type) (TyFun a6989586621679292510 c6989586621679292509 -> Type) -> Type)) #
Instances
| SuppressUnusedWarnings (TyFun (TyFun b6989586621679292508 c6989586621679292509 -> Type) (TyFun (TyFun a6989586621679292510 b6989586621679292508 -> Type) (TyFun a6989586621679292510 c6989586621679292509 -> Type) -> Type) -> *) ((:.$) b6989586621679292508 a6989586621679292510 c6989586621679292509) # | |
| type Apply (TyFun b6989586621679292508 c6989586621679292509 -> Type) (TyFun (TyFun a6989586621679292510 b6989586621679292508 -> Type) (TyFun a6989586621679292510 c6989586621679292509 -> Type) -> Type) ((:.$) b6989586621679292508 a6989586621679292510 c6989586621679292509) l # | |
data (l :: TyFun b6989586621679292508 c6989586621679292509 -> Type) :.$$ (l :: TyFun (TyFun a6989586621679292510 b6989586621679292508 -> Type) (TyFun a6989586621679292510 c6989586621679292509 -> Type)) #
Instances
| SuppressUnusedWarnings ((TyFun b6989586621679292508 c6989586621679292509 -> Type) -> TyFun (TyFun a6989586621679292510 b6989586621679292508 -> Type) (TyFun a6989586621679292510 c6989586621679292509 -> Type) -> *) ((:.$$) b6989586621679292508 a6989586621679292510 c6989586621679292509) # | |
| type Apply (TyFun a6989586621679292510 b6989586621679292508 -> Type) (TyFun a6989586621679292510 c6989586621679292509 -> Type) ((:.$$) b6989586621679292508 a6989586621679292510 c6989586621679292509 l1) l2 # | |
data ((l :: TyFun b6989586621679292508 c6989586621679292509 -> Type) :.$$$ (l :: TyFun a6989586621679292510 b6989586621679292508 -> Type)) (l :: TyFun a6989586621679292510 c6989586621679292509) #
Instances
| SuppressUnusedWarnings ((TyFun b6989586621679292508 c6989586621679292509 -> Type) -> (TyFun a6989586621679292510 b6989586621679292508 -> Type) -> TyFun a6989586621679292510 c6989586621679292509 -> *) ((:.$$$) b6989586621679292508 a6989586621679292510 c6989586621679292509) # | |
| type Apply a c ((:.$$$) b a c l1 l2) l3 # | |
type (:.$$$$) (t :: TyFun b6989586621679292508 c6989586621679292509 -> Type) (t :: TyFun a6989586621679292510 b6989586621679292508 -> Type) (t :: a6989586621679292510) = (:.) t t t #
data FlipSym0 (l :: TyFun (TyFun a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) (TyFun b6989586621679292506 (TyFun a6989586621679292505 c6989586621679292507 -> Type) -> Type)) #
Instances
| SuppressUnusedWarnings (TyFun (TyFun a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) (TyFun b6989586621679292506 (TyFun a6989586621679292505 c6989586621679292507 -> Type) -> Type) -> *) (FlipSym0 b6989586621679292506 a6989586621679292505 c6989586621679292507) # | |
| type Apply (TyFun a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) (TyFun b6989586621679292506 (TyFun a6989586621679292505 c6989586621679292507 -> Type) -> Type) (FlipSym0 b6989586621679292506 a6989586621679292505 c6989586621679292507) l # | |
data FlipSym1 (l :: TyFun a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) (l :: TyFun b6989586621679292506 (TyFun a6989586621679292505 c6989586621679292507 -> Type)) #
Instances
| SuppressUnusedWarnings ((TyFun a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) -> TyFun b6989586621679292506 (TyFun a6989586621679292505 c6989586621679292507 -> Type) -> *) (FlipSym1 b6989586621679292506 a6989586621679292505 c6989586621679292507) # | |
| type Apply b6989586621679292506 (TyFun a6989586621679292505 c6989586621679292507 -> Type) (FlipSym1 b6989586621679292506 a6989586621679292505 c6989586621679292507 l1) l2 # | |
data FlipSym2 (l :: TyFun a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) (l :: b6989586621679292506) (l :: TyFun a6989586621679292505 c6989586621679292507) #
Instances
| SuppressUnusedWarnings ((TyFun a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) -> b6989586621679292506 -> TyFun a6989586621679292505 c6989586621679292507 -> *) (FlipSym2 b6989586621679292506 a6989586621679292505 c6989586621679292507) # | |
| type Apply a c (FlipSym2 b a c l1 l2) l3 # | |
type FlipSym3 (t :: TyFun a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) (t :: b6989586621679292506) (t :: a6989586621679292505) = Flip t t t #
data AsTypeOfSym0 (l :: TyFun a6989586621679292504 (TyFun a6989586621679292504 a6989586621679292504 -> Type)) #
Instances
| SuppressUnusedWarnings (TyFun a6989586621679292504 (TyFun a6989586621679292504 a6989586621679292504 -> Type) -> *) (AsTypeOfSym0 a6989586621679292504) # | |
| type Apply a6989586621679292504 (TyFun a6989586621679292504 a6989586621679292504 -> Type) (AsTypeOfSym0 a6989586621679292504) l # | |
data AsTypeOfSym1 (l :: a6989586621679292504) (l :: TyFun a6989586621679292504 a6989586621679292504) #
Instances
| SuppressUnusedWarnings (a6989586621679292504 -> TyFun a6989586621679292504 a6989586621679292504 -> *) (AsTypeOfSym1 a6989586621679292504) # | |
| type Apply a a (AsTypeOfSym1 a l1) l2 # | |
type AsTypeOfSym2 (t :: a6989586621679292504) (t :: a6989586621679292504) = AsTypeOf t t #
data SeqSym0 (l :: TyFun a6989586621679292502 (TyFun b6989586621679292503 b6989586621679292503 -> Type)) #
Instances
| SuppressUnusedWarnings (TyFun a6989586621679292502 (TyFun b6989586621679292503 b6989586621679292503 -> Type) -> *) (SeqSym0 a6989586621679292502 b6989586621679292503) # | |
| type Apply a6989586621679292502 (TyFun b6989586621679292503 b6989586621679292503 -> Type) (SeqSym0 a6989586621679292502 b6989586621679292503) l # | |