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 | Haskell2010 |
Data.Singletons.Prelude.Either
Description
Defines functions and datatypes relating to the singleton for Either
,
including a singletons version 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 b. 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 a c b (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 family Lefts (a :: [Either a b]) :: [a] where ...
- sLefts :: forall a b (t :: [Either a b]). Sing t -> Sing (Apply LeftsSym0 t :: [a])
- type family Rights (a :: [Either a b]) :: [b] where ...
- sRights :: forall a b (t :: [Either a b]). Sing t -> Sing (Apply RightsSym0 t :: [b])
- type family PartitionEithers (a :: [Either a b]) :: ([a], [b]) where ...
- sPartitionEithers :: forall a b (t :: [Either a b]). Sing t -> Sing (Apply PartitionEithersSym0 t :: ([a], [b]))
- type family IsLeft (a :: Either a b) :: Bool where ...
- sIsLeft :: forall a b (t :: Either a b). Sing t -> Sing (Apply IsLeftSym0 t :: Bool)
- type family IsRight (a :: Either a b) :: Bool where ...
- sIsRight :: forall a b (t :: Either a b). Sing t -> Sing (Apply IsRightSym0 t :: Bool)
- data LeftSym0 :: forall (a6989586621679086104 :: Type) (b6989586621679086105 :: Type). (~>) a6989586621679086104 (Either (a6989586621679086104 :: Type) (b6989586621679086105 :: Type))
- type LeftSym1 (t6989586621679310950 :: a6989586621679086104) = 'Left t6989586621679310950
- data RightSym0 :: forall (b6989586621679086105 :: Type) (a6989586621679086104 :: Type). (~>) b6989586621679086105 (Either (a6989586621679086104 :: Type) (b6989586621679086105 :: Type))
- type RightSym1 (t6989586621679310952 :: b6989586621679086105) = 'Right t6989586621679310952
- data Either_Sym0 :: forall a6989586621680466112 c6989586621680466113 b6989586621680466114. (~>) ((~>) a6989586621680466112 c6989586621680466113) ((~>) ((~>) b6989586621680466114 c6989586621680466113) ((~>) (Either a6989586621680466112 b6989586621680466114) c6989586621680466113))
- data Either_Sym1 (a6989586621680466148 :: (~>) a6989586621680466112 c6989586621680466113) :: forall b6989586621680466114. (~>) ((~>) b6989586621680466114 c6989586621680466113) ((~>) (Either a6989586621680466112 b6989586621680466114) c6989586621680466113)
- data Either_Sym2 (a6989586621680466148 :: (~>) a6989586621680466112 c6989586621680466113) (a6989586621680466149 :: (~>) b6989586621680466114 c6989586621680466113) :: (~>) (Either a6989586621680466112 b6989586621680466114) c6989586621680466113
- type Either_Sym3 (a6989586621680466148 :: (~>) a6989586621680466112 c6989586621680466113) (a6989586621680466149 :: (~>) b6989586621680466114 c6989586621680466113) (a6989586621680466150 :: Either a6989586621680466112 b6989586621680466114) = Either_ a6989586621680466148 a6989586621680466149 a6989586621680466150
- data LeftsSym0 :: forall a6989586621680467594 b6989586621680467595. (~>) [Either a6989586621680467594 b6989586621680467595] [a6989586621680467594]
- type LeftsSym1 (a6989586621680467866 :: [Either a6989586621680467594 b6989586621680467595]) = Lefts a6989586621680467866
- data RightsSym0 :: forall a6989586621680467592 b6989586621680467593. (~>) [Either a6989586621680467592 b6989586621680467593] [b6989586621680467593]
- type RightsSym1 (a6989586621680467861 :: [Either a6989586621680467592 b6989586621680467593]) = Rights a6989586621680467861
- data IsLeftSym0 :: forall a6989586621680467588 b6989586621680467589. (~>) (Either a6989586621680467588 b6989586621680467589) Bool
- type IsLeftSym1 (a6989586621680467837 :: Either a6989586621680467588 b6989586621680467589) = IsLeft a6989586621680467837
- data IsRightSym0 :: forall a6989586621680467586 b6989586621680467587. (~>) (Either a6989586621680467586 b6989586621680467587) Bool
- type IsRightSym1 (a6989586621680467835 :: Either a6989586621680467586 b6989586621680467587) = IsRight a6989586621680467835
The Either
singleton
type family Sing :: k -> Type Source #
The singleton kind-indexed type family.
Instances
data SEither :: forall a b. Either a b -> Type where Source #
Constructors
SLeft :: forall a (n :: a). (Sing (n :: a)) -> SEither ('Left n) | |
SRight :: forall b (n :: b). (Sing (n :: b)) -> SEither ('Right n) |
Instances
(SDecide a, SDecide b) => TestCoercion (SEither :: Either a b -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods 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.Prelude.Instances Methods testEquality :: forall (a0 :: k) (b0 :: k). SEither a0 -> SEither b0 -> Maybe (a0 :~: b0) | |
(ShowSing a, ShowSing b) => Show (SEither z) | |
Singletons from Data.Either
sEither_ :: forall a c b (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) 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 Rights (a :: [Either a b]) :: [b] where ... Source #
Equations
Rights '[] = '[] | |
Rights ('(:) ('Left _) xs) = Apply RightsSym0 xs | |
Rights ('(:) ('Right x) xs) = Apply (Apply (:@#@$) x) (Apply RightsSym0 xs) |
type family PartitionEithers (a :: [Either a b]) :: ([a], [b]) where ... Source #
Equations
PartitionEithers a_6989586621680467839 = Apply (Apply (Apply FoldrSym0 (Apply (Apply Either_Sym0 (Let6989586621680467844LeftSym1 a_6989586621680467839)) (Let6989586621680467844RightSym1 a_6989586621680467839))) (Apply (Apply Tuple2Sym0 '[]) '[])) a_6989586621680467839 |
sPartitionEithers :: forall a b (t :: [Either a b]). Sing t -> Sing (Apply PartitionEithersSym0 t :: ([a], [b])) Source #
Defunctionalization symbols
data LeftSym0 :: forall (a6989586621679086104 :: Type) (b6989586621679086105 :: Type). (~>) a6989586621679086104 (Either (a6989586621679086104 :: Type) (b6989586621679086105 :: Type)) Source #
Instances
SingI (LeftSym0 :: TyFun a (Either a b) -> Type) Source # | |
SuppressUnusedWarnings (LeftSym0 :: TyFun a6989586621679086104 (Either a6989586621679086104 b6989586621679086105) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
type Apply (LeftSym0 :: TyFun a (Either a b6989586621679086105) -> Type) (t6989586621679310950 :: a) Source # | |
Defined in Data.Singletons.Prelude.Instances |
data RightSym0 :: forall (b6989586621679086105 :: Type) (a6989586621679086104 :: Type). (~>) b6989586621679086105 (Either (a6989586621679086104 :: Type) (b6989586621679086105 :: Type)) Source #
Instances
SingI (RightSym0 :: TyFun b (Either a b) -> Type) Source # | |
SuppressUnusedWarnings (RightSym0 :: TyFun b6989586621679086105 (Either a6989586621679086104 b6989586621679086105) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
type Apply (RightSym0 :: TyFun b (Either a6989586621679086104 b) -> Type) (t6989586621679310952 :: b) Source # | |
Defined in Data.Singletons.Prelude.Instances |
type RightSym1 (t6989586621679310952 :: b6989586621679086105) = 'Right t6989586621679310952 Source #
data Either_Sym0 :: forall a6989586621680466112 c6989586621680466113 b6989586621680466114. (~>) ((~>) a6989586621680466112 c6989586621680466113) ((~>) ((~>) b6989586621680466114 c6989586621680466113) ((~>) (Either a6989586621680466112 b6989586621680466114) c6989586621680466113)) Source #
Instances
SingI (Either_Sym0 :: TyFun (a ~> c) ((b ~> c) ~> (Either a b ~> c)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either Methods sing :: Sing Either_Sym0 Source # | |
SuppressUnusedWarnings (Either_Sym0 :: TyFun (a6989586621680466112 ~> c6989586621680466113) ((b6989586621680466114 ~> c6989586621680466113) ~> (Either a6989586621680466112 b6989586621680466114 ~> c6989586621680466113)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either Methods suppressUnusedWarnings :: () Source # | |
type Apply (Either_Sym0 :: TyFun (a6989586621680466112 ~> c6989586621680466113) ((b6989586621680466114 ~> c6989586621680466113) ~> (Either a6989586621680466112 b6989586621680466114 ~> c6989586621680466113)) -> Type) (a6989586621680466148 :: a6989586621680466112 ~> c6989586621680466113) Source # | |
Defined in Data.Singletons.Prelude.Either type Apply (Either_Sym0 :: TyFun (a6989586621680466112 ~> c6989586621680466113) ((b6989586621680466114 ~> c6989586621680466113) ~> (Either a6989586621680466112 b6989586621680466114 ~> c6989586621680466113)) -> Type) (a6989586621680466148 :: a6989586621680466112 ~> c6989586621680466113) = Either_Sym1 a6989586621680466148 b6989586621680466114 :: TyFun (b6989586621680466114 ~> c6989586621680466113) (Either a6989586621680466112 b6989586621680466114 ~> c6989586621680466113) -> Type |
data Either_Sym1 (a6989586621680466148 :: (~>) a6989586621680466112 c6989586621680466113) :: forall b6989586621680466114. (~>) ((~>) b6989586621680466114 c6989586621680466113) ((~>) (Either a6989586621680466112 b6989586621680466114) c6989586621680466113) Source #
Instances
SingI d => SingI (Either_Sym1 d b :: TyFun (b ~> c) (Either a b ~> c) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either Methods sing :: Sing (Either_Sym1 d b) Source # | |
SuppressUnusedWarnings (Either_Sym1 a6989586621680466148 b6989586621680466114 :: TyFun (b6989586621680466114 ~> c6989586621680466113) (Either a6989586621680466112 b6989586621680466114 ~> c6989586621680466113) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either Methods suppressUnusedWarnings :: () Source # | |
type Apply (Either_Sym1 a6989586621680466148 b6989586621680466114 :: TyFun (b6989586621680466114 ~> c6989586621680466113) (Either a6989586621680466112 b6989586621680466114 ~> c6989586621680466113) -> Type) (a6989586621680466149 :: b6989586621680466114 ~> c6989586621680466113) Source # | |
Defined in Data.Singletons.Prelude.Either type Apply (Either_Sym1 a6989586621680466148 b6989586621680466114 :: TyFun (b6989586621680466114 ~> c6989586621680466113) (Either a6989586621680466112 b6989586621680466114 ~> c6989586621680466113) -> Type) (a6989586621680466149 :: b6989586621680466114 ~> c6989586621680466113) = Either_Sym2 a6989586621680466148 a6989586621680466149 |
data Either_Sym2 (a6989586621680466148 :: (~>) a6989586621680466112 c6989586621680466113) (a6989586621680466149 :: (~>) b6989586621680466114 c6989586621680466113) :: (~>) (Either a6989586621680466112 b6989586621680466114) c6989586621680466113 Source #
Instances
(SingI d1, SingI d2) => SingI (Either_Sym2 d1 d2 :: TyFun (Either a b) c -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either Methods sing :: Sing (Either_Sym2 d1 d2) Source # | |
SuppressUnusedWarnings (Either_Sym2 a6989586621680466149 a6989586621680466148 :: TyFun (Either a6989586621680466112 b6989586621680466114) c6989586621680466113 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either Methods suppressUnusedWarnings :: () Source # | |
type Apply (Either_Sym2 a6989586621680466149 a6989586621680466148 :: TyFun (Either a b) c -> Type) (a6989586621680466150 :: Either a b) Source # | |
Defined in Data.Singletons.Prelude.Either type Apply (Either_Sym2 a6989586621680466149 a6989586621680466148 :: TyFun (Either a b) c -> Type) (a6989586621680466150 :: Either a b) = Either_ a6989586621680466149 a6989586621680466148 a6989586621680466150 |
type Either_Sym3 (a6989586621680466148 :: (~>) a6989586621680466112 c6989586621680466113) (a6989586621680466149 :: (~>) b6989586621680466114 c6989586621680466113) (a6989586621680466150 :: Either a6989586621680466112 b6989586621680466114) = Either_ a6989586621680466148 a6989586621680466149 a6989586621680466150 Source #
data LeftsSym0 :: forall a6989586621680467594 b6989586621680467595. (~>) [Either a6989586621680467594 b6989586621680467595] [a6989586621680467594] Source #
Instances
SingI (LeftsSym0 :: TyFun [Either a b] [a] -> Type) Source # | |
SuppressUnusedWarnings (LeftsSym0 :: TyFun [Either a6989586621680467594 b6989586621680467595] [a6989586621680467594] -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either Methods suppressUnusedWarnings :: () Source # | |
type Apply (LeftsSym0 :: TyFun [Either a b] [a] -> Type) (a6989586621680467866 :: [Either a b]) Source # | |
Defined in Data.Singletons.Prelude.Either |
type LeftsSym1 (a6989586621680467866 :: [Either a6989586621680467594 b6989586621680467595]) = Lefts a6989586621680467866 Source #
data RightsSym0 :: forall a6989586621680467592 b6989586621680467593. (~>) [Either a6989586621680467592 b6989586621680467593] [b6989586621680467593] Source #
Instances
SingI (RightsSym0 :: TyFun [Either a b] [b] -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either Methods sing :: Sing RightsSym0 Source # | |
SuppressUnusedWarnings (RightsSym0 :: TyFun [Either a6989586621680467592 b6989586621680467593] [b6989586621680467593] -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either Methods suppressUnusedWarnings :: () Source # | |
type Apply (RightsSym0 :: TyFun [Either a b] [b] -> Type) (a6989586621680467861 :: [Either a b]) Source # | |
Defined in Data.Singletons.Prelude.Either type Apply (RightsSym0 :: TyFun [Either a b] [b] -> Type) (a6989586621680467861 :: [Either a b]) = Rights a6989586621680467861 |
type RightsSym1 (a6989586621680467861 :: [Either a6989586621680467592 b6989586621680467593]) = Rights a6989586621680467861 Source #
data IsLeftSym0 :: forall a6989586621680467588 b6989586621680467589. (~>) (Either a6989586621680467588 b6989586621680467589) Bool Source #
Instances
SingI (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either Methods sing :: Sing IsLeftSym0 Source # | |
SuppressUnusedWarnings (IsLeftSym0 :: TyFun (Either a6989586621680467588 b6989586621680467589) Bool -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either Methods suppressUnusedWarnings :: () Source # | |
type Apply (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) (a6989586621680467837 :: Either a b) Source # | |
Defined in Data.Singletons.Prelude.Either type Apply (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) (a6989586621680467837 :: Either a b) = IsLeft a6989586621680467837 |
type IsLeftSym1 (a6989586621680467837 :: Either a6989586621680467588 b6989586621680467589) = IsLeft a6989586621680467837 Source #
data IsRightSym0 :: forall a6989586621680467586 b6989586621680467587. (~>) (Either a6989586621680467586 b6989586621680467587) Bool Source #
Instances
SingI (IsRightSym0 :: TyFun (Either a b) Bool -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either Methods sing :: Sing IsRightSym0 Source # | |
SuppressUnusedWarnings (IsRightSym0 :: TyFun (Either a6989586621680467586 b6989586621680467587) Bool -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either Methods suppressUnusedWarnings :: () Source # | |
type Apply (IsRightSym0 :: TyFun (Either a b) Bool -> Type) (a6989586621680467835 :: Either a b) Source # | |
Defined in Data.Singletons.Prelude.Either type Apply (IsRightSym0 :: TyFun (Either a b) Bool -> Type) (a6989586621680467835 :: Either a b) = IsRight a6989586621680467835 |
type IsRightSym1 (a6989586621680467835 :: Either a6989586621680467586 b6989586621680467587) = IsRight a6989586621680467835 Source #