Data.Singletons.Prelude.Either

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.

The Either singleton

data family Sing (a :: k)

The singleton kind-indexed data family.

Instances

data Sing Bool

data Sing Bool where

• SFalse :: Sing Bool z
• STrue :: Sing Bool z

data Sing Ordering

data Sing Ordering where

• SLT :: Sing Ordering z
• SEQ :: Sing Ordering z
• SGT :: Sing Ordering z

data Sing *

data Sing * where

• STypeRep :: Sing * a

data Sing Nat

data Sing Nat where

• SNat :: Sing Nat n

data Sing Symbol

data Sing Symbol where

• SSym :: Sing Symbol n

data Sing ()

data Sing () where

• STuple0 :: Sing () z

data Sing [a0]

data Sing [a0] where

• SNil :: Sing [a] z
• SCons :: Sing [a] z

data Sing (Maybe a0)

data Sing (Maybe a0) where

• SNothing :: Sing (Maybe a) z
• SJust :: Sing (Maybe a) z

data Sing (NonEmpty a0)

data Sing (NonEmpty a0) where

• (:%|) :: Sing (NonEmpty a) z

data Sing (Either a0 b0)

data Sing (Either a0 b0) where

• SLeft :: Sing (Either a b) z
• SRight :: Sing (Either a b) z

data Sing (a0, b0)

data Sing (a0, b0) where

• STuple2 :: Sing (a, b) z

data Sing ((~>) k1 k2)

data Sing ((~>) k1 k2) = SLambda {

• applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k1 k2 f t)

}

data Sing (a0, b0, c0)

data Sing (a0, b0, c0) where

• STuple3 :: Sing (a, b, c) z

data Sing (a0, b0, c0, d0)

data Sing (a0, b0, c0, d0) where

• STuple4 :: Sing (a, b, c, d) z

data Sing (a0, b0, c0, d0, e0)

data Sing (a0, b0, c0, d0, e0) where

• STuple5 :: Sing (a, b, c, d, e) z

data Sing (a0, b0, c0, d0, e0, f0)

data Sing (a0, b0, c0, d0, e0, f0) where

• STuple6 :: Sing (a, b, c, d, e, f) z

data Sing (a0, b0, c0, d0, e0, f0, g0)

data Sing (a0, b0, c0, d0, e0, f0, g0) where

• STuple7 :: Sing (a, b, c, d, e, f, g) z

Though Haddock doesn't show it, the Sing instance above declares constructors

SLeft  :: Sing a -> Sing (Left a)
SRight :: Sing b -> Sing (Right b)

type SEither = (Sing :: Either a b -> Type)

SEither is a kind-restricted synonym for Sing: type SEither (a :: Either x y) = Sing a

Singletons from Data.Either

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

type family Either_ (a :: TyFun a c -> Type) (a :: TyFun b c -> Type) (a :: Either a b) :: c where ...

Equations

Either_ f _z_1627829204 (Left x) = Apply f x

Either_ _z_1627829208 g (Right y) = Apply g y

sEither_ :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Either_Sym0 t) t) t :: c)

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 :: [Either a b]) :: [a] where ...

Equations

Lefts '[] = '[]

Lefts ((:) (Left x) xs) = Apply (Apply (:$) x) (Apply LeftsSym0 xs)

Lefts ((:) (Right _z_1627830553) xs) = Apply LeftsSym0 xs

sLefts :: forall t. Sing t -> Sing (Apply LeftsSym0 t :: [a])

type family Rights (a :: [Either a b]) :: [b] where ...

Equations

Rights '[] = '[]

Rights ((:) (Left _z_1627830541) xs) = Apply RightsSym0 xs

Rights ((:) (Right x) xs) = Apply (Apply (:$) x) (Apply RightsSym0 xs)

sRights :: forall t. Sing t -> Sing (Apply RightsSym0 t :: [b])

type family PartitionEithers (a :: [Either a b]) :: ([a], [b]) where ...

Equations

PartitionEithers a_1627830495 = Apply (Apply (Apply FoldrSym0 (Apply (Apply Either_Sym0 (Let1627830502LeftSym1 a_1627830495)) (Let1627830502RightSym1 a_1627830495))) (Apply (Apply Tuple2Sym0 '[]) '[])) a_1627830495

sPartitionEithers :: forall t. Sing t -> Sing (Apply PartitionEithersSym0 t :: ([a], [b]))

type family IsLeft (a :: Either a b) :: Bool where ...

Equations

IsLeft (Left _z_1627830489) = TrueSym0

IsLeft (Right _z_1627830492) = FalseSym0

sIsLeft :: forall t. Sing t -> Sing (Apply IsLeftSym0 t :: Bool)

type family IsRight (a :: Either a b) :: Bool where ...

Equations

IsRight (Left _z_1627830479) = FalseSym0

IsRight (Right _z_1627830482) = TrueSym0

sIsRight :: forall t. Sing t -> Sing (Apply IsRightSym0 t :: Bool)

Defunctionalization symbols

data LeftSym0 l

Instances

SuppressUnusedWarnings (TyFun a1627437720 (Either a1627437720 b1627437721) -> *) (LeftSym0 a1627437720 b1627437721)

Methods

suppressUnusedWarnings :: Proxy (LeftSym0 a1627437720 b1627437721) t -> ()

type Apply a1627437720 (Either a1627437720 b1627437721) (LeftSym0 a1627437720 b1627437721) l0

type Apply a1627437720 (Either a1627437720 b1627437721) (LeftSym0 a1627437720 b1627437721) l0 = LeftSym1 a1627437720 b1627437721 l0

type LeftSym1 t = Left t

data RightSym0 l

Instances

SuppressUnusedWarnings (TyFun b1627437721 (Either a1627437720 b1627437721) -> *) (RightSym0 a1627437720 b1627437721)

Methods

suppressUnusedWarnings :: Proxy (RightSym0 a1627437720 b1627437721) t -> ()

type Apply b1627437721 (Either a1627437720 b1627437721) (RightSym0 a1627437720 b1627437721) l0

type Apply b1627437721 (Either a1627437720 b1627437721) (RightSym0 a1627437720 b1627437721) l0 = RightSym1 b1627437721 a1627437720 l0

type RightSym1 t = Right t

data Either_Sym0 l

Instances

SuppressUnusedWarnings (TyFun (TyFun a1627829180 c1627829181 -> Type) (TyFun (TyFun b1627829182 c1627829181 -> Type) (TyFun (Either a1627829180 b1627829182) c1627829181 -> Type) -> Type) -> *) (Either_Sym0 a1627829180 b1627829182 c1627829181)

Methods

suppressUnusedWarnings :: Proxy (Either_Sym0 a1627829180 b1627829182 c1627829181) t -> ()

type Apply (TyFun a1627829180 c1627829181 -> Type) (TyFun (TyFun b1627829182 c1627829181 -> Type) (TyFun (Either a1627829180 b1627829182) c1627829181 -> Type) -> Type) (Either_Sym0 a1627829180 b1627829182 c1627829181) l0

type Apply (TyFun a1627829180 c1627829181 -> Type) (TyFun (TyFun b1627829182 c1627829181 -> Type) (TyFun (Either a1627829180 b1627829182) c1627829181 -> Type) -> Type) (Either_Sym0 a1627829180 b1627829182 c1627829181) l0 = Either_Sym1 b1627829182 a1627829180 c1627829181 l0

data Either_Sym1 l l

Instances

SuppressUnusedWarnings ((TyFun a1627829180 c1627829181 -> Type) -> TyFun (TyFun b1627829182 c1627829181 -> Type) (TyFun (Either a1627829180 b1627829182) c1627829181 -> Type) -> *) (Either_Sym1 b1627829182 a1627829180 c1627829181)

Methods

suppressUnusedWarnings :: Proxy (Either_Sym1 b1627829182 a1627829180 c1627829181) t -> ()

type Apply (TyFun b1627829182 c1627829181 -> Type) (TyFun (Either a1627829180 b1627829182) c1627829181 -> Type) (Either_Sym1 b1627829182 a1627829180 c1627829181 l1) l0

type Apply (TyFun b1627829182 c1627829181 -> Type) (TyFun (Either a1627829180 b1627829182) c1627829181 -> Type) (Either_Sym1 b1627829182 a1627829180 c1627829181 l1) l0 = Either_Sym2 b1627829182 a1627829180 c1627829181 l1 l0

data Either_Sym2 l l l

Instances

SuppressUnusedWarnings ((TyFun a1627829180 c1627829181 -> Type) -> (TyFun b1627829182 c1627829181 -> Type) -> TyFun (Either a1627829180 b1627829182) c1627829181 -> *) (Either_Sym2 b1627829182 a1627829180 c1627829181)

Methods

suppressUnusedWarnings :: Proxy (Either_Sym2 b1627829182 a1627829180 c1627829181) t -> ()

type Apply (Either a1627829180 b1627829182) c1627829181 (Either_Sym2 b1627829182 a1627829180 c1627829181 l1 l2) l0

type Apply (Either a1627829180 b1627829182) c1627829181 (Either_Sym2 b1627829182 a1627829180 c1627829181 l1 l2) l0 = Either_Sym3 a1627829180 c1627829181 b1627829182 l1 l2 l0

type Either_Sym3 t t t = Either_ t t t

data LeftsSym0 l

Instances

SuppressUnusedWarnings (TyFun [Either a1627830454 b1627830455] [a1627830454] -> *) (LeftsSym0 b1627830455 a1627830454)

Methods

suppressUnusedWarnings :: Proxy (LeftsSym0 b1627830455 a1627830454) t -> ()

type Apply [Either a1627830454 b1627830455] [a1627830454] (LeftsSym0 b1627830455 a1627830454) l0

type Apply [Either a1627830454 b1627830455] [a1627830454] (LeftsSym0 b1627830455 a1627830454) l0 = LeftsSym1 a1627830454 b1627830455 l0

type LeftsSym1 t = Lefts t

data RightsSym0 l

Instances

SuppressUnusedWarnings (TyFun [Either a1627830452 b1627830453] [b1627830453] -> *) (RightsSym0 a1627830452 b1627830453)

Methods

suppressUnusedWarnings :: Proxy (RightsSym0 a1627830452 b1627830453) t -> ()

type Apply [Either a1627830452 b1627830453] [b1627830453] (RightsSym0 a1627830452 b1627830453) l0

type Apply [Either a1627830452 b1627830453] [b1627830453] (RightsSym0 a1627830452 b1627830453) l0 = RightsSym1 a1627830452 b1627830453 l0

type RightsSym1 t = Rights t

data IsLeftSym0 l

Instances

SuppressUnusedWarnings (TyFun (Either a1627830448 b1627830449) Bool -> *) (IsLeftSym0 a1627830448 b1627830449)

Methods

suppressUnusedWarnings :: Proxy (IsLeftSym0 a1627830448 b1627830449) t -> ()

type Apply (Either a1627830448 b1627830449) Bool (IsLeftSym0 a1627830448 b1627830449) l0

type Apply (Either a1627830448 b1627830449) Bool (IsLeftSym0 a1627830448 b1627830449) l0 = IsLeftSym1 a1627830448 b1627830449 l0

type IsLeftSym1 t = IsLeft t

data IsRightSym0 l

Instances

SuppressUnusedWarnings (TyFun (Either a1627830446 b1627830447) Bool -> *) (IsRightSym0 a1627830446 b1627830447)

Methods

suppressUnusedWarnings :: Proxy (IsRightSym0 a1627830446 b1627830447) t -> ()

type Apply (Either a1627830446 b1627830447) Bool (IsRightSym0 a1627830446 b1627830447) l0

type Apply (Either a1627830446 b1627830447) Bool (IsRightSym0 a1627830446 b1627830447) l0 = IsRightSym1 a1627830446 b1627830447 l0

type IsRightSym1 t = IsRight t