Data.Singletons.Maybe

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.

Documentation

data family Sing a

The singleton kind-indexed data family.

Though Haddock doesn't show it, the Sing instance above declares constructors

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

type SMaybe z = Sing z

SBool is a kind-restricted synonym for Sing: type SMaybe (a :: Maybe k) = Sing a

Singletons from Data.Maybe

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)

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.

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)