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 a6989586621679244034 (TyFun b6989586621679244035 b6989586621679244035 -> Type) -> Type) (TyFun b6989586621679244035 (TyFun [a6989586621679244034] b6989586621679244035 -> Type) -> Type))
- data FoldrSym1 (l :: TyFun a6989586621679244034 (TyFun b6989586621679244035 b6989586621679244035 -> Type) -> Type) (l :: TyFun b6989586621679244035 (TyFun [a6989586621679244034] b6989586621679244035 -> Type))
- data FoldrSym2 (l :: TyFun a6989586621679244034 (TyFun b6989586621679244035 b6989586621679244035 -> Type) -> Type) (l :: b6989586621679244035) (l :: TyFun [a6989586621679244034] b6989586621679244035)
- type FoldrSym3 (t :: TyFun a6989586621679244034 (TyFun b6989586621679244035 b6989586621679244035 -> Type) -> Type) (t :: b6989586621679244035) (t :: [a6989586621679244034]) = Foldr t t t
- data MapSym0 (l :: TyFun (TyFun a6989586621679244032 b6989586621679244033 -> Type) (TyFun [a6989586621679244032] [b6989586621679244033] -> Type))
- data MapSym1 (l :: TyFun a6989586621679244032 b6989586621679244033 -> Type) (l :: TyFun [a6989586621679244032] [b6989586621679244033])
- type MapSym2 (t :: TyFun a6989586621679244032 b6989586621679244033 -> Type) (t :: [a6989586621679244032]) = Map t t
- data (:++$) (l :: TyFun [a6989586621679244031] (TyFun [a6989586621679244031] [a6989586621679244031] -> Type))
- data (l :: [a6989586621679244031]) :++$$ (l :: TyFun [a6989586621679244031] [a6989586621679244031])
- type (:++$$$) (t :: [a6989586621679244031]) (t :: [a6989586621679244031]) = (:++) t t
- type OtherwiseSym0 = Otherwise
- data IdSym0 (l :: TyFun a6989586621679244030 a6989586621679244030)
- type IdSym1 (t :: a6989586621679244030) = Id t
- data ConstSym0 (l :: TyFun a6989586621679244028 (TyFun b6989586621679244029 a6989586621679244028 -> Type))
- data ConstSym1 (l :: a6989586621679244028) (l :: TyFun b6989586621679244029 a6989586621679244028)
- type ConstSym2 (t :: a6989586621679244028) (t :: b6989586621679244029) = Const t t
- data (:.$) (l :: TyFun (TyFun b6989586621679244025 c6989586621679244026 -> Type) (TyFun (TyFun a6989586621679244027 b6989586621679244025 -> Type) (TyFun a6989586621679244027 c6989586621679244026 -> Type) -> Type))
- data (l :: TyFun b6989586621679244025 c6989586621679244026 -> Type) :.$$ (l :: TyFun (TyFun a6989586621679244027 b6989586621679244025 -> Type) (TyFun a6989586621679244027 c6989586621679244026 -> Type))
- data ((l :: TyFun b6989586621679244025 c6989586621679244026 -> Type) :.$$$ (l :: TyFun a6989586621679244027 b6989586621679244025 -> Type)) (l :: TyFun a6989586621679244027 c6989586621679244026)
- type (:.$$$$) (t :: TyFun b6989586621679244025 c6989586621679244026 -> Type) (t :: TyFun a6989586621679244027 b6989586621679244025 -> Type) (t :: a6989586621679244027) = (:.) 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 a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) (TyFun b6989586621679244023 (TyFun a6989586621679244022 c6989586621679244024 -> Type) -> Type))
- data FlipSym1 (l :: TyFun a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) (l :: TyFun b6989586621679244023 (TyFun a6989586621679244022 c6989586621679244024 -> Type))
- data FlipSym2 (l :: TyFun a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) (l :: b6989586621679244023) (l :: TyFun a6989586621679244022 c6989586621679244024)
- type FlipSym3 (t :: TyFun a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) (t :: b6989586621679244023) (t :: a6989586621679244022) = Flip t t t
- data AsTypeOfSym0 (l :: TyFun a6989586621679244021 (TyFun a6989586621679244021 a6989586621679244021 -> Type))
- data AsTypeOfSym1 (l :: a6989586621679244021) (l :: TyFun a6989586621679244021 a6989586621679244021)
- type AsTypeOfSym2 (t :: a6989586621679244021) (t :: a6989586621679244021) = AsTypeOf t t
- data SeqSym0 (l :: TyFun a6989586621679244019 (TyFun b6989586621679244020 b6989586621679244020 -> Type))
- data SeqSym1 (l :: a6989586621679244019) (l :: TyFun b6989586621679244020 b6989586621679244020)
- type SeqSym2 (t :: a6989586621679244019) (t :: b6989586621679244020) = 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_6989586621679244075 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 a6989586621679244034 (TyFun b6989586621679244035 b6989586621679244035 -> Type) -> Type) (TyFun b6989586621679244035 (TyFun [a6989586621679244034] b6989586621679244035 -> Type) -> Type)) #
Instances
SuppressUnusedWarnings (TyFun (TyFun a6989586621679244034 (TyFun b6989586621679244035 b6989586621679244035 -> Type) -> Type) (TyFun b6989586621679244035 (TyFun [a6989586621679244034] b6989586621679244035 -> Type) -> Type) -> *) (FoldrSym0 a6989586621679244034 b6989586621679244035) # | |
type Apply (TyFun a6989586621679244034 (TyFun b6989586621679244035 b6989586621679244035 -> Type) -> Type) (TyFun b6989586621679244035 (TyFun [a6989586621679244034] b6989586621679244035 -> Type) -> Type) (FoldrSym0 a6989586621679244034 b6989586621679244035) l # | |
data FoldrSym1 (l :: TyFun a6989586621679244034 (TyFun b6989586621679244035 b6989586621679244035 -> Type) -> Type) (l :: TyFun b6989586621679244035 (TyFun [a6989586621679244034] b6989586621679244035 -> Type)) #
Instances
SuppressUnusedWarnings ((TyFun a6989586621679244034 (TyFun b6989586621679244035 b6989586621679244035 -> Type) -> Type) -> TyFun b6989586621679244035 (TyFun [a6989586621679244034] b6989586621679244035 -> Type) -> *) (FoldrSym1 a6989586621679244034 b6989586621679244035) # | |
type Apply b6989586621679244035 (TyFun [a6989586621679244034] b6989586621679244035 -> Type) (FoldrSym1 a6989586621679244034 b6989586621679244035 l1) l2 # | |
data FoldrSym2 (l :: TyFun a6989586621679244034 (TyFun b6989586621679244035 b6989586621679244035 -> Type) -> Type) (l :: b6989586621679244035) (l :: TyFun [a6989586621679244034] b6989586621679244035) #
Instances
SuppressUnusedWarnings ((TyFun a6989586621679244034 (TyFun b6989586621679244035 b6989586621679244035 -> Type) -> Type) -> b6989586621679244035 -> TyFun [a6989586621679244034] b6989586621679244035 -> *) (FoldrSym2 a6989586621679244034 b6989586621679244035) # | |
type Apply [a] b (FoldrSym2 a b l1 l2) l3 # | |
type FoldrSym3 (t :: TyFun a6989586621679244034 (TyFun b6989586621679244035 b6989586621679244035 -> Type) -> Type) (t :: b6989586621679244035) (t :: [a6989586621679244034]) = Foldr t t t #
data MapSym0 (l :: TyFun (TyFun a6989586621679244032 b6989586621679244033 -> Type) (TyFun [a6989586621679244032] [b6989586621679244033] -> Type)) #
Instances
SuppressUnusedWarnings (TyFun (TyFun a6989586621679244032 b6989586621679244033 -> Type) (TyFun [a6989586621679244032] [b6989586621679244033] -> Type) -> *) (MapSym0 a6989586621679244032 b6989586621679244033) # | |
type Apply (TyFun a6989586621679244032 b6989586621679244033 -> Type) (TyFun [a6989586621679244032] [b6989586621679244033] -> Type) (MapSym0 a6989586621679244032 b6989586621679244033) l # | |
data MapSym1 (l :: TyFun a6989586621679244032 b6989586621679244033 -> Type) (l :: TyFun [a6989586621679244032] [b6989586621679244033]) #
type MapSym2 (t :: TyFun a6989586621679244032 b6989586621679244033 -> Type) (t :: [a6989586621679244032]) = Map t t #
data (:++$) (l :: TyFun [a6989586621679244031] (TyFun [a6989586621679244031] [a6989586621679244031] -> Type)) #
data (l :: [a6989586621679244031]) :++$$ (l :: TyFun [a6989586621679244031] [a6989586621679244031]) #
type OtherwiseSym0 = Otherwise #
data ConstSym0 (l :: TyFun a6989586621679244028 (TyFun b6989586621679244029 a6989586621679244028 -> Type)) #
Instances
SuppressUnusedWarnings (TyFun a6989586621679244028 (TyFun b6989586621679244029 a6989586621679244028 -> Type) -> *) (ConstSym0 b6989586621679244029 a6989586621679244028) # | |
type Apply a6989586621679244028 (TyFun b6989586621679244029 a6989586621679244028 -> Type) (ConstSym0 b6989586621679244029 a6989586621679244028) l # | |
data (:.$) (l :: TyFun (TyFun b6989586621679244025 c6989586621679244026 -> Type) (TyFun (TyFun a6989586621679244027 b6989586621679244025 -> Type) (TyFun a6989586621679244027 c6989586621679244026 -> Type) -> Type)) #
Instances
SuppressUnusedWarnings (TyFun (TyFun b6989586621679244025 c6989586621679244026 -> Type) (TyFun (TyFun a6989586621679244027 b6989586621679244025 -> Type) (TyFun a6989586621679244027 c6989586621679244026 -> Type) -> Type) -> *) ((:.$) b6989586621679244025 a6989586621679244027 c6989586621679244026) # | |
type Apply (TyFun b6989586621679244025 c6989586621679244026 -> Type) (TyFun (TyFun a6989586621679244027 b6989586621679244025 -> Type) (TyFun a6989586621679244027 c6989586621679244026 -> Type) -> Type) ((:.$) b6989586621679244025 a6989586621679244027 c6989586621679244026) l # | |
data (l :: TyFun b6989586621679244025 c6989586621679244026 -> Type) :.$$ (l :: TyFun (TyFun a6989586621679244027 b6989586621679244025 -> Type) (TyFun a6989586621679244027 c6989586621679244026 -> Type)) #
Instances
SuppressUnusedWarnings ((TyFun b6989586621679244025 c6989586621679244026 -> Type) -> TyFun (TyFun a6989586621679244027 b6989586621679244025 -> Type) (TyFun a6989586621679244027 c6989586621679244026 -> Type) -> *) ((:.$$) b6989586621679244025 a6989586621679244027 c6989586621679244026) # | |
type Apply (TyFun a6989586621679244027 b6989586621679244025 -> Type) (TyFun a6989586621679244027 c6989586621679244026 -> Type) ((:.$$) b6989586621679244025 a6989586621679244027 c6989586621679244026 l1) l2 # | |
data ((l :: TyFun b6989586621679244025 c6989586621679244026 -> Type) :.$$$ (l :: TyFun a6989586621679244027 b6989586621679244025 -> Type)) (l :: TyFun a6989586621679244027 c6989586621679244026) #
Instances
SuppressUnusedWarnings ((TyFun b6989586621679244025 c6989586621679244026 -> Type) -> (TyFun a6989586621679244027 b6989586621679244025 -> Type) -> TyFun a6989586621679244027 c6989586621679244026 -> *) ((:.$$$) b6989586621679244025 a6989586621679244027 c6989586621679244026) # | |
type Apply a c ((:.$$$) b a c l1 l2) l3 # | |
type (:.$$$$) (t :: TyFun b6989586621679244025 c6989586621679244026 -> Type) (t :: TyFun a6989586621679244027 b6989586621679244025 -> Type) (t :: a6989586621679244027) = (:.) t t t #
data FlipSym0 (l :: TyFun (TyFun a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) (TyFun b6989586621679244023 (TyFun a6989586621679244022 c6989586621679244024 -> Type) -> Type)) #
Instances
SuppressUnusedWarnings (TyFun (TyFun a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) (TyFun b6989586621679244023 (TyFun a6989586621679244022 c6989586621679244024 -> Type) -> Type) -> *) (FlipSym0 b6989586621679244023 a6989586621679244022 c6989586621679244024) # | |
type Apply (TyFun a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) (TyFun b6989586621679244023 (TyFun a6989586621679244022 c6989586621679244024 -> Type) -> Type) (FlipSym0 b6989586621679244023 a6989586621679244022 c6989586621679244024) l # | |
data FlipSym1 (l :: TyFun a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) (l :: TyFun b6989586621679244023 (TyFun a6989586621679244022 c6989586621679244024 -> Type)) #
Instances
SuppressUnusedWarnings ((TyFun a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) -> TyFun b6989586621679244023 (TyFun a6989586621679244022 c6989586621679244024 -> Type) -> *) (FlipSym1 b6989586621679244023 a6989586621679244022 c6989586621679244024) # | |
type Apply b6989586621679244023 (TyFun a6989586621679244022 c6989586621679244024 -> Type) (FlipSym1 b6989586621679244023 a6989586621679244022 c6989586621679244024 l1) l2 # | |
data FlipSym2 (l :: TyFun a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) (l :: b6989586621679244023) (l :: TyFun a6989586621679244022 c6989586621679244024) #
Instances
SuppressUnusedWarnings ((TyFun a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) -> b6989586621679244023 -> TyFun a6989586621679244022 c6989586621679244024 -> *) (FlipSym2 b6989586621679244023 a6989586621679244022 c6989586621679244024) # | |
type Apply a c (FlipSym2 b a c l1 l2) l3 # | |
type FlipSym3 (t :: TyFun a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) (t :: b6989586621679244023) (t :: a6989586621679244022) = Flip t t t #
data AsTypeOfSym0 (l :: TyFun a6989586621679244021 (TyFun a6989586621679244021 a6989586621679244021 -> Type)) #
Instances
SuppressUnusedWarnings (TyFun a6989586621679244021 (TyFun a6989586621679244021 a6989586621679244021 -> Type) -> *) (AsTypeOfSym0 a6989586621679244021) # | |
type Apply a6989586621679244021 (TyFun a6989586621679244021 a6989586621679244021 -> Type) (AsTypeOfSym0 a6989586621679244021) l # | |
data AsTypeOfSym1 (l :: a6989586621679244021) (l :: TyFun a6989586621679244021 a6989586621679244021) #
Instances
SuppressUnusedWarnings (a6989586621679244021 -> TyFun a6989586621679244021 a6989586621679244021 -> *) (AsTypeOfSym1 a6989586621679244021) # | |
type Apply a a (AsTypeOfSym1 a l1) l2 # | |
type AsTypeOfSym2 (t :: a6989586621679244021) (t :: a6989586621679244021) = AsTypeOf t t #
data SeqSym0 (l :: TyFun a6989586621679244019 (TyFun b6989586621679244020 b6989586621679244020 -> Type)) #
Instances
SuppressUnusedWarnings (TyFun a6989586621679244019 (TyFun b6989586621679244020 b6989586621679244020 -> Type) -> *) (SeqSym0 a6989586621679244019 b6989586621679244020) # | |
type Apply a6989586621679244019 (TyFun b6989586621679244020 b6989586621679244020 -> Type) (SeqSym0 a6989586621679244019 b6989586621679244020) l # | |