Copyright	(C) 2013-2014 Richard Eisenberg, Jan Stolarek
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (eir@cis.upenn.edu)
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.Prelude.Maybe

Contents

Singletons from Data.Maybe
Defunctionalization symbols

Description

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.

Synopsis

Documentation

data family Sing a Source

The singleton kind-indexed data family.

Instances

data Sing Bool where SFalse :: (~) Bool z False => Sing Bool z STrue :: (~) Bool z True => Sing Bool z Source
data Sing Ordering where SLT :: (~) Ordering z LT => Sing Ordering z SEQ :: (~) Ordering z EQ => Sing Ordering z SGT :: (~) Ordering z GT => Sing Ordering z Source
data Sing * where STypeRep :: Typeable * a => Sing * a Source
data Sing Nat where SNat :: KnownNat n => Sing Nat n Source
data Sing Symbol where SSym :: KnownSymbol n => Sing Symbol n Source
data Sing () where STuple0 :: (~) () z () => Sing () z Source
data Sing [a0] where SNil :: (~) [a] z ([] a) => Sing [a] z SCons :: (~) [a] z ((:) a n n) => Sing a n -> Sing [a] n -> Sing [a] z Source
data Sing (Maybe a0) where SNothing :: (~) (Maybe a) z (Nothing a) => Sing (Maybe a) z SJust :: (~) (Maybe a) z (Just a n) => Sing a n -> Sing (Maybe a) z Source
data Sing (TyFun k1 k2 -> *) = SLambda { applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k2 k1 f t) } Source
data Sing (Either a0 b0) where SLeft :: (~) (Either a b) z (Left a b n) => Sing a n -> Sing (Either a b) z SRight :: (~) (Either a b) z (Right a b n) => Sing b n -> Sing (Either a b) z Source
data Sing ((,) a0 b0) where STuple2 :: (~) ((,) a b) z ((,) a b n n) => Sing a n -> Sing b n -> Sing ((,) a b) z Source
data Sing ((,,) a0 b0 c0) where STuple3 :: (~) ((,,) a b c) z ((,,) a b c n n n) => Sing a n -> Sing b n -> Sing c n -> Sing ((,,) a b c) z Source
data Sing ((,,,) a0 b0 c0 d0) where STuple4 :: (~) ((,,,) a b c d) z ((,,,) a b c d n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing ((,,,) a b c d) z Source
data Sing ((,,,,) a0 b0 c0 d0 e0) where STuple5 :: (~) ((,,,,) a b c d e) z ((,,,,) a b c d e n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing ((,,,,) a b c d e) z Source
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where STuple6 :: (~) ((,,,,,) a b c d e f) z ((,,,,,) a b c d e f n n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing f n -> Sing ((,,,,,) a b c d e f) z Source
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where STuple7 :: (~) ((,,,,,,) a b c d e f g) z ((,,,,,,) a b c d e f g n n n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing f n -> Sing g n -> Sing ((,,,,,,) a b c d e f g) z Source

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

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

type SMaybe = (Sing :: Maybe a -> *) Source

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

Singletons from `Data.Maybe`

maybe_ :: forall b a. b -> (a -> b) -> Maybe a -> b Source

type family Maybe_ a a a :: b Source

Equations

Maybe_ n _z_1627814740 Nothing = n
Maybe_ _z_1627814743 f (Just x) = Apply f x

sMaybe_ :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Maybe_Sym0 t) t) t :: b) 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.

type family IsJust a :: Bool Source

Equations

IsJust Nothing = FalseSym0
IsJust (Just _z_1627816178) = TrueSym0

sIsJust :: forall t. Sing t -> Sing (Apply IsJustSym0 t :: Bool) Source

type family IsNothing a :: Bool Source

Equations

IsNothing Nothing = TrueSym0
IsNothing (Just _z_1627816171) = FalseSym0

sIsNothing :: forall t. Sing t -> Sing (Apply IsNothingSym0 t :: Bool) Source

type family FromJust a :: a Source

Equations

FromJust Nothing = Apply ErrorSym0 "Maybe.fromJust: Nothing"
FromJust (Just x) = x

sFromJust :: forall t. Sing t -> Sing (Apply FromJustSym0 t :: a) Source

type family FromMaybe a a :: a Source

Equations

FromMaybe d x = Case_1627816158 d x (Let1627816150Scrutinee_1627816070Sym2 d x)

sFromMaybe :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply FromMaybeSym0 t) t :: a) Source

type family ListToMaybe a :: Maybe a Source

Equations

ListToMaybe `[]` = NothingSym0
ListToMaybe ((:) a _z_1627816131) = Apply JustSym0 a

sListToMaybe :: forall t. Sing t -> Sing (Apply ListToMaybeSym0 t :: Maybe a) Source

type family MaybeToList a :: [a] Source

Equations

MaybeToList Nothing = `[]`
MaybeToList (Just x) = Apply (Apply (:$) x) `[]`

sMaybeToList :: forall t. Sing t -> Sing (Apply MaybeToListSym0 t :: [a]) Source

type family CatMaybes a :: [a] Source

Equations

CatMaybes `[]` = `[]`
CatMaybes ((:) (Just x) xs) = Apply (Apply (:$) x) (Apply CatMaybesSym0 xs)
CatMaybes ((:) Nothing xs) = Apply CatMaybesSym0 xs

sCatMaybes :: forall t. Sing t -> Sing (Apply CatMaybesSym0 t :: [a]) Source

type family MapMaybe a a :: [b] Source

Equations

MapMaybe _z_1627816083 `[]` = `[]`
MapMaybe f ((:) x xs) = Case_1627816115 f x xs (Let1627816102Scrutinee_1627816072Sym3 f x xs)

sMapMaybe :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply MapMaybeSym0 t) t :: [b]) Source

Defunctionalization symbols

type NothingSym0 = Nothing Source

data JustSym0 l Source

Instances

SuppressUnusedWarnings (TyFun k (Maybe k) -> *) (JustSym0 k) Source
type Apply (Maybe k) k (JustSym0 k) l0 = JustSym1 k l0 Source

type JustSym1 t = Just t Source

data Maybe_Sym0 l Source

Instances

SuppressUnusedWarnings (TyFun k (TyFun (TyFun k k -> ) (TyFun (Maybe k) k -> ) -> ) -> ) (Maybe_Sym0 k k) Source
type Apply (TyFun (TyFun k1 k -> ) (TyFun (Maybe k1) k -> ) -> *) k (Maybe_Sym0 k k1) l0 = Maybe_Sym1 k k1 l0 Source

data Maybe_Sym1 l l Source

Instances

SuppressUnusedWarnings (k -> TyFun (TyFun k k -> ) (TyFun (Maybe k) k -> ) -> *) (Maybe_Sym1 k k) Source
type Apply (TyFun (Maybe k) k1 -> ) (TyFun k k1 -> ) (Maybe_Sym1 k1 k l1) l0 = Maybe_Sym2 k1 k l1 l0 Source

data Maybe_Sym2 l l l Source

Instances

SuppressUnusedWarnings (k -> (TyFun k k -> ) -> TyFun (Maybe k) k -> ) (Maybe_Sym2 k k) Source
type Apply k (Maybe k1) (Maybe_Sym2 k k1 l1 l2) l0 = Maybe_Sym3 k k1 l1 l2 l0 Source

type Maybe_Sym3 t t t = Maybe_ t t t Source

data IsJustSym0 l Source

Instances

SuppressUnusedWarnings (TyFun (Maybe k) Bool -> *) (IsJustSym0 k) Source
type Apply Bool (Maybe k) (IsJustSym0 k) l0 = IsJustSym1 k l0 Source

type IsJustSym1 t = IsJust t Source

data IsNothingSym0 l Source

Instances

SuppressUnusedWarnings (TyFun (Maybe k) Bool -> *) (IsNothingSym0 k) Source
type Apply Bool (Maybe k) (IsNothingSym0 k) l0 = IsNothingSym1 k l0 Source

type IsNothingSym1 t = IsNothing t Source

data FromJustSym0 l Source

Instances

SuppressUnusedWarnings (TyFun (Maybe k) k -> *) (FromJustSym0 k) Source
type Apply k (Maybe k) (FromJustSym0 k) l0 = FromJustSym1 k l0 Source

type FromJustSym1 t = FromJust t Source

data FromMaybeSym0 l Source

Instances

SuppressUnusedWarnings (TyFun k (TyFun (Maybe k) k -> ) -> ) (FromMaybeSym0 k) Source
type Apply (TyFun (Maybe k) k -> *) k (FromMaybeSym0 k) l0 = FromMaybeSym1 k l0 Source

data FromMaybeSym1 l l Source

Instances

SuppressUnusedWarnings (k -> TyFun (Maybe k) k -> *) (FromMaybeSym1 k) Source
type Apply k (Maybe k) (FromMaybeSym1 k l1) l0 = FromMaybeSym2 k l1 l0 Source

type FromMaybeSym2 t t = FromMaybe t t Source

data ListToMaybeSym0 l Source

Instances

SuppressUnusedWarnings (TyFun [k] (Maybe k) -> *) (ListToMaybeSym0 k) Source
type Apply (Maybe k) [k] (ListToMaybeSym0 k) l0 = ListToMaybeSym1 k l0 Source

type ListToMaybeSym1 t = ListToMaybe t Source

data MaybeToListSym0 l Source

Instances

SuppressUnusedWarnings (TyFun (Maybe k) [k] -> *) (MaybeToListSym0 k) Source
type Apply [k] (Maybe k) (MaybeToListSym0 k) l0 = MaybeToListSym1 k l0 Source

type MaybeToListSym1 t = MaybeToList t Source

data CatMaybesSym0 l Source

Instances

SuppressUnusedWarnings (TyFun [Maybe k] [k] -> *) (CatMaybesSym0 k) Source
type Apply [k] [Maybe k] (CatMaybesSym0 k) l0 = CatMaybesSym1 k l0 Source

type CatMaybesSym1 t = CatMaybes t Source

data MapMaybeSym0 l Source

Instances

SuppressUnusedWarnings (TyFun (TyFun k (Maybe k) -> ) (TyFun [k] [k] -> ) -> *) (MapMaybeSym0 k k) Source
type Apply (TyFun [k] [k1] -> ) (TyFun k (Maybe k1) -> ) (MapMaybeSym0 k k1) l0 = MapMaybeSym1 k k1 l0 Source

data MapMaybeSym1 l l Source

Instances

SuppressUnusedWarnings ((TyFun k (Maybe k) -> ) -> TyFun [k] [k] -> ) (MapMaybeSym1 k k) Source
type Apply [k1] [k] (MapMaybeSym1 k k1 l1) l0 = MapMaybeSym2 k k1 l1 l0 Source

type MapMaybeSym2 t t = MapMaybe t t Source

Documentation

Singletons from Data.Maybe

Defunctionalization symbols

Singletons from `Data.Maybe`