| Copyright | (C) 2013 Richard Eisenberg |
|---|---|
| License | (C) 2013 Richard Eisenberg |
| Maintainer | Richard Eisenberg (eir@cis.upenn.edu) |
| Stability | experimental |
| Portability | non-portable |
| Safe Haskell | None |
Data.Singletons.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.
- data family Sing a
- type SEither z = Sing z
- type family Either_ a a a :: c
- sEither_ :: forall t t t. (forall t. Sing t -> Sing (t t)) -> (forall t. Sing t -> Sing (t t)) -> Sing t -> Sing (Either_ t t t)
- type family Lefts a :: [a]
- sLefts :: forall t. Sing t -> Sing (Lefts t)
- type family Rights a :: [b]
- sRights :: forall t. Sing t -> Sing (Rights t)
- type family PartitionEithers a :: ([a], [b])
- sPartitionEithers :: forall t. Sing t -> Sing (PartitionEithers t)
- type family IsLeft a :: Bool
- sIsLeft :: forall t. Sing t -> Sing (IsLeft t)
- type family IsRight a :: Bool
- sIsRight :: forall t. Sing t -> Sing (IsRight t)
The Either singleton
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 t t t. (forall t. Sing t -> Sing (t t)) -> (forall t. Sing t -> Sing (t t)) -> Sing t -> Sing (Either_ t t t)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 :: ([a], [b])Source
sPartitionEithers :: forall t. Sing t -> Sing (PartitionEithers t)Source