| Copyright | (C) 2013-2014 Richard Eisenberg Jan Stolarek |
|---|---|
| License | BSD-style (see LICENSE) |
| Maintainer | Richard Eisenberg (rae@cs.brynmawr.edu) |
| 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
- data family Sing (a :: k)
- type SEither = (Sing :: Either a b -> Type)
- 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 ...
- 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)
- type family Lefts (a :: [Either a b]) :: [a] where ...
- sLefts :: forall (t :: [Either a b]). Sing t -> Sing (Apply LeftsSym0 t :: [a])
- type family Rights (a :: [Either a b]) :: [b] where ...
- sRights :: forall (t :: [Either a b]). Sing t -> Sing (Apply RightsSym0 t :: [b])
- type family PartitionEithers (a :: [Either a b]) :: ([a], [b]) where ...
- sPartitionEithers :: forall (t :: [Either a b]). Sing t -> Sing (Apply PartitionEithersSym0 t :: ([a], [b]))
- type family IsLeft (a :: Either a b) :: Bool where ...
- sIsLeft :: forall (t :: Either a b). Sing t -> Sing (Apply IsLeftSym0 t :: Bool)
- type family IsRight (a :: Either a b) :: Bool where ...
- sIsRight :: forall (t :: Either a b). Sing t -> Sing (Apply IsRightSym0 t :: Bool)
- data LeftSym0 (l :: TyFun a6989586621679083190 (Either a6989586621679083190 b6989586621679083191))
- type LeftSym1 (t :: a6989586621679083190) = Left t
- data RightSym0 (l :: TyFun b6989586621679083191 (Either a6989586621679083190 b6989586621679083191))
- type RightSym1 (t :: b6989586621679083191) = Right t
- data Either_Sym0 (l :: TyFun (TyFun a6989586621679940661 c6989586621679940662 -> Type) (TyFun (TyFun b6989586621679940663 c6989586621679940662 -> Type) (TyFun (Either a6989586621679940661 b6989586621679940663) c6989586621679940662 -> Type) -> Type))
- data Either_Sym1 (l :: TyFun a6989586621679940661 c6989586621679940662 -> Type) (l :: TyFun (TyFun b6989586621679940663 c6989586621679940662 -> Type) (TyFun (Either a6989586621679940661 b6989586621679940663) c6989586621679940662 -> Type))
- data Either_Sym2 (l :: TyFun a6989586621679940661 c6989586621679940662 -> Type) (l :: TyFun b6989586621679940663 c6989586621679940662 -> Type) (l :: TyFun (Either a6989586621679940661 b6989586621679940663) c6989586621679940662)
- type Either_Sym3 (t :: TyFun a6989586621679940661 c6989586621679940662 -> Type) (t :: TyFun b6989586621679940663 c6989586621679940662 -> Type) (t :: Either a6989586621679940661 b6989586621679940663) = Either_ t t t
- data LeftsSym0 (l :: TyFun [Either a6989586621679941797 b6989586621679941798] [a6989586621679941797])
- type LeftsSym1 (t :: [Either a6989586621679941797 b6989586621679941798]) = Lefts t
- data RightsSym0 (l :: TyFun [Either a6989586621679941795 b6989586621679941796] [b6989586621679941796])
- type RightsSym1 (t :: [Either a6989586621679941795 b6989586621679941796]) = Rights t
- data IsLeftSym0 (l :: TyFun (Either a6989586621679941791 b6989586621679941792) Bool)
- type IsLeftSym1 (t :: Either a6989586621679941791 b6989586621679941792) = IsLeft t
- data IsRightSym0 (l :: TyFun (Either a6989586621679941789 b6989586621679941790) Bool)
- type IsRightSym1 (t :: Either a6989586621679941789 b6989586621679941790) = IsRight t
The Either singleton
The singleton kind-indexed data family.
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
type family Either_ (a :: TyFun a c -> Type) (a :: TyFun b c -> Type) (a :: Either a b) :: c where ... #
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 PartitionEithers (a :: [Either a b]) :: ([a], [b]) where ... #
Equations
| PartitionEithers a_6989586621679942164 = Apply (Apply (Apply FoldrSym0 (Apply (Apply Either_Sym0 (Let6989586621679942171LeftSym1 a_6989586621679942164)) (Let6989586621679942171RightSym1 a_6989586621679942164))) (Apply (Apply Tuple2Sym0 '[]) '[])) a_6989586621679942164 |
sPartitionEithers :: forall (t :: [Either a b]). Sing t -> Sing (Apply PartitionEithersSym0 t :: ([a], [b])) #
Defunctionalization symbols
data LeftSym0 (l :: TyFun a6989586621679083190 (Either a6989586621679083190 b6989586621679083191)) #
Instances
| SuppressUnusedWarnings (LeftSym0 :: TyFun a6989586621679083190 (Either a6989586621679083190 b6989586621679083191) -> *) # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () # | |
| type Apply (LeftSym0 :: TyFun a (Either a b6989586621679083191) -> *) (l :: a) # | |
data RightSym0 (l :: TyFun b6989586621679083191 (Either a6989586621679083190 b6989586621679083191)) #
Instances
| SuppressUnusedWarnings (RightSym0 :: TyFun b6989586621679083191 (Either a6989586621679083190 b6989586621679083191) -> *) # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () # | |
| type Apply (RightSym0 :: TyFun b (Either a6989586621679083190 b) -> *) (l :: b) # | |
data Either_Sym0 (l :: TyFun (TyFun a6989586621679940661 c6989586621679940662 -> Type) (TyFun (TyFun b6989586621679940663 c6989586621679940662 -> Type) (TyFun (Either a6989586621679940661 b6989586621679940663) c6989586621679940662 -> Type) -> Type)) #
Instances
| SuppressUnusedWarnings (Either_Sym0 :: TyFun (TyFun a6989586621679940661 c6989586621679940662 -> Type) (TyFun (TyFun b6989586621679940663 c6989586621679940662 -> Type) (TyFun (Either a6989586621679940661 b6989586621679940663) c6989586621679940662 -> Type) -> Type) -> *) # | |
Defined in Data.Singletons.Prelude.Either Methods suppressUnusedWarnings :: () # | |
| type Apply (Either_Sym0 :: TyFun (TyFun a6989586621679940661 c6989586621679940662 -> Type) (TyFun (TyFun b6989586621679940663 c6989586621679940662 -> Type) (TyFun (Either a6989586621679940661 b6989586621679940663) c6989586621679940662 -> Type) -> Type) -> *) (l :: TyFun a6989586621679940661 c6989586621679940662 -> Type) # | |
Defined in Data.Singletons.Prelude.Either type Apply (Either_Sym0 :: TyFun (TyFun a6989586621679940661 c6989586621679940662 -> Type) (TyFun (TyFun b6989586621679940663 c6989586621679940662 -> Type) (TyFun (Either a6989586621679940661 b6989586621679940663) c6989586621679940662 -> Type) -> Type) -> *) (l :: TyFun a6989586621679940661 c6989586621679940662 -> Type) = (Either_Sym1 l :: TyFun (TyFun b6989586621679940663 c6989586621679940662 -> Type) (TyFun (Either a6989586621679940661 b6989586621679940663) c6989586621679940662 -> Type) -> *) | |
data Either_Sym1 (l :: TyFun a6989586621679940661 c6989586621679940662 -> Type) (l :: TyFun (TyFun b6989586621679940663 c6989586621679940662 -> Type) (TyFun (Either a6989586621679940661 b6989586621679940663) c6989586621679940662 -> Type)) #
Instances
| SuppressUnusedWarnings (Either_Sym1 :: (TyFun a6989586621679940661 c6989586621679940662 -> Type) -> TyFun (TyFun b6989586621679940663 c6989586621679940662 -> Type) (TyFun (Either a6989586621679940661 b6989586621679940663) c6989586621679940662 -> Type) -> *) # | |
Defined in Data.Singletons.Prelude.Either Methods suppressUnusedWarnings :: () # | |
| type Apply (Either_Sym1 l1 :: TyFun (TyFun b6989586621679940663 c6989586621679940662 -> Type) (TyFun (Either a6989586621679940661 b6989586621679940663) c6989586621679940662 -> Type) -> *) (l2 :: TyFun b6989586621679940663 c6989586621679940662 -> Type) # | |
Defined in Data.Singletons.Prelude.Either | |
data Either_Sym2 (l :: TyFun a6989586621679940661 c6989586621679940662 -> Type) (l :: TyFun b6989586621679940663 c6989586621679940662 -> Type) (l :: TyFun (Either a6989586621679940661 b6989586621679940663) c6989586621679940662) #
Instances
| SuppressUnusedWarnings (Either_Sym2 :: (TyFun a6989586621679940661 c6989586621679940662 -> Type) -> (TyFun b6989586621679940663 c6989586621679940662 -> Type) -> TyFun (Either a6989586621679940661 b6989586621679940663) c6989586621679940662 -> *) # | |
Defined in Data.Singletons.Prelude.Either Methods suppressUnusedWarnings :: () # | |
| type Apply (Either_Sym2 l1 l2 :: TyFun (Either a b) c -> *) (l3 :: Either a b) # | |
Defined in Data.Singletons.Prelude.Either | |
type Either_Sym3 (t :: TyFun a6989586621679940661 c6989586621679940662 -> Type) (t :: TyFun b6989586621679940663 c6989586621679940662 -> Type) (t :: Either a6989586621679940661 b6989586621679940663) = Either_ t t t #
data LeftsSym0 (l :: TyFun [Either a6989586621679941797 b6989586621679941798] [a6989586621679941797]) #
data RightsSym0 (l :: TyFun [Either a6989586621679941795 b6989586621679941796] [b6989586621679941796]) #
Instances
| SuppressUnusedWarnings (RightsSym0 :: TyFun [Either a6989586621679941795 b6989586621679941796] [b6989586621679941796] -> *) # | |
Defined in Data.Singletons.Prelude.Either Methods suppressUnusedWarnings :: () # | |
| type Apply (RightsSym0 :: TyFun [Either a b] [b] -> *) (l :: [Either a b]) # | |
Defined in Data.Singletons.Prelude.Either | |
type RightsSym1 (t :: [Either a6989586621679941795 b6989586621679941796]) = Rights t #
data IsLeftSym0 (l :: TyFun (Either a6989586621679941791 b6989586621679941792) Bool) #
Instances
| SuppressUnusedWarnings (IsLeftSym0 :: TyFun (Either a6989586621679941791 b6989586621679941792) Bool -> *) # | |
Defined in Data.Singletons.Prelude.Either Methods suppressUnusedWarnings :: () # | |
| type Apply (IsLeftSym0 :: TyFun (Either a b) Bool -> *) (l :: Either a b) # | |
Defined in Data.Singletons.Prelude.Either | |
type IsLeftSym1 (t :: Either a6989586621679941791 b6989586621679941792) = IsLeft t #
data IsRightSym0 (l :: TyFun (Either a6989586621679941789 b6989586621679941790) Bool) #
Instances
| SuppressUnusedWarnings (IsRightSym0 :: TyFun (Either a6989586621679941789 b6989586621679941790) Bool -> *) # | |
Defined in Data.Singletons.Prelude.Either Methods suppressUnusedWarnings :: () # | |
| type Apply (IsRightSym0 :: TyFun (Either a b) Bool -> *) (l :: Either a b) # | |
Defined in Data.Singletons.Prelude.Either | |
type IsRightSym1 (t :: Either a6989586621679941789 b6989586621679941790) = IsRight t #