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 |
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
- data family Sing :: k -> Type
- type SEither = (Sing :: Either a b -> Type)
- 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 (a6989586621679089135 :: Type) (b6989586621679089136 :: Type). (~>) a6989586621679089135 (Either (a6989586621679089135 :: Type) (b6989586621679089136 :: Type))
- type LeftSym1 (t6989586621679298961 :: a6989586621679089135) = Left t6989586621679298961
- data RightSym0 :: forall (a6989586621679089135 :: Type) (b6989586621679089136 :: Type). (~>) b6989586621679089136 (Either (a6989586621679089135 :: Type) (b6989586621679089136 :: Type))
- type RightSym1 (t6989586621679298963 :: b6989586621679089136) = Right t6989586621679298963
- data Either_Sym0 :: forall a6989586621680432731 b6989586621680432733 c6989586621680432732. (~>) ((~>) a6989586621680432731 c6989586621680432732) ((~>) ((~>) b6989586621680432733 c6989586621680432732) ((~>) (Either a6989586621680432731 b6989586621680432733) c6989586621680432732))
- data Either_Sym1 (a6989586621680432767 :: (~>) a6989586621680432731 c6989586621680432732) :: forall b6989586621680432733. (~>) ((~>) b6989586621680432733 c6989586621680432732) ((~>) (Either a6989586621680432731 b6989586621680432733) c6989586621680432732)
- data Either_Sym2 (a6989586621680432767 :: (~>) a6989586621680432731 c6989586621680432732) (a6989586621680432768 :: (~>) b6989586621680432733 c6989586621680432732) :: (~>) (Either a6989586621680432731 b6989586621680432733) c6989586621680432732
- type Either_Sym3 (a6989586621680432767 :: (~>) a6989586621680432731 c6989586621680432732) (a6989586621680432768 :: (~>) b6989586621680432733 c6989586621680432732) (a6989586621680432769 :: Either a6989586621680432731 b6989586621680432733) = Either_ a6989586621680432767 a6989586621680432768 a6989586621680432769
- data LeftsSym0 :: forall a6989586621680434209 b6989586621680434210. (~>) [Either a6989586621680434209 b6989586621680434210] [a6989586621680434209]
- type LeftsSym1 (a6989586621680434599 :: [Either a6989586621680434209 b6989586621680434210]) = Lefts a6989586621680434599
- data RightsSym0 :: forall a6989586621680434207 b6989586621680434208. (~>) [Either a6989586621680434207 b6989586621680434208] [b6989586621680434208]
- type RightsSym1 (a6989586621680434594 :: [Either a6989586621680434207 b6989586621680434208]) = Rights a6989586621680434594
- data IsLeftSym0 :: forall a6989586621680434203 b6989586621680434204. (~>) (Either a6989586621680434203 b6989586621680434204) Bool
- type IsLeftSym1 (a6989586621680434570 :: Either a6989586621680434203 b6989586621680434204) = IsLeft a6989586621680434570
- data IsRightSym0 :: forall a6989586621680434201 b6989586621680434202. (~>) (Either a6989586621680434201 b6989586621680434202) Bool
- type IsRightSym1 (a6989586621680434568 :: Either a6989586621680434201 b6989586621680434202) = IsRight a6989586621680434568
The Either
singleton
data family Sing :: k -> Type Source #
The singleton kind-indexed data family.
Instances
SDecide k => TestCoercion (Sing :: k -> Type) Source # | |
Defined in Data.Singletons.Decide | |
SDecide k => TestEquality (Sing :: k -> Type) Source # | |
Defined in Data.Singletons.Decide | |
Show (SSymbol s) Source # | |
Show (SNat n) Source # | |
Eq (Sing a) Source # | |
Ord (Sing a) Source # | |
Show (Sing z) Source # | |
(ShowSing a, ShowSing [a]) => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
Show (Sing z) Source # | |
(ShowSing a, ShowSing b) => Show (Sing z) Source # | |
Show (Sing a) Source # | |
Show (Sing z) Source # | |
(ShowSing a, ShowSing b) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c, ShowSing d) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f, ShowSing g) => Show (Sing z) Source # | |
Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
(ShowSing a, ShowSing b) => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing m => Show (Sing z) Source # | |
ShowSing (Maybe a) => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing (Maybe a) => Show (Sing z) Source # | |
ShowSing (Maybe a) => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing Bool => Show (Sing z) Source # | |
ShowSing Bool => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
(ShowSing a, ShowSing [a]) => Show (Sing z) Source # | |
data Sing (a :: Bool) Source # | |
data Sing (a :: Ordering) Source # | |
data Sing (n :: Nat) Source # | |
data Sing (n :: Symbol) Source # | |
Defined in Data.Singletons.TypeLits.Internal | |
data Sing (a :: ()) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
data Sing (a :: Void) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
data Sing (a :: All) Source # | |
data Sing (a :: Any) Source # | |
data Sing (a :: PErrorMessage) Source # | |
Defined in Data.Singletons.TypeError data Sing (a :: PErrorMessage) where
| |
data Sing (b :: [a]) Source # | |
data Sing (b :: Maybe a) Source # | |
data Sing (a :: TYPE rep) Source # | A choice of singleton for the kind Conceivably, one could generalize this instance to `Sing :: k -> Type` for
any kind We cannot produce explicit singleton values for everything in |
Defined in Data.Singletons.TypeRepTYPE | |
data Sing (b :: Min a) Source # | |
data Sing (b :: Max a) Source # | |
data Sing (b :: First a) Source # | |
data Sing (b :: Last a) Source # | |
data Sing (a :: WrappedMonoid m) Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: WrappedMonoid m) where
| |
data Sing (b :: Option a) Source # | |
data Sing (b :: Identity a) Source # | |
data Sing (b :: First a) Source # | |
data Sing (b :: Last a) Source # | |
data Sing (b :: Dual a) Source # | |
data Sing (b :: Sum a) Source # | |
data Sing (b :: Product a) Source # | |
data Sing (b :: Down a) Source # | |
data Sing (b :: NonEmpty a) Source # | |
data Sing (c :: Either a b) Source # | |
data Sing (c :: (a, b)) Source # | |
data Sing (c :: Arg a b) Source # | |
data Sing (f :: k1 ~> k2) Source # | |
data Sing (d :: (a, b, c)) Source # | |
data Sing (c :: Const a b) Source # | |
data Sing (e :: (a, b, c, d)) Source # | |
data Sing (f :: (a, b, c, d, e)) Source # | |
data Sing (g :: (a, b, c, d, e, f)) Source # | |
data Sing (h :: (a, b, c, d, e, f, g)) Source # | |
Defined in Data.Singletons.Prelude.Instances |
Though Haddock doesn't show it, the Sing
instance above declares
constructors
SLeft :: Sing a -> Sing (Left a) SRight :: Sing b -> Sing (Right b)
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 PartitionEithers (a :: [Either a b]) :: ([a], [b]) where ... Source #
PartitionEithers a_6989586621680434572 = Apply (Apply (Apply FoldrSym0 (Apply (Apply Either_Sym0 (Let6989586621680434577LeftSym1 a_6989586621680434572)) (Let6989586621680434577RightSym1 a_6989586621680434572))) (Apply (Apply Tuple2Sym0 '[]) '[])) a_6989586621680434572 |
sPartitionEithers :: forall a b (t :: [Either a b]). Sing t -> Sing (Apply PartitionEithersSym0 t :: ([a], [b])) Source #
Defunctionalization symbols
data LeftSym0 :: forall (a6989586621679089135 :: Type) (b6989586621679089136 :: Type). (~>) a6989586621679089135 (Either (a6989586621679089135 :: Type) (b6989586621679089136 :: Type)) Source #
Instances
SingI (LeftSym0 :: TyFun a (Either a b) -> Type) Source # | |
SuppressUnusedWarnings (LeftSym0 :: TyFun a6989586621679089135 (Either a6989586621679089135 b6989586621679089136) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances suppressUnusedWarnings :: () Source # | |
type Apply (LeftSym0 :: TyFun a (Either a b6989586621679089136) -> Type) (t6989586621679298961 :: a) Source # | |
data RightSym0 :: forall (a6989586621679089135 :: Type) (b6989586621679089136 :: Type). (~>) b6989586621679089136 (Either (a6989586621679089135 :: Type) (b6989586621679089136 :: Type)) Source #
Instances
SingI (RightSym0 :: TyFun b (Either a b) -> Type) Source # | |
SuppressUnusedWarnings (RightSym0 :: TyFun b6989586621679089136 (Either a6989586621679089135 b6989586621679089136) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances suppressUnusedWarnings :: () Source # | |
type Apply (RightSym0 :: TyFun b (Either a6989586621679089135 b) -> Type) (t6989586621679298963 :: b) Source # | |
data Either_Sym0 :: forall a6989586621680432731 b6989586621680432733 c6989586621680432732. (~>) ((~>) a6989586621680432731 c6989586621680432732) ((~>) ((~>) b6989586621680432733 c6989586621680432732) ((~>) (Either a6989586621680432731 b6989586621680432733) c6989586621680432732)) Source #
Instances
SingI (Either_Sym0 :: TyFun (a ~> c) ((b ~> c) ~> (Either a b ~> c)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either sing :: Sing Either_Sym0 Source # | |
SuppressUnusedWarnings (Either_Sym0 :: TyFun (a6989586621680432731 ~> c6989586621680432732) ((b6989586621680432733 ~> c6989586621680432732) ~> (Either a6989586621680432731 b6989586621680432733 ~> c6989586621680432732)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either suppressUnusedWarnings :: () Source # | |
type Apply (Either_Sym0 :: TyFun (a6989586621680432731 ~> c6989586621680432732) ((b6989586621680432733 ~> c6989586621680432732) ~> (Either a6989586621680432731 b6989586621680432733 ~> c6989586621680432732)) -> Type) (a6989586621680432767 :: a6989586621680432731 ~> c6989586621680432732) Source # | |
Defined in Data.Singletons.Prelude.Either type Apply (Either_Sym0 :: TyFun (a6989586621680432731 ~> c6989586621680432732) ((b6989586621680432733 ~> c6989586621680432732) ~> (Either a6989586621680432731 b6989586621680432733 ~> c6989586621680432732)) -> Type) (a6989586621680432767 :: a6989586621680432731 ~> c6989586621680432732) = (Either_Sym1 a6989586621680432767 b6989586621680432733 :: TyFun (b6989586621680432733 ~> c6989586621680432732) (Either a6989586621680432731 b6989586621680432733 ~> c6989586621680432732) -> Type) |
data Either_Sym1 (a6989586621680432767 :: (~>) a6989586621680432731 c6989586621680432732) :: forall b6989586621680432733. (~>) ((~>) b6989586621680432733 c6989586621680432732) ((~>) (Either a6989586621680432731 b6989586621680432733) c6989586621680432732) Source #
Instances
SingI d => SingI (Either_Sym1 d b :: TyFun (b ~> c) (Either a b ~> c) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either sing :: Sing (Either_Sym1 d b) Source # | |
SuppressUnusedWarnings (Either_Sym1 a6989586621680432767 b6989586621680432733 :: TyFun (b6989586621680432733 ~> c6989586621680432732) (Either a6989586621680432731 b6989586621680432733 ~> c6989586621680432732) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either suppressUnusedWarnings :: () Source # | |
type Apply (Either_Sym1 a6989586621680432767 b6989586621680432733 :: TyFun (b6989586621680432733 ~> c6989586621680432732) (Either a6989586621680432731 b6989586621680432733 ~> c6989586621680432732) -> Type) (a6989586621680432768 :: b6989586621680432733 ~> c6989586621680432732) Source # | |
Defined in Data.Singletons.Prelude.Either type Apply (Either_Sym1 a6989586621680432767 b6989586621680432733 :: TyFun (b6989586621680432733 ~> c6989586621680432732) (Either a6989586621680432731 b6989586621680432733 ~> c6989586621680432732) -> Type) (a6989586621680432768 :: b6989586621680432733 ~> c6989586621680432732) = Either_Sym2 a6989586621680432767 a6989586621680432768 |
data Either_Sym2 (a6989586621680432767 :: (~>) a6989586621680432731 c6989586621680432732) (a6989586621680432768 :: (~>) b6989586621680432733 c6989586621680432732) :: (~>) (Either a6989586621680432731 b6989586621680432733) c6989586621680432732 Source #
Instances
(SingI d1, SingI d2) => SingI (Either_Sym2 d1 d2 :: TyFun (Either a b) c -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either sing :: Sing (Either_Sym2 d1 d2) Source # | |
SuppressUnusedWarnings (Either_Sym2 a6989586621680432768 a6989586621680432767 :: TyFun (Either a6989586621680432731 b6989586621680432733) c6989586621680432732 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either suppressUnusedWarnings :: () Source # | |
type Apply (Either_Sym2 a6989586621680432768 a6989586621680432767 :: TyFun (Either a b) c -> Type) (a6989586621680432769 :: Either a b) Source # | |
Defined in Data.Singletons.Prelude.Either |
type Either_Sym3 (a6989586621680432767 :: (~>) a6989586621680432731 c6989586621680432732) (a6989586621680432768 :: (~>) b6989586621680432733 c6989586621680432732) (a6989586621680432769 :: Either a6989586621680432731 b6989586621680432733) = Either_ a6989586621680432767 a6989586621680432768 a6989586621680432769 Source #
data LeftsSym0 :: forall a6989586621680434209 b6989586621680434210. (~>) [Either a6989586621680434209 b6989586621680434210] [a6989586621680434209] Source #
Instances
SingI (LeftsSym0 :: TyFun [Either a b] [a] -> Type) Source # | |
SuppressUnusedWarnings (LeftsSym0 :: TyFun [Either a6989586621680434209 b6989586621680434210] [a6989586621680434209] -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either suppressUnusedWarnings :: () Source # | |
type Apply (LeftsSym0 :: TyFun [Either a b] [a] -> Type) (a6989586621680434599 :: [Either a b]) Source # | |
type LeftsSym1 (a6989586621680434599 :: [Either a6989586621680434209 b6989586621680434210]) = Lefts a6989586621680434599 Source #
data RightsSym0 :: forall a6989586621680434207 b6989586621680434208. (~>) [Either a6989586621680434207 b6989586621680434208] [b6989586621680434208] Source #
Instances
SingI (RightsSym0 :: TyFun [Either a b] [b] -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either sing :: Sing RightsSym0 Source # | |
SuppressUnusedWarnings (RightsSym0 :: TyFun [Either a6989586621680434207 b6989586621680434208] [b6989586621680434208] -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either suppressUnusedWarnings :: () Source # | |
type Apply (RightsSym0 :: TyFun [Either a b] [b] -> Type) (a6989586621680434594 :: [Either a b]) Source # | |
Defined in Data.Singletons.Prelude.Either |
type RightsSym1 (a6989586621680434594 :: [Either a6989586621680434207 b6989586621680434208]) = Rights a6989586621680434594 Source #
data IsLeftSym0 :: forall a6989586621680434203 b6989586621680434204. (~>) (Either a6989586621680434203 b6989586621680434204) Bool Source #
Instances
SingI (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either sing :: Sing IsLeftSym0 Source # | |
SuppressUnusedWarnings (IsLeftSym0 :: TyFun (Either a6989586621680434203 b6989586621680434204) Bool -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either suppressUnusedWarnings :: () Source # | |
type Apply (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) (a6989586621680434570 :: Either a b) Source # | |
Defined in Data.Singletons.Prelude.Either |
type IsLeftSym1 (a6989586621680434570 :: Either a6989586621680434203 b6989586621680434204) = IsLeft a6989586621680434570 Source #
data IsRightSym0 :: forall a6989586621680434201 b6989586621680434202. (~>) (Either a6989586621680434201 b6989586621680434202) Bool Source #
Instances
SingI (IsRightSym0 :: TyFun (Either a b) Bool -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either sing :: Sing IsRightSym0 Source # | |
SuppressUnusedWarnings (IsRightSym0 :: TyFun (Either a6989586621680434201 b6989586621680434202) Bool -> Type) Source # | |
Defined in Data.Singletons.Prelude.Either suppressUnusedWarnings :: () Source # | |
type Apply (IsRightSym0 :: TyFun (Either a b) Bool -> Type) (a6989586621680434568 :: Either a b) Source # | |
Defined in Data.Singletons.Prelude.Either |
type IsRightSym1 (a6989586621680434568 :: Either a6989586621680434201 b6989586621680434202) = IsRight a6989586621680434568 Source #