Data.Singletons.Prelude.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 :: k)

The singleton kind-indexed data family.

Instances

data Sing Bool

data Sing Bool where

• SFalse :: Sing Bool z
• STrue :: Sing Bool z

data Sing Ordering

data Sing Ordering where

• SLT :: Sing Ordering z
• SEQ :: Sing Ordering z
• SGT :: Sing Ordering z

data Sing *

data Sing * where

• STypeRep :: Sing * a

data Sing Nat

data Sing Nat where

• SNat :: Sing Nat n

data Sing Symbol

data Sing Symbol where

• SSym :: Sing Symbol n

data Sing ()

data Sing () where

• STuple0 :: Sing () z

data Sing [a0]

data Sing [a0] where

• SNil :: Sing [a] z
• SCons :: Sing [a] z

data Sing (Maybe a0)

data Sing (Maybe a0) where

• SNothing :: Sing (Maybe a) z
• SJust :: Sing (Maybe a) z

data Sing (NonEmpty a0)

data Sing (NonEmpty a0) where

• (:%|) :: Sing (NonEmpty a) z

data Sing (Either a0 b0)

data Sing (Either a0 b0) where

• SLeft :: Sing (Either a b) z
• SRight :: Sing (Either a b) z

data Sing (a0, b0)

data Sing (a0, b0) where

• STuple2 :: Sing (a, b) z

data Sing ((~>) k1 k2)

data Sing ((~>) k1 k2) = SLambda {

• applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k1 k2 f t)

}

data Sing (a0, b0, c0)

data Sing (a0, b0, c0) where

• STuple3 :: Sing (a, b, c) z

data Sing (a0, b0, c0, d0)

data Sing (a0, b0, c0, d0) where

• STuple4 :: Sing (a, b, c, d) z

data Sing (a0, b0, c0, d0, e0)

data Sing (a0, b0, c0, d0, e0) where

• STuple5 :: Sing (a, b, c, d, e) z

data Sing (a0, b0, c0, d0, e0, f0)

data Sing (a0, b0, c0, d0, e0, f0) where

• STuple6 :: Sing (a, b, c, d, e, f) z

data Sing (a0, b0, c0, d0, e0, f0, g0)

data Sing (a0, b0, c0, d0, e0, f0, g0) where

• STuple7 :: Sing (a, b, c, d, e, f, g) z

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 -> Type)

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

type family Maybe_ (a :: b) (a :: TyFun a b -> Type) (a :: Maybe a) :: b where ...

Equations

Maybe_ n _z_1627847793 Nothing = n

Maybe_ _z_1627847796 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)

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 :: Maybe a) :: Bool where ...

Equations

IsJust Nothing = FalseSym0

IsJust (Just _z_1627849157) = TrueSym0

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

type family IsNothing (a :: Maybe a) :: Bool where ...

Equations

IsNothing Nothing = TrueSym0

IsNothing (Just _z_1627849150) = FalseSym0

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

type family FromJust (a :: Maybe a) :: a where ...

Equations

FromJust Nothing = Apply ErrorSym0 "Maybe.fromJust: Nothing"

FromJust (Just x) = x

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

type family FromMaybe (a :: a) (a :: Maybe a) :: a where ...

Equations

FromMaybe d x = Case_1627849137 d x x

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

type family ListToMaybe (a :: [a]) :: Maybe a where ...

Equations

ListToMaybe '[] = NothingSym0

ListToMaybe ((:) a _z_1627849118) = Apply JustSym0 a

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

type family MaybeToList (a :: Maybe a) :: [a] where ...

Equations

MaybeToList Nothing = '[]

MaybeToList (Just x) = Apply (Apply (:$) x) '[]

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

type family CatMaybes (a :: [Maybe a]) :: [a] where ...

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])

type family MapMaybe (a :: TyFun a (Maybe b) -> Type) (a :: [a]) :: [b] where ...

Equations

MapMaybe _z_1627849070 '[] = '[]

MapMaybe f ((:) x xs) = Case_1627849102 f x xs (Let1627849089Scrutinee_1627849059Sym3 f x xs)

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

Defunctionalization symbols

type NothingSym0 = Nothing

data JustSym0 l

Instances

SuppressUnusedWarnings (TyFun a822083586 (Maybe a822083586) -> *) (JustSym0 a822083586)

Methods

suppressUnusedWarnings :: Proxy (JustSym0 a822083586) t -> ()

type Apply a822083586 (Maybe a822083586) (JustSym0 a822083586) l0

type Apply a822083586 (Maybe a822083586) (JustSym0 a822083586) l0 = JustSym1 a822083586 l0

type JustSym1 t = Just t

data Maybe_Sym0 l

Instances

SuppressUnusedWarnings (TyFun b1627847771 (TyFun (TyFun a1627847772 b1627847771 -> Type) (TyFun (Maybe a1627847772) b1627847771 -> Type) -> Type) -> *) (Maybe_Sym0 a1627847772 b1627847771)

Methods

suppressUnusedWarnings :: Proxy (Maybe_Sym0 a1627847772 b1627847771) t -> ()

type Apply b1627847771 (TyFun (TyFun a1627847772 b1627847771 -> Type) (TyFun (Maybe a1627847772) b1627847771 -> Type) -> Type) (Maybe_Sym0 a1627847772 b1627847771) l0

type Apply b1627847771 (TyFun (TyFun a1627847772 b1627847771 -> Type) (TyFun (Maybe a1627847772) b1627847771 -> Type) -> Type) (Maybe_Sym0 a1627847772 b1627847771) l0 = Maybe_Sym1 a1627847772 b1627847771 l0

data Maybe_Sym1 l l

Instances

SuppressUnusedWarnings (b1627847771 -> TyFun (TyFun a1627847772 b1627847771 -> Type) (TyFun (Maybe a1627847772) b1627847771 -> Type) -> *) (Maybe_Sym1 a1627847772 b1627847771)

Methods

suppressUnusedWarnings :: Proxy (Maybe_Sym1 a1627847772 b1627847771) t -> ()

type Apply (TyFun a1627847772 b1627847771 -> Type) (TyFun (Maybe a1627847772) b1627847771 -> Type) (Maybe_Sym1 a1627847772 b1627847771 l1) l0

type Apply (TyFun a1627847772 b1627847771 -> Type) (TyFun (Maybe a1627847772) b1627847771 -> Type) (Maybe_Sym1 a1627847772 b1627847771 l1) l0 = Maybe_Sym2 a1627847772 b1627847771 l1 l0

data Maybe_Sym2 l l l

Instances

SuppressUnusedWarnings (b1627847771 -> (TyFun a1627847772 b1627847771 -> Type) -> TyFun (Maybe a1627847772) b1627847771 -> *) (Maybe_Sym2 a1627847772 b1627847771)

Methods

suppressUnusedWarnings :: Proxy (Maybe_Sym2 a1627847772 b1627847771) t -> ()

type Apply (Maybe a1627847772) b1627847771 (Maybe_Sym2 a1627847772 b1627847771 l1 l2) l0

type Apply (Maybe a1627847772) b1627847771 (Maybe_Sym2 a1627847772 b1627847771 l1 l2) l0 = Maybe_Sym3 b1627847771 a1627847772 l1 l2 l0

type Maybe_Sym3 t t t = Maybe_ t t t

data IsJustSym0 l

Instances

SuppressUnusedWarnings (TyFun (Maybe a1627849036) Bool -> *) (IsJustSym0 a1627849036)

Methods

suppressUnusedWarnings :: Proxy (IsJustSym0 a1627849036) t -> ()

type Apply (Maybe a1627849036) Bool (IsJustSym0 a1627849036) l0

type Apply (Maybe a1627849036) Bool (IsJustSym0 a1627849036) l0 = IsJustSym1 a1627849036 l0

type IsJustSym1 t = IsJust t

data IsNothingSym0 l

Instances

SuppressUnusedWarnings (TyFun (Maybe a1627849035) Bool -> *) (IsNothingSym0 a1627849035)

Methods

suppressUnusedWarnings :: Proxy (IsNothingSym0 a1627849035) t -> ()

type Apply (Maybe a1627849035) Bool (IsNothingSym0 a1627849035) l0

type Apply (Maybe a1627849035) Bool (IsNothingSym0 a1627849035) l0 = IsNothingSym1 a1627849035 l0

type IsNothingSym1 t = IsNothing t

data FromJustSym0 l

Instances

SuppressUnusedWarnings (TyFun (Maybe a1627849034) a1627849034 -> *) (FromJustSym0 a1627849034)

Methods

suppressUnusedWarnings :: Proxy (FromJustSym0 a1627849034) t -> ()

type Apply (Maybe a1627849034) a1627849034 (FromJustSym0 a1627849034) l0

type Apply (Maybe a1627849034) a1627849034 (FromJustSym0 a1627849034) l0 = FromJustSym1 a1627849034 l0

type FromJustSym1 t = FromJust t

data FromMaybeSym0 l

Instances

SuppressUnusedWarnings (TyFun a1627849033 (TyFun (Maybe a1627849033) a1627849033 -> Type) -> *) (FromMaybeSym0 a1627849033)

Methods

suppressUnusedWarnings :: Proxy (FromMaybeSym0 a1627849033) t -> ()

type Apply a1627849033 (TyFun (Maybe a1627849033) a1627849033 -> Type) (FromMaybeSym0 a1627849033) l0

type Apply a1627849033 (TyFun (Maybe a1627849033) a1627849033 -> Type) (FromMaybeSym0 a1627849033) l0 = FromMaybeSym1 a1627849033 l0

data FromMaybeSym1 l l

Instances

SuppressUnusedWarnings (a1627849033 -> TyFun (Maybe a1627849033) a1627849033 -> *) (FromMaybeSym1 a1627849033)

Methods

suppressUnusedWarnings :: Proxy (FromMaybeSym1 a1627849033) t -> ()

type Apply (Maybe a1627849033) a1627849033 (FromMaybeSym1 a1627849033 l1) l0

type Apply (Maybe a1627849033) a1627849033 (FromMaybeSym1 a1627849033 l1) l0 = FromMaybeSym2 a1627849033 l1 l0

type FromMaybeSym2 t t = FromMaybe t t

data ListToMaybeSym0 l

Instances

SuppressUnusedWarnings (TyFun [a1627849031] (Maybe a1627849031) -> *) (ListToMaybeSym0 a1627849031)

Methods

suppressUnusedWarnings :: Proxy (ListToMaybeSym0 a1627849031) t -> ()

type Apply [a1627849031] (Maybe a1627849031) (ListToMaybeSym0 a1627849031) l0

type Apply [a1627849031] (Maybe a1627849031) (ListToMaybeSym0 a1627849031) l0 = ListToMaybeSym1 a1627849031 l0

type ListToMaybeSym1 t = ListToMaybe t

data MaybeToListSym0 l

Instances

SuppressUnusedWarnings (TyFun (Maybe a1627849032) [a1627849032] -> *) (MaybeToListSym0 a1627849032)

Methods

suppressUnusedWarnings :: Proxy (MaybeToListSym0 a1627849032) t -> ()

type Apply (Maybe a1627849032) [a1627849032] (MaybeToListSym0 a1627849032) l0

type Apply (Maybe a1627849032) [a1627849032] (MaybeToListSym0 a1627849032) l0 = MaybeToListSym1 a1627849032 l0

type MaybeToListSym1 t = MaybeToList t

data CatMaybesSym0 l

Instances

SuppressUnusedWarnings (TyFun [Maybe a1627849030] [a1627849030] -> *) (CatMaybesSym0 a1627849030)

Methods

suppressUnusedWarnings :: Proxy (CatMaybesSym0 a1627849030) t -> ()

type Apply [Maybe a1627849030] [a1627849030] (CatMaybesSym0 a1627849030) l0

type Apply [Maybe a1627849030] [a1627849030] (CatMaybesSym0 a1627849030) l0 = CatMaybesSym1 a1627849030 l0

type CatMaybesSym1 t = CatMaybes t

data MapMaybeSym0 l

Instances

SuppressUnusedWarnings (TyFun (TyFun a1627849028 (Maybe b1627849029) -> Type) (TyFun [a1627849028] [b1627849029] -> Type) -> *) (MapMaybeSym0 a1627849028 b1627849029)

Methods

suppressUnusedWarnings :: Proxy (MapMaybeSym0 a1627849028 b1627849029) t -> ()

type Apply (TyFun a1627849028 (Maybe b1627849029) -> Type) (TyFun [a1627849028] [b1627849029] -> Type) (MapMaybeSym0 a1627849028 b1627849029) l0

type Apply (TyFun a1627849028 (Maybe b1627849029) -> Type) (TyFun [a1627849028] [b1627849029] -> Type) (MapMaybeSym0 a1627849028 b1627849029) l0 = MapMaybeSym1 a1627849028 b1627849029 l0

data MapMaybeSym1 l l

Instances

SuppressUnusedWarnings ((TyFun a1627849028 (Maybe b1627849029) -> Type) -> TyFun [a1627849028] [b1627849029] -> *) (MapMaybeSym1 a1627849028 b1627849029)

Methods

suppressUnusedWarnings :: Proxy (MapMaybeSym1 a1627849028 b1627849029) t -> ()

type Apply [a1627849028] [b1627849029] (MapMaybeSym1 a1627849028 b1627849029 l1) l0

type Apply [a1627849028] [b1627849029] (MapMaybeSym1 a1627849028 b1627849029 l1) l0 = MapMaybeSym2 a1627849028 b1627849029 l1 l0

type MapMaybeSym2 t t = MapMaybe t t