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 |

- The
`Either`

singleton - Singletons from
`Data.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.

- 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