Copyright | (C) 2013-2014 Richard Eisenberg Jan Stolarek |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Ryan Scott |
Stability | experimental |
Portability | non-portable |
Safe Haskell | Safe-Inferred |
Language | GHC2021 |
Defines functions and datatypes relating to the singleton for Either
,
including singled versions of all the definitions in Data.Either
.
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.Either
. Also, please excuse
the apparent repeated variable names. This is due to an interaction
between Template Haskell and Haddock.
Synopsis
- type family Sing :: k -> Type
- data SEither :: forall (a :: Type) (b :: Type). Either a b -> Type where
- either_ :: (a -> c) -> (b -> c) -> Either a b -> c
- type family Either_ (a :: (~>) a c) (a :: (~>) b c) (a :: Either a b) :: c where ...
- sEither_ :: forall (t :: (~>) a c) (t :: (~>) b c) (t :: Either a b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Either_Sym0 t) t) t :: c) :: Type
- type family Lefts (a :: [Either a b]) :: [a] where ...
- sLefts :: forall (t :: [Either a b]). Sing t -> Sing (Apply LeftsSym0 t :: [a]) :: Type
- type family Rights (a :: [Either a b]) :: [b] where ...
- sRights :: forall (t :: [Either a b]). Sing t -> Sing (Apply RightsSym0 t :: [b]) :: Type
- type family PartitionEithers (a :: [Either a b]) :: ([a], [b]) where ...
- sPartitionEithers :: forall (t :: [Either a b]). Sing t -> Sing (Apply PartitionEithersSym0 t :: ([a], [b])) :: Type
- type family IsLeft (a :: Either a b) :: Bool where ...
- sIsLeft :: forall (t :: Either a b). Sing t -> Sing (Apply IsLeftSym0 t :: Bool) :: Type
- type family IsRight (a :: Either a b) :: Bool where ...
- sIsRight :: forall (t :: Either a b). Sing t -> Sing (Apply IsRightSym0 t :: Bool) :: Type
- data LeftSym0 :: (~>) a (Either (a :: Type) (b :: Type))
- type family LeftSym1 (a6989586621679037600 :: a) :: Either (a :: Type) (b :: Type) where ...
- data RightSym0 :: (~>) b (Either (a :: Type) (b :: Type))
- type family RightSym1 (a6989586621679037602 :: b) :: Either (a :: Type) (b :: Type) where ...
- data Either_Sym0 :: (~>) ((~>) a c) ((~>) ((~>) b c) ((~>) (Either a b) c))
- data Either_Sym1 (a6989586621679264752 :: (~>) a c) :: (~>) ((~>) b c) ((~>) (Either a b) c)
- data Either_Sym2 (a6989586621679264752 :: (~>) a c) (a6989586621679264753 :: (~>) b c) :: (~>) (Either a b) c
- type family Either_Sym3 (a6989586621679264752 :: (~>) a c) (a6989586621679264753 :: (~>) b c) (a6989586621679264754 :: Either a b) :: c where ...
- data LeftsSym0 :: (~>) [Either a b] [a]
- type family LeftsSym1 (a6989586621679267017 :: [Either a b]) :: [a] where ...
- data RightsSym0 :: (~>) [Either a b] [b]
- type family RightsSym1 (a6989586621679267011 :: [Either a b]) :: [b] where ...
- data IsLeftSym0 :: (~>) (Either a b) Bool
- type family IsLeftSym1 (a6989586621679266989 :: Either a b) :: Bool where ...
- data IsRightSym0 :: (~>) (Either a b) Bool
- type family IsRightSym1 (a6989586621679266986 :: Either a b) :: Bool where ...
The Either
singleton
type family Sing :: k -> Type #
The singleton kind-indexed type family.
Instances
data SEither :: forall (a :: Type) (b :: Type). Either a b -> Type where Source #
SLeft :: forall (a :: Type) (b :: Type) (n :: a). (Sing n) -> SEither ('Left n :: Either (a :: Type) (b :: Type)) | |
SRight :: forall (a :: Type) (b :: Type) (n :: b). (Sing n) -> SEither ('Right n :: Either (a :: Type) (b :: Type)) |
Instances
(SDecide a, SDecide b) => TestCoercion (SEither :: Either a b -> Type) Source # | |
Defined in Data.Singletons.Base.Instances testCoercion :: forall (a0 :: k) (b0 :: k). SEither a0 -> SEither b0 -> Maybe (Coercion a0 b0) | |
(SDecide a, SDecide b) => TestEquality (SEither :: Either a b -> Type) Source # | |
Defined in Data.Singletons.Base.Instances testEquality :: forall (a0 :: k) (b0 :: k). SEither a0 -> SEither b0 -> Maybe (a0 :~: b0) | |
(ShowSing a, ShowSing b) => Show (SEither z) Source # | |
Singletons from Data.Either
sEither_ :: forall (t :: (~>) a c) (t :: (~>) b c) (t :: Either a b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Either_Sym0 t) t) t :: c) :: Type Source #
The preceding two definitions are derived from the function either
in
Data.Either
. The extra underscore is to avoid name clashes with the type
Either
.
type family PartitionEithers (a :: [Either a b]) :: ([a], [b]) where ... Source #
PartitionEithers a_6989586621679266990 = Apply (Apply (Apply FoldrSym0 (Apply (Apply Either_Sym0 (Let6989586621679266996LeftSym1 a_6989586621679266990)) (Let6989586621679266996RightSym1 a_6989586621679266990))) (Apply (Apply Tuple2Sym0 NilSym0) NilSym0)) a_6989586621679266990 |
sPartitionEithers :: forall (t :: [Either a b]). Sing t -> Sing (Apply PartitionEithersSym0 t :: ([a], [b])) :: Type Source #
Defunctionalization symbols
data LeftSym0 :: (~>) a (Either (a :: Type) (b :: Type)) Source #
Instances
SingI (LeftSym0 :: TyFun a (Either a b) -> Type) Source # | |
Defined in Data.Singletons.Base.Instances | |
SuppressUnusedWarnings (LeftSym0 :: TyFun a (Either a b) -> Type) Source # | |
Defined in Data.Singletons.Base.Instances suppressUnusedWarnings :: () # | |
type Apply (LeftSym0 :: TyFun a (Either a b) -> Type) (a6989586621679037600 :: a) Source # | |
Defined in Data.Singletons.Base.Instances |
type family LeftSym1 (a6989586621679037600 :: a) :: Either (a :: Type) (b :: Type) where ... Source #
LeftSym1 a6989586621679037600 = 'Left a6989586621679037600 |
data RightSym0 :: (~>) b (Either (a :: Type) (b :: Type)) Source #
Instances
SingI (RightSym0 :: TyFun b (Either a b) -> Type) Source # | |
Defined in Data.Singletons.Base.Instances | |
SuppressUnusedWarnings (RightSym0 :: TyFun b (Either a b) -> Type) Source # | |
Defined in Data.Singletons.Base.Instances suppressUnusedWarnings :: () # | |
type Apply (RightSym0 :: TyFun b (Either a b) -> Type) (a6989586621679037602 :: b) Source # | |
Defined in Data.Singletons.Base.Instances |
type family RightSym1 (a6989586621679037602 :: b) :: Either (a :: Type) (b :: Type) where ... Source #
RightSym1 a6989586621679037602 = 'Right a6989586621679037602 |
data Either_Sym0 :: (~>) ((~>) a c) ((~>) ((~>) b c) ((~>) (Either a b) c)) Source #
Instances
SingI (Either_Sym0 :: TyFun (a ~> c) ((b ~> c) ~> (Either a b ~> c)) -> Type) Source # | |
Defined in Data.Either.Singletons sing :: Sing Either_Sym0 # | |
SuppressUnusedWarnings (Either_Sym0 :: TyFun (a ~> c) ((b ~> c) ~> (Either a b ~> c)) -> Type) Source # | |
Defined in Data.Either.Singletons suppressUnusedWarnings :: () # | |
type Apply (Either_Sym0 :: TyFun (a ~> c) ((b ~> c) ~> (Either a b ~> c)) -> Type) (a6989586621679264752 :: a ~> c) Source # | |
Defined in Data.Either.Singletons |
data Either_Sym1 (a6989586621679264752 :: (~>) a c) :: (~>) ((~>) b c) ((~>) (Either a b) c) Source #
Instances
SingI1 (Either_Sym1 :: (a ~> c) -> TyFun (b ~> c) (Either a b ~> c) -> Type) Source # | |
Defined in Data.Either.Singletons liftSing :: forall (x :: k1). Sing x -> Sing (Either_Sym1 x) # | |
SingI d => SingI (Either_Sym1 d :: TyFun (b ~> c) (Either a b ~> c) -> Type) Source # | |
Defined in Data.Either.Singletons sing :: Sing (Either_Sym1 d) # | |
SuppressUnusedWarnings (Either_Sym1 a6989586621679264752 :: TyFun (b ~> c) (Either a b ~> c) -> Type) Source # | |
Defined in Data.Either.Singletons suppressUnusedWarnings :: () # | |
type Apply (Either_Sym1 a6989586621679264752 :: TyFun (b ~> c) (Either a b ~> c) -> Type) (a6989586621679264753 :: b ~> c) Source # | |
Defined in Data.Either.Singletons type Apply (Either_Sym1 a6989586621679264752 :: TyFun (b ~> c) (Either a b ~> c) -> Type) (a6989586621679264753 :: b ~> c) = Either_Sym2 a6989586621679264752 a6989586621679264753 |
data Either_Sym2 (a6989586621679264752 :: (~>) a c) (a6989586621679264753 :: (~>) b c) :: (~>) (Either a b) c Source #
Instances
SingI2 (Either_Sym2 :: (a ~> c) -> (b ~> c) -> TyFun (Either a b) c -> Type) Source # | |
Defined in Data.Either.Singletons | |
SingI d => SingI1 (Either_Sym2 d :: (b ~> c) -> TyFun (Either a b) c -> Type) Source # | |
Defined in Data.Either.Singletons liftSing :: forall (x :: k1). Sing x -> Sing (Either_Sym2 d x) # | |
(SingI d1, SingI d2) => SingI (Either_Sym2 d1 d2 :: TyFun (Either a b) c -> Type) Source # | |
Defined in Data.Either.Singletons sing :: Sing (Either_Sym2 d1 d2) # | |
SuppressUnusedWarnings (Either_Sym2 a6989586621679264752 a6989586621679264753 :: TyFun (Either a b) c -> Type) Source # | |
Defined in Data.Either.Singletons suppressUnusedWarnings :: () # | |
type Apply (Either_Sym2 a6989586621679264752 a6989586621679264753 :: TyFun (Either a b) c -> Type) (a6989586621679264754 :: Either a b) Source # | |
Defined in Data.Either.Singletons type Apply (Either_Sym2 a6989586621679264752 a6989586621679264753 :: TyFun (Either a b) c -> Type) (a6989586621679264754 :: Either a b) = Either_ a6989586621679264752 a6989586621679264753 a6989586621679264754 |
type family Either_Sym3 (a6989586621679264752 :: (~>) a c) (a6989586621679264753 :: (~>) b c) (a6989586621679264754 :: Either a b) :: c where ... Source #
Either_Sym3 a6989586621679264752 a6989586621679264753 a6989586621679264754 = Either_ a6989586621679264752 a6989586621679264753 a6989586621679264754 |
data LeftsSym0 :: (~>) [Either a b] [a] Source #
Instances
SingI (LeftsSym0 :: TyFun [Either a b] [a] -> Type) Source # | |
Defined in Data.Either.Singletons | |
SuppressUnusedWarnings (LeftsSym0 :: TyFun [Either a b] [a] -> Type) Source # | |
Defined in Data.Either.Singletons suppressUnusedWarnings :: () # | |
type Apply (LeftsSym0 :: TyFun [Either a b] [a] -> Type) (a6989586621679267017 :: [Either a b]) Source # | |
Defined in Data.Either.Singletons |
data RightsSym0 :: (~>) [Either a b] [b] Source #
Instances
SingI (RightsSym0 :: TyFun [Either a b] [b] -> Type) Source # | |
Defined in Data.Either.Singletons sing :: Sing RightsSym0 # | |
SuppressUnusedWarnings (RightsSym0 :: TyFun [Either a b] [b] -> Type) Source # | |
Defined in Data.Either.Singletons suppressUnusedWarnings :: () # | |
type Apply (RightsSym0 :: TyFun [Either a b] [b] -> Type) (a6989586621679267011 :: [Either a b]) Source # | |
Defined in Data.Either.Singletons type Apply (RightsSym0 :: TyFun [Either a b] [b] -> Type) (a6989586621679267011 :: [Either a b]) = Rights a6989586621679267011 |
type family RightsSym1 (a6989586621679267011 :: [Either a b]) :: [b] where ... Source #
RightsSym1 a6989586621679267011 = Rights a6989586621679267011 |
data IsLeftSym0 :: (~>) (Either a b) Bool Source #
Instances
SingI (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) Source # | |
Defined in Data.Either.Singletons sing :: Sing IsLeftSym0 # | |
SuppressUnusedWarnings (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) Source # | |
Defined in Data.Either.Singletons suppressUnusedWarnings :: () # | |
type Apply (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) (a6989586621679266989 :: Either a b) Source # | |
Defined in Data.Either.Singletons type Apply (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) (a6989586621679266989 :: Either a b) = IsLeft a6989586621679266989 |
type family IsLeftSym1 (a6989586621679266989 :: Either a b) :: Bool where ... Source #
IsLeftSym1 a6989586621679266989 = IsLeft a6989586621679266989 |
data IsRightSym0 :: (~>) (Either a b) Bool Source #
Instances
SingI (IsRightSym0 :: TyFun (Either a b) Bool -> Type) Source # | |
Defined in Data.Either.Singletons sing :: Sing IsRightSym0 # | |
SuppressUnusedWarnings (IsRightSym0 :: TyFun (Either a b) Bool -> Type) Source # | |
Defined in Data.Either.Singletons suppressUnusedWarnings :: () # | |
type Apply (IsRightSym0 :: TyFun (Either a b) Bool -> Type) (a6989586621679266986 :: Either a b) Source # | |
Defined in Data.Either.Singletons type Apply (IsRightSym0 :: TyFun (Either a b) Bool -> Type) (a6989586621679266986 :: Either a b) = IsRight a6989586621679266986 |
type family IsRightSym1 (a6989586621679266986 :: Either a b) :: Bool where ... Source #
IsRightSym1 a6989586621679266986 = IsRight a6989586621679266986 |