Copyright | (C) 2013 Richard Eisenberg |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Richard Eisenberg (eir@cis.upenn.edu) |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
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
The singleton kind-indexed data family.
Instances
TestCoercion * (Sing *) | |
SDecide k (KProxy k) => TestEquality k (Sing k) | |
data Sing Bool where | |
data Sing Ordering where | |
data Sing * where | |
data Sing Nat = SNat Integer | |
data Sing Symbol = SSym String | |
data Sing () where | |
data Sing [a0] where | |
data Sing (Maybe a0) where | |
data Sing (Either a0 b0) where | |
data Sing ((,) a0 b0) where | |
data Sing ((,,) a0 b0 c0) where | |
data Sing ((,,,) a0 b0 c0 d0) where | |
data Sing ((,,,,) a0 b0 c0 d0 e0) where | |
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where | |
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where |
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
Equations
PartitionEithers es = PartitionEithers_aux `(`[]`, `[]`)` es |
sPartitionEithers :: forall t. Sing t -> Sing (PartitionEithers t) Source