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

The singleton kind-indexed data family.

Instances

TestCoercion * (Sing *)

SDecide k (KProxy k) => TestEquality k (Sing k)

data Sing Bool where

• SFalse :: (~) Bool z False => Sing Bool z
• STrue :: (~) Bool z True => Sing Bool z

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

data Sing * where

• STypeRep :: Typeable * a => Sing * a

data Sing Nat where

• SNat :: KnownNat n => Sing Nat n

data Sing Symbol where

• SSym :: KnownSymbol n => Sing Symbol n

data Sing () where

• STuple0 :: (~) () z () => Sing () z

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

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

data Sing (TyFun k1 k2 -> *) = SLambda {

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

}

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

data Sing ((,) a0 b0) where

• STuple2 :: (~) ((,) a b) z ((,) a b n n) => Sing a n -> Sing b n -> Sing ((,) a b) z

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

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

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

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

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

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

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

type family Maybe_ a a a :: b

Equations

Maybe_ n z Nothing = n

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

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

Equations

IsJust Nothing = FalseSym0

IsJust (Just z) = TrueSym0

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

type family IsNothing a :: Bool

Equations

IsNothing Nothing = TrueSym0

IsNothing (Just z) = FalseSym0

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

type family FromJust a :: a

Equations

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

FromJust (Just x) = x

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

type family FromMaybe a a :: a

Equations

FromMaybe d x = Case_1627755653 d x (Let1627755645Scrutinee_1627755568Sym2 d x)

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

type family ListToMaybe a :: Maybe a

Equations

ListToMaybe `[]` = NothingSym0

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

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

type family MaybeToList a :: [a]

Equations

MaybeToList Nothing = `[]`

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

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

type family CatMaybes a :: [a]

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)

type family MapMaybe a a :: [b]

Equations

MapMaybe z `[]` = `[]`

MapMaybe f ((:) x xs) = Case_1627755611 f x xs (Let1627755598Scrutinee_1627755570Sym3 f x xs)

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

Defunctionalization symbols

type NothingSym0 = Nothing

data JustSym0 l

Instances

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

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

type JustSym1 t = Just t

data Maybe_Sym0 l

Instances

SuppressUnusedWarnings (TyFun k (TyFun (TyFun k k -> *) (TyFun (Maybe k) k -> *) -> *) -> *) (Maybe_Sym0 k k)

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

data Maybe_Sym1 l l

Instances

SuppressUnusedWarnings (k -> TyFun (TyFun k k -> *) (TyFun (Maybe k) k -> *) -> *) (Maybe_Sym1 k k)

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

data Maybe_Sym2 l l l

Instances

SuppressUnusedWarnings (k -> (TyFun k k -> *) -> TyFun (Maybe k) k -> *) (Maybe_Sym2 k k)

type Apply k (Maybe k1) (Maybe_Sym2 k k1 l1 l2) l0 = Maybe_Sym3 k k1 l1 l2 l0

type Maybe_Sym3 t t t = Maybe_ t t t

data IsJustSym0 l

Instances

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

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

type IsJustSym1 t = IsJust t

data IsNothingSym0 l

Instances

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

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

type IsNothingSym1 t = IsNothing t

data FromJustSym0 l

Instances

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

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

type FromJustSym1 t = FromJust t

data FromMaybeSym0 l

Instances

SuppressUnusedWarnings (TyFun k (TyFun (Maybe k) k -> *) -> *) (FromMaybeSym0 k)

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

data FromMaybeSym1 l l

Instances

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

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

type FromMaybeSym2 t t = FromMaybe t t

data ListToMaybeSym0 l

Instances

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

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

type ListToMaybeSym1 t = ListToMaybe t

data MaybeToListSym0 l

Instances

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

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

type MaybeToListSym1 t = MaybeToList t

data CatMaybesSym0 l

Instances

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

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

type CatMaybesSym1 t = CatMaybes t

data MapMaybeSym0 l

Instances

SuppressUnusedWarnings (TyFun (TyFun k (Maybe k) -> *) (TyFun [k] [k] -> *) -> *) (MapMaybeSym0 k k)

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

data MapMaybeSym1 l l

Instances

SuppressUnusedWarnings ((TyFun k (Maybe k) -> *) -> TyFun [k] [k] -> *) (MapMaybeSym1 k k)

type Apply [k1] [k] (MapMaybeSym1 k k1 l1) l0 = MapMaybeSym2 k k1 l1 l0

type MapMaybeSym2 t t = MapMaybe t t