singletons-1.0: A framework for generating singleton types

Data.Promotion.Prelude.Either

Description

Defines promoted functions and datatypes relating to `Either`, including a promoted 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

# Promoted functions from `Data.Either`

either_ :: forall a c b. (a -> c) -> (b -> c) -> Either a b -> c Source

type family Either_ a a a :: c Source

Equations

 Either_ f z (Left x) = Apply f x Either_ z g (Right y) = Apply g y

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 a :: [] a Source

Equations

 Lefts [] = [] Lefts ((:) (Left x) xs) = Apply (Apply (:\$) x) (Apply LeftsSym0 xs) Lefts ((:) (Right z) xs) = Apply LeftsSym0 xs

type family Rights a :: [] b Source

Equations

 Rights [] = [] Rights ((:) (Left z) xs) = Apply RightsSym0 xs Rights ((:) (Right x) xs) = Apply (Apply (:\$) x) (Apply RightsSym0 xs)

type family PartitionEithers a :: (,) ([] a) ([] b) Source

Equations

 PartitionEithers a_1627864927 = Apply (Apply (Apply FoldrSym0 (Apply (Apply Either_Sym0 (Let_1627864934LeftSym1 a_1627864927)) (Let_1627864934RightSym1 a_1627864927))) (Apply (Apply Tuple2Sym0 []) [])) a_1627864927

type family IsLeft a :: Bool Source

Equations

 IsLeft (Left z) = TrueSym0 IsLeft (Right z) = FalseSym0

type family IsRight a :: Bool Source

Equations

 IsRight (Left z) = FalseSym0 IsRight (Right z) = TrueSym0

# Defunctionalization symbols

data LeftSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun k (Either k k) -> *) (LeftSym0 k k) type Apply (Either k k1) k (LeftSym0 k1 k) l0 = LeftSym1 k k1 l0

type LeftSym1 t = Left t Source

data RightSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun k (Either k k) -> *) (RightSym0 k k) type Apply (Either k k1) k1 (RightSym0 k k1) l0 = RightSym1 k k1 l0

data Either_Sym0 l Source

Instances

 SuppressUnusedWarnings (TyFun (TyFun k k -> *) (TyFun (TyFun k k -> *) (TyFun (Either k k) k -> *) -> *) -> *) (Either_Sym0 k k k) type Apply (TyFun (TyFun k2 k -> *) (TyFun (Either k1 k2) k -> *) -> *) (TyFun k1 k -> *) (Either_Sym0 k2 k k1) l0 = Either_Sym1 k k1 k2 l0

data Either_Sym1 l l Source

Instances

 SuppressUnusedWarnings ((TyFun k k -> *) -> TyFun (TyFun k k -> *) (TyFun (Either k k) k -> *) -> *) (Either_Sym1 k k k) type Apply (TyFun (Either k2 k) k1 -> *) (TyFun k k1 -> *) (Either_Sym1 k1 k2 k l1) l0 = Either_Sym2 k1 k2 k l1 l0

data Either_Sym2 l l l Source

Instances

 SuppressUnusedWarnings ((TyFun k k -> *) -> (TyFun k k -> *) -> TyFun (Either k k) k -> *) (Either_Sym2 k k k) type Apply k (Either k1 k2) (Either_Sym2 k k1 k2 l1 l2) l0 = Either_Sym3 k k1 k2 l1 l2 l0

type Either_Sym3 t t t = Either_ t t t Source

data LeftsSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun [Either k k] [k] -> *) (LeftsSym0 k k) type Apply [k] [Either k k1] (LeftsSym0 k k1) l0 = LeftsSym1 k k1 l0

data RightsSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun [Either k k] [k] -> *) (RightsSym0 k k) type Apply [k] [Either k1 k] (RightsSym0 k1 k) l0 = RightsSym1 k1 k l0

data IsLeftSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun (Either k k) Bool -> *) (IsLeftSym0 k k) type Apply Bool (Either k k1) (IsLeftSym0 k k1) l0 = IsLeftSym1 k k1 l0

data IsRightSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun (Either k k) Bool -> *) (IsRightSym0 k k) type Apply Bool (Either k k1) (IsRightSym0 k k1) l0 = IsRightSym1 k k1 l0