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 |

Defines functions and datatypes relating to the singleton for `Maybe`

,
including a singletons version of all the definitions in `Data.Maybe`

.

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.Maybe`

. Also, please excuse
the apparent repeated variable names. This is due to an interaction
between Template Haskell and Haddock.

- data family Sing a
- type SMaybe z = Sing z
- type family Maybe_ a a a :: b
- sMaybe_ :: forall t t t. Sing t -> (forall t. Sing t -> Sing (t t)) -> Sing t -> Sing (Maybe_ t t t)
- type family IsJust a :: Bool
- sIsJust :: forall t. Sing t -> Sing (IsJust t)
- type family IsNothing a :: Bool
- sIsNothing :: forall t. Sing t -> Sing (IsNothing t)
- type family FromJust a :: a
- sFromJust :: forall t. Sing t -> Sing (FromJust t)
- type family FromMaybe a a :: a
- sFromMaybe :: forall t t. Sing t -> Sing t -> Sing (FromMaybe t t)
- type family MaybeToList a :: [a]
- sMaybeToList :: forall t. Sing t -> Sing (MaybeToList t)
- type family ListToMaybe a :: Maybe a
- sListToMaybe :: forall t. Sing t -> Sing (ListToMaybe t)
- type family CatMaybes a :: [a]
- sCatMaybes :: forall t. Sing t -> Sing (CatMaybes t)
- type family MapMaybe a a :: [b]
- sMapMaybe :: forall t t. (forall t. Sing t -> Sing (t t)) -> Sing t -> Sing (MapMaybe t t)

# Documentation

Though Haddock doesn't show it, the `Sing`

instance above declares
constructors

SNothing :: Sing Nothing SJust :: Sing a -> Sing (Just a)

# Singletons from `Data.Maybe`

sMaybe_ :: forall t t t. Sing t -> (forall t. Sing t -> Sing (t t)) -> Sing t -> Sing (Maybe_ t t t)Source

The preceding two definitions are derived from the function `maybe`

in
`Data.Maybe`

. The extra underscore is to avoid name clashes with the type
`Maybe`

.

sIsNothing :: forall t. Sing t -> Sing (IsNothing t)Source

type family MaybeToList a :: [a]Source

sMaybeToList :: forall t. Sing t -> Sing (MaybeToList t)Source

type family ListToMaybe a :: Maybe aSource

sListToMaybe :: forall t. Sing t -> Sing (ListToMaybe t)Source

sCatMaybes :: forall t. Sing t -> Sing (CatMaybes t)Source