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 (z :: Bool)

data Sing (z :: Bool) where

• SFalse :: Sing False
• STrue :: Sing True

data Sing (z :: Ordering)

data Sing (z :: Ordering) where

• SLT :: Sing LT
• SEQ :: Sing EQ
• SGT :: Sing GT

data Sing (a :: Type)

data Sing (a :: Type) = STypeRep (TypeRep a)

data Sing (n :: Nat)

data Sing (n :: Nat) where

• SNat :: Sing n

data Sing (n :: Symbol)

data Sing (n :: Symbol) where

• SSym :: Sing n

data Sing (z :: ())

data Sing (z :: ()) where

• STuple0 :: Sing ()

data Sing (z :: Void)

data Sing (z :: Void)

data Sing (z :: [a])

data Sing (z :: [a]) where

• SNil :: Sing ([] :: [k])
• SCons :: Sing (n ': n)

data Sing (z :: Maybe a)

data Sing (z :: Maybe a) where

• SNothing :: Sing (Nothing :: Maybe a)
• SJust :: Sing (Just n)

data Sing (z :: NonEmpty a)

data Sing (z :: NonEmpty a) where

• (:%|) :: Sing (n :| n)

data Sing (z :: Either a b)

data Sing (z :: Either a b) where

• SLeft :: Sing (Left n :: Either a b)
• SRight :: Sing (Right n :: Either a b)

data Sing (z :: (a, b))

data Sing (z :: (a, b)) where

• STuple2 :: Sing ((,) n n)

data Sing (f :: k1 ~> k2)

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

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

}

data Sing (z :: (a, b, c))

data Sing (z :: (a, b, c)) where

• STuple3 :: Sing ((,,) n n n)

data Sing (z :: (a, b, c, d))

data Sing (z :: (a, b, c, d)) where

• STuple4 :: Sing ((,,,) n n n n)

data Sing (z :: (a, b, c, d, e))

data Sing (z :: (a, b, c, d, e)) where

• STuple5 :: Sing ((,,,,) n n n n n)

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

data Sing (z :: (a, b, c, d, e, f)) where

• STuple6 :: Sing ((,,,,,) n n n n n n)

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

data Sing (z :: (a, b, c, d, e, f, g)) where

• STuple7 :: Sing ((,,,,,,) n n n n n n n)

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_ :: (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 _ (Left x) = Apply f x

Either_ _ g (Right y) = Apply g y

sEither_ :: forall (t :: TyFun a c -> Type) (t :: TyFun b c -> Type) (t :: Either a b). 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 _) xs) = Apply LeftsSym0 xs

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

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

Equations

Rights '[] = '[]

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

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

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

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

Equations

PartitionEithers a_6989586621679913642 = Apply (Apply (Apply FoldrSym0 (Apply (Apply Either_Sym0 (Let6989586621679913649LeftSym1 a_6989586621679913642)) (Let6989586621679913649RightSym1 a_6989586621679913642))) (Apply (Apply Tuple2Sym0 '[]) '[])) a_6989586621679913642

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

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

Equations

IsLeft (Left _) = TrueSym0

IsLeft (Right _) = FalseSym0

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

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

Equations

IsRight (Left _) = FalseSym0

IsRight (Right _) = TrueSym0

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

Defunctionalization symbols

data LeftSym0 (l :: TyFun a6989586621679082339 (Either a6989586621679082339 b6989586621679082340))

Instances

SuppressUnusedWarnings (LeftSym0 :: TyFun a6989586621679082339 (Either a6989586621679082339 b6989586621679082340) -> *)

Methods

suppressUnusedWarnings :: ()

type Apply (LeftSym0 :: TyFun a (Either a b6989586621679082340) -> *) (l :: a)

type Apply (LeftSym0 :: TyFun a (Either a b6989586621679082340) -> *) (l :: a) = (Left l :: Either a b6989586621679082340)

type LeftSym1 (t :: a6989586621679082339) = Left t

data RightSym0 (l :: TyFun b6989586621679082340 (Either a6989586621679082339 b6989586621679082340))

Instances

SuppressUnusedWarnings (RightSym0 :: TyFun b6989586621679082340 (Either a6989586621679082339 b6989586621679082340) -> *)

Methods

suppressUnusedWarnings :: ()

type Apply (RightSym0 :: TyFun b (Either a6989586621679082339 b) -> *) (l :: b)

type Apply (RightSym0 :: TyFun b (Either a6989586621679082339 b) -> *) (l :: b) = (Right l :: Either a6989586621679082339 b)

type RightSym1 (t :: b6989586621679082340) = Right t

data Either_Sym0 (l :: TyFun (TyFun a6989586621679912139 c6989586621679912140 -> Type) (TyFun (TyFun b6989586621679912141 c6989586621679912140 -> Type) (TyFun (Either a6989586621679912139 b6989586621679912141) c6989586621679912140 -> Type) -> Type))

Instances

SuppressUnusedWarnings (Either_Sym0 :: TyFun (TyFun a6989586621679912139 c6989586621679912140 -> Type) (TyFun (TyFun b6989586621679912141 c6989586621679912140 -> Type) (TyFun (Either a6989586621679912139 b6989586621679912141) c6989586621679912140 -> Type) -> Type) -> *)

Methods

suppressUnusedWarnings :: ()

type Apply (Either_Sym0 :: TyFun (TyFun a6989586621679912139 c6989586621679912140 -> Type) (TyFun (TyFun b6989586621679912141 c6989586621679912140 -> Type) (TyFun (Either a6989586621679912139 b6989586621679912141) c6989586621679912140 -> Type) -> Type) -> *) (l :: TyFun a6989586621679912139 c6989586621679912140 -> Type)

type Apply (Either_Sym0 :: TyFun (TyFun a6989586621679912139 c6989586621679912140 -> Type) (TyFun (TyFun b6989586621679912141 c6989586621679912140 -> Type) (TyFun (Either a6989586621679912139 b6989586621679912141) c6989586621679912140 -> Type) -> Type) -> *) (l :: TyFun a6989586621679912139 c6989586621679912140 -> Type) = (Either_Sym1 l :: TyFun (TyFun b6989586621679912141 c6989586621679912140 -> Type) (TyFun (Either a6989586621679912139 b6989586621679912141) c6989586621679912140 -> Type) -> *)

data Either_Sym1 (l :: TyFun a6989586621679912139 c6989586621679912140 -> Type) (l :: TyFun (TyFun b6989586621679912141 c6989586621679912140 -> Type) (TyFun (Either a6989586621679912139 b6989586621679912141) c6989586621679912140 -> Type))

Instances

SuppressUnusedWarnings (Either_Sym1 :: (TyFun a6989586621679912139 c6989586621679912140 -> Type) -> TyFun (TyFun b6989586621679912141 c6989586621679912140 -> Type) (TyFun (Either a6989586621679912139 b6989586621679912141) c6989586621679912140 -> Type) -> *)

Methods

suppressUnusedWarnings :: ()

type Apply (Either_Sym1 l1 :: TyFun (TyFun b6989586621679912141 c6989586621679912140 -> Type) (TyFun (Either a6989586621679912139 b6989586621679912141) c6989586621679912140 -> Type) -> *) (l2 :: TyFun b6989586621679912141 c6989586621679912140 -> Type)

type Apply (Either_Sym1 l1 :: TyFun (TyFun b6989586621679912141 c6989586621679912140 -> Type) (TyFun (Either a6989586621679912139 b6989586621679912141) c6989586621679912140 -> Type) -> *) (l2 :: TyFun b6989586621679912141 c6989586621679912140 -> Type) = Either_Sym2 l1 l2

data Either_Sym2 (l :: TyFun a6989586621679912139 c6989586621679912140 -> Type) (l :: TyFun b6989586621679912141 c6989586621679912140 -> Type) (l :: TyFun (Either a6989586621679912139 b6989586621679912141) c6989586621679912140)

Instances

SuppressUnusedWarnings (Either_Sym2 :: (TyFun a6989586621679912139 c6989586621679912140 -> Type) -> (TyFun b6989586621679912141 c6989586621679912140 -> Type) -> TyFun (Either a6989586621679912139 b6989586621679912141) c6989586621679912140 -> *)

Methods

suppressUnusedWarnings :: ()

type Apply (Either_Sym2 l1 l2 :: TyFun (Either a b) c -> *) (l3 :: Either a b)

type Apply (Either_Sym2 l1 l2 :: TyFun (Either a b) c -> *) (l3 :: Either a b) = Either_ l1 l2 l3

type Either_Sym3 (t :: TyFun a6989586621679912139 c6989586621679912140 -> Type) (t :: TyFun b6989586621679912141 c6989586621679912140 -> Type) (t :: Either a6989586621679912139 b6989586621679912141) = Either_ t t t

data LeftsSym0 (l :: TyFun [Either a6989586621679913275 b6989586621679913276] [a6989586621679913275])

Instances

SuppressUnusedWarnings (LeftsSym0 :: TyFun [Either a6989586621679913275 b6989586621679913276] [a6989586621679913275] -> *)

Methods

suppressUnusedWarnings :: ()

type Apply (LeftsSym0 :: TyFun [Either a b] [a] -> *) (l :: [Either a b])

type Apply (LeftsSym0 :: TyFun [Either a b] [a] -> *) (l :: [Either a b]) = Lefts l

type LeftsSym1 (t :: [Either a6989586621679913275 b6989586621679913276]) = Lefts t

data RightsSym0 (l :: TyFun [Either a6989586621679913273 b6989586621679913274] [b6989586621679913274])

Instances

SuppressUnusedWarnings (RightsSym0 :: TyFun [Either a6989586621679913273 b6989586621679913274] [b6989586621679913274] -> *)

Methods

suppressUnusedWarnings :: ()

type Apply (RightsSym0 :: TyFun [Either a b] [b] -> *) (l :: [Either a b])

type Apply (RightsSym0 :: TyFun [Either a b] [b] -> *) (l :: [Either a b]) = Rights l

type RightsSym1 (t :: [Either a6989586621679913273 b6989586621679913274]) = Rights t

data IsLeftSym0 (l :: TyFun (Either a6989586621679913269 b6989586621679913270) Bool)

Instances

SuppressUnusedWarnings (IsLeftSym0 :: TyFun (Either a6989586621679913269 b6989586621679913270) Bool -> *)

Methods

suppressUnusedWarnings :: ()

type Apply (IsLeftSym0 :: TyFun (Either a b) Bool -> *) (l :: Either a b)

type Apply (IsLeftSym0 :: TyFun (Either a b) Bool -> *) (l :: Either a b) = IsLeft l

type IsLeftSym1 (t :: Either a6989586621679913269 b6989586621679913270) = IsLeft t

data IsRightSym0 (l :: TyFun (Either a6989586621679913267 b6989586621679913268) Bool)

Instances

SuppressUnusedWarnings (IsRightSym0 :: TyFun (Either a6989586621679913267 b6989586621679913268) Bool -> *)

Methods

suppressUnusedWarnings :: ()

type Apply (IsRightSym0 :: TyFun (Either a b) Bool -> *) (l :: Either a b)

type Apply (IsRightSym0 :: TyFun (Either a b) Bool -> *) (l :: Either a b) = IsRight l

type IsRightSym1 (t :: Either a6989586621679913267 b6989586621679913268) = IsRight t