Copyright | (C) 2013-2014 Richard Eisenberg Jan Stolarek |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Ryan Scott |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
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 (a1 :: Either a b) where
- either_ :: (a -> c) -> (b -> c) -> Either a b -> c
- type family Either_ (a1 :: a ~> c) (a2 :: b ~> c) (a3 :: Either a b) :: c where ...
- sEither_ :: forall a c b (t1 :: a ~> c) (t2 :: b ~> c) (t3 :: Either a b). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (Either_Sym0 :: TyFun (a ~> c) ((b ~> c) ~> (Either a b ~> c)) -> Type) t1) t2) t3)
- type family Lefts (a1 :: [Either a b]) :: [a] where ...
- sLefts :: forall a b (t :: [Either a b]). Sing t -> Sing (Apply (LeftsSym0 :: TyFun [Either a b] [a] -> Type) t)
- type family Rights (a1 :: [Either a b]) :: [b] where ...
- sRights :: forall a b (t :: [Either a b]). Sing t -> Sing (Apply (RightsSym0 :: TyFun [Either a b] [b] -> Type) t)
- type family PartitionEithers (a1 :: [Either a b]) :: ([a], [b]) where ...
- sPartitionEithers :: forall a b (t :: [Either a b]). Sing t -> Sing (Apply (PartitionEithersSym0 :: TyFun [Either a b] ([a], [b]) -> Type) t)
- type family IsLeft (a1 :: Either a b) :: Bool where ...
- sIsLeft :: forall a b (t :: Either a b). Sing t -> Sing (Apply (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) t)
- type family IsRight (a1 :: Either a b) :: Bool where ...
- sIsRight :: forall a b (t :: Either a b). Sing t -> Sing (Apply (IsRightSym0 :: TyFun (Either a b) Bool -> Type) t)
- data LeftSym0 (a1 :: TyFun a (Either a b))
- type family LeftSym1 (a6989586621679046286 :: a) :: Either a b where ...
- data RightSym0 (a1 :: TyFun b (Either a b))
- type family RightSym1 (a6989586621679046288 :: b) :: Either a b where ...
- data Either_Sym0 (a1 :: TyFun (a ~> c) ((b ~> c) ~> (Either a b ~> c)))
- data Either_Sym1 (a6989586621679334944 :: a ~> c) (b1 :: TyFun (b ~> c) (Either a b ~> c))
- data Either_Sym2 (a6989586621679334944 :: a ~> c) (a6989586621679334945 :: b ~> c) (c1 :: TyFun (Either a b) c)
- type family Either_Sym3 (a6989586621679334944 :: a ~> c) (a6989586621679334945 :: b ~> c) (a6989586621679334946 :: Either a b) :: c where ...
- data LeftsSym0 (a1 :: TyFun [Either a b] [a])
- type family LeftsSym1 (a6989586621679337128 :: [Either a b]) :: [a] where ...
- data RightsSym0 (a1 :: TyFun [Either a b] [b])
- type family RightsSym1 (a6989586621679337122 :: [Either a b]) :: [b] where ...
- data IsLeftSym0 (a1 :: TyFun (Either a b) Bool)
- type family IsLeftSym1 (a6989586621679337100 :: Either a b) :: Bool where ...
- data IsRightSym0 (a1 :: TyFun (Either a b) Bool)
- type family IsRightSym1 (a6989586621679337097 :: Either a b) :: Bool where ...
The Either
singleton
type family Sing :: k -> Type #
Instances
data SEither (a1 :: Either a b) where Source #
SLeft :: forall a b (n :: a). Sing n -> SEither ('Left n :: Either a b) | |
SRight :: forall a b (n :: b). Sing n -> SEither ('Right n :: Either a b) |
Instances
(SDecide a, SDecide b) => TestCoercion (SEither :: Either a b -> Type) Source # | |
Defined in Data.Singletons.Base.Instances | |
(SDecide a, SDecide b) => TestEquality (SEither :: Either a b -> Type) Source # | |
Defined in Data.Singletons.Base.Instances | |
(ShowSing a, ShowSing b) => Show (SEither z) Source # | |
Eq (SEither z) Source # | |
Singletons from Data.Either
sEither_ :: forall a c b (t1 :: a ~> c) (t2 :: b ~> c) (t3 :: Either a b). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (Either_Sym0 :: TyFun (a ~> c) ((b ~> c) ~> (Either a b ~> c)) -> Type) t1) t2) t3) 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 Lefts (a1 :: [Either a b]) :: [a] where ... Source #
Lefts ('[] :: [Either a b]) = NilSym0 :: [a] | |
Lefts (('Left x :: Either a b) ': xs :: [Either a b]) = Apply (Apply ((:@#@$) :: TyFun a ([a] ~> [a]) -> Type) x) (Apply (LeftsSym0 :: TyFun [Either a b] [a] -> Type) xs) | |
Lefts (('Right _1 :: Either a b) ': xs :: [Either a b]) = Apply (LeftsSym0 :: TyFun [Either a b] [a] -> Type) xs |
sLefts :: forall a b (t :: [Either a b]). Sing t -> Sing (Apply (LeftsSym0 :: TyFun [Either a b] [a] -> Type) t) Source #
type family Rights (a1 :: [Either a b]) :: [b] where ... Source #
Rights ('[] :: [Either a b]) = NilSym0 :: [b] | |
Rights (('Left _1 :: Either a b) ': xs :: [Either a b]) = Apply (RightsSym0 :: TyFun [Either a b] [b] -> Type) xs | |
Rights (('Right x :: Either a b) ': xs :: [Either a b]) = Apply (Apply ((:@#@$) :: TyFun b ([b] ~> [b]) -> Type) x) (Apply (RightsSym0 :: TyFun [Either a b] [b] -> Type) xs) |
sRights :: forall a b (t :: [Either a b]). Sing t -> Sing (Apply (RightsSym0 :: TyFun [Either a b] [b] -> Type) t) Source #
type family PartitionEithers (a1 :: [Either a b]) :: ([a], [b]) where ... Source #
PartitionEithers (a_6989586621679337101 :: [Either a b]) = Apply (Apply (Apply (FoldrSym0 :: TyFun (Either a b ~> (([a], [b]) ~> ([a], [b]))) (([a], [b]) ~> ([Either a b] ~> ([a], [b]))) -> Type) (Apply (Apply (Either_Sym0 :: TyFun (a ~> (TyFun ([a], [b]) ([a], [b]) -> Type)) ((b ~> (TyFun ([a], [b]) ([a], [b]) -> Type)) ~> (Either a b ~> (TyFun ([a], [b]) ([a], [b]) -> Type))) -> Type) (Let6989586621679337107LeftSym1 a_6989586621679337101 :: TyFun a (TyFun ([a], [b]) ([a], [b]) -> Type) -> Type)) (Let6989586621679337107RightSym1 a_6989586621679337101 :: TyFun b (TyFun ([a], [b]) ([a], [b]) -> Type) -> Type))) (Apply (Apply (Tuple2Sym0 :: TyFun [a] ([b] ~> ([a], [b])) -> Type) (NilSym0 :: [a])) (NilSym0 :: [b]))) a_6989586621679337101 |
sPartitionEithers :: forall a b (t :: [Either a b]). Sing t -> Sing (Apply (PartitionEithersSym0 :: TyFun [Either a b] ([a], [b]) -> Type) t) Source #
sIsLeft :: forall a b (t :: Either a b). Sing t -> Sing (Apply (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) t) Source #
sIsRight :: forall a b (t :: Either a b). Sing t -> Sing (Apply (IsRightSym0 :: TyFun (Either a b) Bool -> Type) t) Source #
Defunctionalization symbols
data LeftSym0 (a1 :: TyFun a (Either a b)) Source #
Instances
data RightSym0 (a1 :: TyFun b (Either a b)) Source #
Instances
data Either_Sym0 (a1 :: TyFun (a ~> c) ((b ~> c) ~> (Either a b ~> c))) Source #
Instances
SingI (Either_Sym0 :: TyFun (a ~> c) ((b ~> c) ~> (Either a b ~> c)) -> Type) Source # | |
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) (a6989586621679334944 :: a ~> c) Source # | |
data Either_Sym1 (a6989586621679334944 :: a ~> c) (b1 :: TyFun (b ~> c) (Either a b ~> c)) Source #
Instances
SingI1 (Either_Sym1 :: (a ~> c) -> TyFun (b ~> c) (Either a b ~> c) -> Type) Source # | |
SingI d => SingI (Either_Sym1 d :: TyFun (b ~> c) (Either a b ~> c) -> Type) Source # | |
Defined in Data.Either.Singletons | |
SuppressUnusedWarnings (Either_Sym1 a6989586621679334944 :: TyFun (b ~> c) (Either a b ~> c) -> Type) Source # | |
Defined in Data.Either.Singletons suppressUnusedWarnings :: () # | |
type Apply (Either_Sym1 a6989586621679334944 :: TyFun (b ~> c) (Either a b ~> c) -> Type) (a6989586621679334945 :: b ~> c) Source # | |
Defined in Data.Either.Singletons type Apply (Either_Sym1 a6989586621679334944 :: TyFun (b ~> c) (Either a b ~> c) -> Type) (a6989586621679334945 :: b ~> c) = Either_Sym2 a6989586621679334944 a6989586621679334945 |
data Either_Sym2 (a6989586621679334944 :: a ~> c) (a6989586621679334945 :: b ~> c) (c1 :: TyFun (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 | |
(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 a6989586621679334944 a6989586621679334945 :: TyFun (Either a b) c -> Type) Source # | |
Defined in Data.Either.Singletons suppressUnusedWarnings :: () # | |
type Apply (Either_Sym2 a6989586621679334944 a6989586621679334945 :: TyFun (Either a b) c -> Type) (a6989586621679334946 :: Either a b) Source # | |
Defined in Data.Either.Singletons |
type family Either_Sym3 (a6989586621679334944 :: a ~> c) (a6989586621679334945 :: b ~> c) (a6989586621679334946 :: Either a b) :: c where ... Source #
Either_Sym3 (a6989586621679334944 :: a ~> c) (a6989586621679334945 :: b ~> c) (a6989586621679334946 :: Either a b) = Either_ a6989586621679334944 a6989586621679334945 a6989586621679334946 |
data LeftsSym0 (a1 :: TyFun [Either a b] [a]) Source #
Instances
SingI (LeftsSym0 :: TyFun [Either a b] [a] -> Type) Source # | |
SuppressUnusedWarnings (LeftsSym0 :: TyFun [Either a b] [a] -> Type) Source # | |
Defined in Data.Either.Singletons suppressUnusedWarnings :: () # | |
type Apply (LeftsSym0 :: TyFun [Either a b] [a] -> Type) (a6989586621679337128 :: [Either a b]) Source # | |
data RightsSym0 (a1 :: TyFun [Either a b] [b]) Source #
Instances
SingI (RightsSym0 :: TyFun [Either a b] [b] -> Type) Source # | |
Defined in Data.Either.Singletons | |
SuppressUnusedWarnings (RightsSym0 :: TyFun [Either a b] [b] -> Type) Source # | |
Defined in Data.Either.Singletons suppressUnusedWarnings :: () # | |
type Apply (RightsSym0 :: TyFun [Either a b] [b] -> Type) (a6989586621679337122 :: [Either a b]) Source # | |
Defined in Data.Either.Singletons |
type family RightsSym1 (a6989586621679337122 :: [Either a b]) :: [b] where ... Source #
RightsSym1 (a6989586621679337122 :: [Either a b]) = Rights a6989586621679337122 |
data IsLeftSym0 (a1 :: TyFun (Either a b) Bool) Source #
Instances
SingI (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) Source # | |
Defined in Data.Either.Singletons | |
SuppressUnusedWarnings (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) Source # | |
Defined in Data.Either.Singletons suppressUnusedWarnings :: () # | |
type Apply (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) (a6989586621679337100 :: Either a b) Source # | |
Defined in Data.Either.Singletons |
type family IsLeftSym1 (a6989586621679337100 :: Either a b) :: Bool where ... Source #
IsLeftSym1 (a6989586621679337100 :: Either a b) = IsLeft a6989586621679337100 |
data IsRightSym0 (a1 :: TyFun (Either a b) Bool) Source #
Instances
SingI (IsRightSym0 :: TyFun (Either a b) Bool -> Type) Source # | |
Defined in Data.Either.Singletons | |
SuppressUnusedWarnings (IsRightSym0 :: TyFun (Either a b) Bool -> Type) Source # | |
Defined in Data.Either.Singletons suppressUnusedWarnings :: () # | |
type Apply (IsRightSym0 :: TyFun (Either a b) Bool -> Type) (a6989586621679337097 :: Either a b) Source # | |
Defined in Data.Either.Singletons |
type family IsRightSym1 (a6989586621679337097 :: Either a b) :: Bool where ... Source #
IsRightSym1 (a6989586621679337097 :: Either a b) = IsRight a6989586621679337097 |