Copyright | (C) 2013-2014 Richard Eisenberg Jan Stolarek |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Ryan Scott |
Stability | experimental |
Portability | non-portable |
Safe Haskell | Safe-Inferred |
Language | GHC2021 |
Defines functions and datatypes relating to the singleton for Maybe
,
including singled versions 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
- type family Sing :: k -> Type
- data SMaybe :: forall (a :: Type). Maybe a -> Type where
- maybe_ :: b -> (a -> b) -> Maybe a -> b
- type family Maybe_ (a :: b) (a :: (~>) a b) (a :: Maybe a) :: b where ...
- sMaybe_ :: forall b a (t :: b) (t :: (~>) a b) (t :: Maybe a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Maybe_Sym0 t) t) t :: b)
- type family IsJust (a :: Maybe a) :: Bool where ...
- sIsJust :: forall a (t :: Maybe a). Sing t -> Sing (Apply IsJustSym0 t :: Bool)
- type family IsNothing (a :: Maybe a) :: Bool where ...
- sIsNothing :: forall a (t :: Maybe a). Sing t -> Sing (Apply IsNothingSym0 t :: Bool)
- type family FromJust (a :: Maybe a) :: a where ...
- sFromJust :: forall a (t :: Maybe a). Sing t -> Sing (Apply FromJustSym0 t :: a)
- type family FromMaybe (a :: a) (a :: Maybe a) :: a where ...
- sFromMaybe :: forall a (t :: a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply FromMaybeSym0 t) t :: a)
- type family ListToMaybe (a :: [a]) :: Maybe a where ...
- sListToMaybe :: forall a (t :: [a]). Sing t -> Sing (Apply ListToMaybeSym0 t :: Maybe a)
- type family MaybeToList (a :: Maybe a) :: [a] where ...
- sMaybeToList :: forall a (t :: Maybe a). Sing t -> Sing (Apply MaybeToListSym0 t :: [a])
- type family CatMaybes (a :: [Maybe a]) :: [a] where ...
- sCatMaybes :: forall a (t :: [Maybe a]). Sing t -> Sing (Apply CatMaybesSym0 t :: [a])
- type family MapMaybe (a :: (~>) a (Maybe b)) (a :: [a]) :: [b] where ...
- sMapMaybe :: forall a b (t :: (~>) a (Maybe b)) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply MapMaybeSym0 t) t :: [b])
- type family NothingSym0 :: Maybe (a :: Type) where ...
- data JustSym0 :: (~>) a (Maybe (a :: Type))
- type family JustSym1 (a6989586621679040342 :: a) :: Maybe (a :: Type) where ...
- data Maybe_Sym0 :: (~>) b ((~>) ((~>) a b) ((~>) (Maybe a) b))
- data Maybe_Sym1 (a6989586621679568692 :: b) :: (~>) ((~>) a b) ((~>) (Maybe a) b)
- data Maybe_Sym2 (a6989586621679568692 :: b) (a6989586621679568693 :: (~>) a b) :: (~>) (Maybe a) b
- type family Maybe_Sym3 (a6989586621679568692 :: b) (a6989586621679568693 :: (~>) a b) (a6989586621679568694 :: Maybe a) :: b where ...
- data IsJustSym0 :: (~>) (Maybe a) Bool
- type family IsJustSym1 (a6989586621679570864 :: Maybe a) :: Bool where ...
- data IsNothingSym0 :: (~>) (Maybe a) Bool
- type family IsNothingSym1 (a6989586621679570861 :: Maybe a) :: Bool where ...
- data FromJustSym0 :: (~>) (Maybe a) a
- type family FromJustSym1 (a6989586621679570857 :: Maybe a) :: a where ...
- data FromMaybeSym0 :: (~>) a ((~>) (Maybe a) a)
- data FromMaybeSym1 (a6989586621679570847 :: a) :: (~>) (Maybe a) a
- type family FromMaybeSym2 (a6989586621679570847 :: a) (a6989586621679570848 :: Maybe a) :: a where ...
- data ListToMaybeSym0 :: (~>) [a] (Maybe a)
- type family ListToMaybeSym1 (a6989586621679570838 :: [a]) :: Maybe a where ...
- data MaybeToListSym0 :: (~>) (Maybe a) [a]
- type family MaybeToListSym1 (a6989586621679570842 :: Maybe a) :: [a] where ...
- data CatMaybesSym0 :: (~>) [Maybe a] [a]
- type family CatMaybesSym1 (a6989586621679570832 :: [Maybe a]) :: [a] where ...
- data MapMaybeSym0 :: (~>) ((~>) a (Maybe b)) ((~>) [a] [b])
- data MapMaybeSym1 (a6989586621679570817 :: (~>) a (Maybe b)) :: (~>) [a] [b]
- type family MapMaybeSym2 (a6989586621679570817 :: (~>) a (Maybe b)) (a6989586621679570818 :: [a]) :: [b] where ...
Documentation
type family Sing :: k -> Type #
Instances
data SMaybe :: forall (a :: Type). Maybe a -> Type where Source #
SNothing :: forall (a :: Type). SMaybe ('Nothing :: Maybe (a :: Type)) | |
SJust :: forall (a :: Type) (n :: a). (Sing n) -> SMaybe ('Just n :: Maybe (a :: Type)) |
Instances
SDecide a => TestCoercion (SMaybe :: Maybe a -> Type) Source # | |
Defined in Data.Singletons.Base.Instances | |
SDecide a => TestEquality (SMaybe :: Maybe a -> Type) Source # | |
Defined in Data.Singletons.Base.Instances | |
ShowSing a => Show (SMaybe z) Source # | |
Singletons from Data.Maybe
sMaybe_ :: forall b a (t :: b) (t :: (~>) a b) (t :: Maybe a). 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
.
sIsNothing :: forall a (t :: Maybe a). Sing t -> Sing (Apply IsNothingSym0 t :: Bool) Source #
type family FromMaybe (a :: a) (a :: Maybe a) :: a where ... Source #
FromMaybe d x = Case_6989586621679570851 d x x |
sFromMaybe :: forall a (t :: a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply FromMaybeSym0 t) t :: a) Source #
type family ListToMaybe (a :: [a]) :: Maybe a where ... Source #
ListToMaybe '[] = NothingSym0 | |
ListToMaybe ('(:) a _) = Apply JustSym0 a |
sListToMaybe :: forall a (t :: [a]). Sing t -> Sing (Apply ListToMaybeSym0 t :: Maybe a) Source #
type family MaybeToList (a :: Maybe a) :: [a] where ... Source #
MaybeToList 'Nothing = NilSym0 | |
MaybeToList ('Just x) = Apply (Apply (:@#@$) x) NilSym0 |
sMaybeToList :: forall a (t :: Maybe a). Sing t -> Sing (Apply MaybeToListSym0 t :: [a]) Source #
type family CatMaybes (a :: [Maybe a]) :: [a] where ... Source #
CatMaybes '[] = NilSym0 | |
CatMaybes ('(:) ('Just x) xs) = Apply (Apply (:@#@$) x) (Apply CatMaybesSym0 xs) | |
CatMaybes ('(:) 'Nothing xs) = Apply CatMaybesSym0 xs |
sCatMaybes :: forall a (t :: [Maybe a]). Sing t -> Sing (Apply CatMaybesSym0 t :: [a]) Source #
sMapMaybe :: forall a b (t :: (~>) a (Maybe b)) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply MapMaybeSym0 t) t :: [b]) Source #
Defunctionalization symbols
type family NothingSym0 :: Maybe (a :: Type) where ... Source #
data JustSym0 :: (~>) a (Maybe (a :: Type)) Source #
Instances
SingI (JustSym0 :: TyFun a (Maybe a) -> Type) Source # | |
Defined in Data.Singletons.Base.Instances | |
SuppressUnusedWarnings (JustSym0 :: TyFun a (Maybe a) -> Type) Source # | |
Defined in Data.Singletons.Base.Instances suppressUnusedWarnings :: () # | |
type Apply (JustSym0 :: TyFun a (Maybe a) -> Type) (a6989586621679040342 :: a) Source # | |
Defined in Data.Singletons.Base.Instances |
data Maybe_Sym0 :: (~>) b ((~>) ((~>) a b) ((~>) (Maybe a) b)) Source #
Instances
SingI (Maybe_Sym0 :: TyFun b ((a ~> b) ~> (Maybe a ~> b)) -> Type) Source # | |
Defined in Data.Maybe.Singletons sing :: Sing Maybe_Sym0 | |
SuppressUnusedWarnings (Maybe_Sym0 :: TyFun b ((a ~> b) ~> (Maybe a ~> b)) -> Type) Source # | |
Defined in Data.Maybe.Singletons suppressUnusedWarnings :: () # | |
type Apply (Maybe_Sym0 :: TyFun b ((a ~> b) ~> (Maybe a ~> b)) -> Type) (a6989586621679568692 :: b) Source # | |
Defined in Data.Maybe.Singletons type Apply (Maybe_Sym0 :: TyFun b ((a ~> b) ~> (Maybe a ~> b)) -> Type) (a6989586621679568692 :: b) = Maybe_Sym1 a6989586621679568692 :: TyFun (a ~> b) (Maybe a ~> b) -> Type |
data Maybe_Sym1 (a6989586621679568692 :: b) :: (~>) ((~>) a b) ((~>) (Maybe a) b) Source #
Instances
SingI1 (Maybe_Sym1 :: b -> TyFun (a ~> b) (Maybe a ~> b) -> Type) Source # | |
Defined in Data.Maybe.Singletons liftSing :: forall (x :: k1). Sing x -> Sing (Maybe_Sym1 x) | |
SingI d => SingI (Maybe_Sym1 d :: TyFun (a ~> b) (Maybe a ~> b) -> Type) Source # | |
Defined in Data.Maybe.Singletons sing :: Sing (Maybe_Sym1 d) | |
SuppressUnusedWarnings (Maybe_Sym1 a6989586621679568692 :: TyFun (a ~> b) (Maybe a ~> b) -> Type) Source # | |
Defined in Data.Maybe.Singletons suppressUnusedWarnings :: () # | |
type Apply (Maybe_Sym1 a6989586621679568692 :: TyFun (a ~> b) (Maybe a ~> b) -> Type) (a6989586621679568693 :: a ~> b) Source # | |
Defined in Data.Maybe.Singletons type Apply (Maybe_Sym1 a6989586621679568692 :: TyFun (a ~> b) (Maybe a ~> b) -> Type) (a6989586621679568693 :: a ~> b) = Maybe_Sym2 a6989586621679568692 a6989586621679568693 |
data Maybe_Sym2 (a6989586621679568692 :: b) (a6989586621679568693 :: (~>) a b) :: (~>) (Maybe a) b Source #
Instances
SingI2 (Maybe_Sym2 :: b -> (a ~> b) -> TyFun (Maybe a) b -> Type) Source # | |
Defined in Data.Maybe.Singletons liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (Maybe_Sym2 x y) | |
SingI d => SingI1 (Maybe_Sym2 d :: (a ~> b) -> TyFun (Maybe a) b -> Type) Source # | |
Defined in Data.Maybe.Singletons liftSing :: forall (x :: k1). Sing x -> Sing (Maybe_Sym2 d x) | |
(SingI d1, SingI d2) => SingI (Maybe_Sym2 d1 d2 :: TyFun (Maybe a) b -> Type) Source # | |
Defined in Data.Maybe.Singletons sing :: Sing (Maybe_Sym2 d1 d2) | |
SuppressUnusedWarnings (Maybe_Sym2 a6989586621679568692 a6989586621679568693 :: TyFun (Maybe a) b -> Type) Source # | |
Defined in Data.Maybe.Singletons suppressUnusedWarnings :: () # | |
type Apply (Maybe_Sym2 a6989586621679568692 a6989586621679568693 :: TyFun (Maybe a) b -> Type) (a6989586621679568694 :: Maybe a) Source # | |
Defined in Data.Maybe.Singletons type Apply (Maybe_Sym2 a6989586621679568692 a6989586621679568693 :: TyFun (Maybe a) b -> Type) (a6989586621679568694 :: Maybe a) = Maybe_ a6989586621679568692 a6989586621679568693 a6989586621679568694 |
type family Maybe_Sym3 (a6989586621679568692 :: b) (a6989586621679568693 :: (~>) a b) (a6989586621679568694 :: Maybe a) :: b where ... Source #
Maybe_Sym3 a6989586621679568692 a6989586621679568693 a6989586621679568694 = Maybe_ a6989586621679568692 a6989586621679568693 a6989586621679568694 |
data IsJustSym0 :: (~>) (Maybe a) Bool Source #
Instances
SingI (IsJustSym0 :: TyFun (Maybe a) Bool -> Type) Source # | |
Defined in Data.Maybe.Singletons sing :: Sing IsJustSym0 | |
SuppressUnusedWarnings (IsJustSym0 :: TyFun (Maybe a) Bool -> Type) Source # | |
Defined in Data.Maybe.Singletons suppressUnusedWarnings :: () # | |
type Apply (IsJustSym0 :: TyFun (Maybe a) Bool -> Type) (a6989586621679570864 :: Maybe a) Source # | |
Defined in Data.Maybe.Singletons |
type family IsJustSym1 (a6989586621679570864 :: Maybe a) :: Bool where ... Source #
IsJustSym1 a6989586621679570864 = IsJust a6989586621679570864 |
data IsNothingSym0 :: (~>) (Maybe a) Bool Source #
Instances
SingI (IsNothingSym0 :: TyFun (Maybe a) Bool -> Type) Source # | |
Defined in Data.Maybe.Singletons | |
SuppressUnusedWarnings (IsNothingSym0 :: TyFun (Maybe a) Bool -> Type) Source # | |
Defined in Data.Maybe.Singletons suppressUnusedWarnings :: () # | |
type Apply (IsNothingSym0 :: TyFun (Maybe a) Bool -> Type) (a6989586621679570861 :: Maybe a) Source # | |
Defined in Data.Maybe.Singletons |
type family IsNothingSym1 (a6989586621679570861 :: Maybe a) :: Bool where ... Source #
IsNothingSym1 a6989586621679570861 = IsNothing a6989586621679570861 |
data FromJustSym0 :: (~>) (Maybe a) a Source #
Instances
SingI (FromJustSym0 :: TyFun (Maybe a) a -> Type) Source # | |
Defined in Data.Maybe.Singletons sing :: Sing FromJustSym0 | |
SuppressUnusedWarnings (FromJustSym0 :: TyFun (Maybe a) a -> Type) Source # | |
Defined in Data.Maybe.Singletons suppressUnusedWarnings :: () # | |
type Apply (FromJustSym0 :: TyFun (Maybe a) a -> Type) (a6989586621679570857 :: Maybe a) Source # | |
Defined in Data.Maybe.Singletons type Apply (FromJustSym0 :: TyFun (Maybe a) a -> Type) (a6989586621679570857 :: Maybe a) = FromJust a6989586621679570857 |
type family FromJustSym1 (a6989586621679570857 :: Maybe a) :: a where ... Source #
FromJustSym1 a6989586621679570857 = FromJust a6989586621679570857 |
data FromMaybeSym0 :: (~>) a ((~>) (Maybe a) a) Source #
Instances
SingI (FromMaybeSym0 :: TyFun a (Maybe a ~> a) -> Type) Source # | |
Defined in Data.Maybe.Singletons | |
SuppressUnusedWarnings (FromMaybeSym0 :: TyFun a (Maybe a ~> a) -> Type) Source # | |
Defined in Data.Maybe.Singletons suppressUnusedWarnings :: () # | |
type Apply (FromMaybeSym0 :: TyFun a (Maybe a ~> a) -> Type) (a6989586621679570847 :: a) Source # | |
Defined in Data.Maybe.Singletons type Apply (FromMaybeSym0 :: TyFun a (Maybe a ~> a) -> Type) (a6989586621679570847 :: a) = FromMaybeSym1 a6989586621679570847 |
data FromMaybeSym1 (a6989586621679570847 :: a) :: (~>) (Maybe a) a Source #
Instances
SingI1 (FromMaybeSym1 :: a -> TyFun (Maybe a) a -> Type) Source # | |
Defined in Data.Maybe.Singletons liftSing :: forall (x :: k1). Sing x -> Sing (FromMaybeSym1 x) | |
SingI d => SingI (FromMaybeSym1 d :: TyFun (Maybe a) a -> Type) Source # | |
Defined in Data.Maybe.Singletons sing :: Sing (FromMaybeSym1 d) | |
SuppressUnusedWarnings (FromMaybeSym1 a6989586621679570847 :: TyFun (Maybe a) a -> Type) Source # | |
Defined in Data.Maybe.Singletons suppressUnusedWarnings :: () # | |
type Apply (FromMaybeSym1 a6989586621679570847 :: TyFun (Maybe a) a -> Type) (a6989586621679570848 :: Maybe a) Source # | |
Defined in Data.Maybe.Singletons type Apply (FromMaybeSym1 a6989586621679570847 :: TyFun (Maybe a) a -> Type) (a6989586621679570848 :: Maybe a) = FromMaybe a6989586621679570847 a6989586621679570848 |
type family FromMaybeSym2 (a6989586621679570847 :: a) (a6989586621679570848 :: Maybe a) :: a where ... Source #
FromMaybeSym2 a6989586621679570847 a6989586621679570848 = FromMaybe a6989586621679570847 a6989586621679570848 |
data ListToMaybeSym0 :: (~>) [a] (Maybe a) Source #
Instances
SingI (ListToMaybeSym0 :: TyFun [a] (Maybe a) -> Type) Source # | |
Defined in Data.Maybe.Singletons | |
SuppressUnusedWarnings (ListToMaybeSym0 :: TyFun [a] (Maybe a) -> Type) Source # | |
Defined in Data.Maybe.Singletons suppressUnusedWarnings :: () # | |
type Apply (ListToMaybeSym0 :: TyFun [a] (Maybe a) -> Type) (a6989586621679570838 :: [a]) Source # | |
Defined in Data.Maybe.Singletons type Apply (ListToMaybeSym0 :: TyFun [a] (Maybe a) -> Type) (a6989586621679570838 :: [a]) = ListToMaybe a6989586621679570838 |
type family ListToMaybeSym1 (a6989586621679570838 :: [a]) :: Maybe a where ... Source #
ListToMaybeSym1 a6989586621679570838 = ListToMaybe a6989586621679570838 |
data MaybeToListSym0 :: (~>) (Maybe a) [a] Source #
Instances
SingI (MaybeToListSym0 :: TyFun (Maybe a) [a] -> Type) Source # | |
Defined in Data.Maybe.Singletons | |
SuppressUnusedWarnings (MaybeToListSym0 :: TyFun (Maybe a) [a] -> Type) Source # | |
Defined in Data.Maybe.Singletons suppressUnusedWarnings :: () # | |
type Apply (MaybeToListSym0 :: TyFun (Maybe a) [a] -> Type) (a6989586621679570842 :: Maybe a) Source # | |
Defined in Data.Maybe.Singletons type Apply (MaybeToListSym0 :: TyFun (Maybe a) [a] -> Type) (a6989586621679570842 :: Maybe a) = MaybeToList a6989586621679570842 |
type family MaybeToListSym1 (a6989586621679570842 :: Maybe a) :: [a] where ... Source #
MaybeToListSym1 a6989586621679570842 = MaybeToList a6989586621679570842 |
data CatMaybesSym0 :: (~>) [Maybe a] [a] Source #
Instances
SingI (CatMaybesSym0 :: TyFun [Maybe a] [a] -> Type) Source # | |
Defined in Data.Maybe.Singletons | |
SuppressUnusedWarnings (CatMaybesSym0 :: TyFun [Maybe a] [a] -> Type) Source # | |
Defined in Data.Maybe.Singletons suppressUnusedWarnings :: () # | |
type Apply (CatMaybesSym0 :: TyFun [Maybe a] [a] -> Type) (a6989586621679570832 :: [Maybe a]) Source # | |
Defined in Data.Maybe.Singletons type Apply (CatMaybesSym0 :: TyFun [Maybe a] [a] -> Type) (a6989586621679570832 :: [Maybe a]) = CatMaybes a6989586621679570832 |
type family CatMaybesSym1 (a6989586621679570832 :: [Maybe a]) :: [a] where ... Source #
CatMaybesSym1 a6989586621679570832 = CatMaybes a6989586621679570832 |
data MapMaybeSym0 :: (~>) ((~>) a (Maybe b)) ((~>) [a] [b]) Source #
Instances
SingI (MapMaybeSym0 :: TyFun (a ~> Maybe b) ([a] ~> [b]) -> Type) Source # | |
Defined in Data.Maybe.Singletons sing :: Sing MapMaybeSym0 | |
SuppressUnusedWarnings (MapMaybeSym0 :: TyFun (a ~> Maybe b) ([a] ~> [b]) -> Type) Source # | |
Defined in Data.Maybe.Singletons suppressUnusedWarnings :: () # | |
type Apply (MapMaybeSym0 :: TyFun (a ~> Maybe b) ([a] ~> [b]) -> Type) (a6989586621679570817 :: a ~> Maybe b) Source # | |
Defined in Data.Maybe.Singletons type Apply (MapMaybeSym0 :: TyFun (a ~> Maybe b) ([a] ~> [b]) -> Type) (a6989586621679570817 :: a ~> Maybe b) = MapMaybeSym1 a6989586621679570817 |
data MapMaybeSym1 (a6989586621679570817 :: (~>) a (Maybe b)) :: (~>) [a] [b] Source #
Instances
SingI1 (MapMaybeSym1 :: (a ~> Maybe b) -> TyFun [a] [b] -> Type) Source # | |
Defined in Data.Maybe.Singletons liftSing :: forall (x :: k1). Sing x -> Sing (MapMaybeSym1 x) | |
SingI d => SingI (MapMaybeSym1 d :: TyFun [a] [b] -> Type) Source # | |
Defined in Data.Maybe.Singletons sing :: Sing (MapMaybeSym1 d) | |
SuppressUnusedWarnings (MapMaybeSym1 a6989586621679570817 :: TyFun [a] [b] -> Type) Source # | |
Defined in Data.Maybe.Singletons suppressUnusedWarnings :: () # | |
type Apply (MapMaybeSym1 a6989586621679570817 :: TyFun [a] [b] -> Type) (a6989586621679570818 :: [a]) Source # | |
Defined in Data.Maybe.Singletons type Apply (MapMaybeSym1 a6989586621679570817 :: TyFun [a] [b] -> Type) (a6989586621679570818 :: [a]) = MapMaybe a6989586621679570817 a6989586621679570818 |
type family MapMaybeSym2 (a6989586621679570817 :: (~>) a (Maybe b)) (a6989586621679570818 :: [a]) :: [b] where ... Source #
MapMaybeSym2 a6989586621679570817 a6989586621679570818 = MapMaybe a6989586621679570817 a6989586621679570818 |