| 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 | Haskell2010 |
Data.Maybe.Singletons
Description
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 (a6989586621679042084 :: a) :: Maybe (a :: Type) where ...
- data Maybe_Sym0 :: (~>) b ((~>) ((~>) a b) ((~>) (Maybe a) b))
- data Maybe_Sym1 (a6989586621679569538 :: b) :: (~>) ((~>) a b) ((~>) (Maybe a) b)
- data Maybe_Sym2 (a6989586621679569538 :: b) (a6989586621679569539 :: (~>) a b) :: (~>) (Maybe a) b
- type family Maybe_Sym3 (a6989586621679569538 :: b) (a6989586621679569539 :: (~>) a b) (a6989586621679569540 :: Maybe a) :: b where ...
- data IsJustSym0 :: (~>) (Maybe a) Bool
- type family IsJustSym1 (a6989586621679571618 :: Maybe a) :: Bool where ...
- data IsNothingSym0 :: (~>) (Maybe a) Bool
- type family IsNothingSym1 (a6989586621679571615 :: Maybe a) :: Bool where ...
- data FromJustSym0 :: (~>) (Maybe a) a
- type family FromJustSym1 (a6989586621679571611 :: Maybe a) :: a where ...
- data FromMaybeSym0 :: (~>) a ((~>) (Maybe a) a)
- data FromMaybeSym1 (a6989586621679571601 :: a) :: (~>) (Maybe a) a
- type family FromMaybeSym2 (a6989586621679571601 :: a) (a6989586621679571602 :: Maybe a) :: a where ...
- data ListToMaybeSym0 :: (~>) [a] (Maybe a)
- type family ListToMaybeSym1 (a6989586621679571592 :: [a]) :: Maybe a where ...
- data MaybeToListSym0 :: (~>) (Maybe a) [a]
- type family MaybeToListSym1 (a6989586621679571596 :: Maybe a) :: [a] where ...
- data CatMaybesSym0 :: (~>) [Maybe a] [a]
- type family CatMaybesSym1 (a6989586621679571586 :: [Maybe a]) :: [a] where ...
- data MapMaybeSym0 :: (~>) ((~>) a (Maybe b)) ((~>) [a] [b])
- data MapMaybeSym1 (a6989586621679571571 :: (~>) a (Maybe b)) :: (~>) [a] [b]
- type family MapMaybeSym2 (a6989586621679571571 :: (~>) a (Maybe b)) (a6989586621679571572 :: [a]) :: [b] where ...
Documentation
type family Sing :: k -> Type #
Instances
data SMaybe :: forall (a :: Type). Maybe a -> Type where Source #
Constructors
| 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 #
Equations
| FromMaybe d x = Case_6989586621679571605 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 #
Equations
| 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 #
Equations
| 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 #
Equations
| 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 #
Equations
| NothingSym0 = 'Nothing |
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 Methods suppressUnusedWarnings :: () # | |
| type Apply (JustSym0 :: TyFun a (Maybe a) -> Type) (a6989586621679042084 :: 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 Methods sing :: Sing Maybe_Sym0 | |
| SuppressUnusedWarnings (Maybe_Sym0 :: TyFun b ((a ~> b) ~> (Maybe a ~> b)) -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (Maybe_Sym0 :: TyFun b ((a ~> b) ~> (Maybe a ~> b)) -> Type) (a6989586621679569538 :: b) Source # | |
Defined in Data.Maybe.Singletons type Apply (Maybe_Sym0 :: TyFun b ((a ~> b) ~> (Maybe a ~> b)) -> Type) (a6989586621679569538 :: b) = Maybe_Sym1 a6989586621679569538 :: TyFun (a ~> b) (Maybe a ~> b) -> Type | |
data Maybe_Sym1 (a6989586621679569538 :: 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 Methods 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 Methods sing :: Sing (Maybe_Sym1 d) | |
| SuppressUnusedWarnings (Maybe_Sym1 a6989586621679569538 :: TyFun (a ~> b) (Maybe a ~> b) -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (Maybe_Sym1 a6989586621679569538 :: TyFun (a ~> b) (Maybe a ~> b) -> Type) (a6989586621679569539 :: a ~> b) Source # | |
Defined in Data.Maybe.Singletons type Apply (Maybe_Sym1 a6989586621679569538 :: TyFun (a ~> b) (Maybe a ~> b) -> Type) (a6989586621679569539 :: a ~> b) = Maybe_Sym2 a6989586621679569538 a6989586621679569539 | |
data Maybe_Sym2 (a6989586621679569538 :: b) (a6989586621679569539 :: (~>) a b) :: (~>) (Maybe a) b Source #
Instances
| SingI2 (Maybe_Sym2 :: b -> (a ~> b) -> TyFun (Maybe a) b -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods 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 Methods 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 Methods sing :: Sing (Maybe_Sym2 d1 d2) | |
| SuppressUnusedWarnings (Maybe_Sym2 a6989586621679569538 a6989586621679569539 :: TyFun (Maybe a) b -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (Maybe_Sym2 a6989586621679569538 a6989586621679569539 :: TyFun (Maybe a) b -> Type) (a6989586621679569540 :: Maybe a) Source # | |
Defined in Data.Maybe.Singletons type Apply (Maybe_Sym2 a6989586621679569538 a6989586621679569539 :: TyFun (Maybe a) b -> Type) (a6989586621679569540 :: Maybe a) = Maybe_ a6989586621679569538 a6989586621679569539 a6989586621679569540 | |
type family Maybe_Sym3 (a6989586621679569538 :: b) (a6989586621679569539 :: (~>) a b) (a6989586621679569540 :: Maybe a) :: b where ... Source #
Equations
| Maybe_Sym3 a6989586621679569538 a6989586621679569539 a6989586621679569540 = Maybe_ a6989586621679569538 a6989586621679569539 a6989586621679569540 |
data IsJustSym0 :: (~>) (Maybe a) Bool Source #
Instances
| SingI (IsJustSym0 :: TyFun (Maybe a) Bool -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods sing :: Sing IsJustSym0 | |
| SuppressUnusedWarnings (IsJustSym0 :: TyFun (Maybe a) Bool -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (IsJustSym0 :: TyFun (Maybe a) Bool -> Type) (a6989586621679571618 :: Maybe a) Source # | |
Defined in Data.Maybe.Singletons | |
type family IsJustSym1 (a6989586621679571618 :: Maybe a) :: Bool where ... Source #
Equations
| IsJustSym1 a6989586621679571618 = IsJust a6989586621679571618 |
data IsNothingSym0 :: (~>) (Maybe a) Bool Source #
Instances
| SingI (IsNothingSym0 :: TyFun (Maybe a) Bool -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods | |
| SuppressUnusedWarnings (IsNothingSym0 :: TyFun (Maybe a) Bool -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (IsNothingSym0 :: TyFun (Maybe a) Bool -> Type) (a6989586621679571615 :: Maybe a) Source # | |
Defined in Data.Maybe.Singletons | |
type family IsNothingSym1 (a6989586621679571615 :: Maybe a) :: Bool where ... Source #
Equations
| IsNothingSym1 a6989586621679571615 = IsNothing a6989586621679571615 |
data FromJustSym0 :: (~>) (Maybe a) a Source #
Instances
| SingI (FromJustSym0 :: TyFun (Maybe a) a -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods sing :: Sing FromJustSym0 | |
| SuppressUnusedWarnings (FromJustSym0 :: TyFun (Maybe a) a -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (FromJustSym0 :: TyFun (Maybe a) a -> Type) (a6989586621679571611 :: Maybe a) Source # | |
Defined in Data.Maybe.Singletons type Apply (FromJustSym0 :: TyFun (Maybe a) a -> Type) (a6989586621679571611 :: Maybe a) = FromJust a6989586621679571611 | |
type family FromJustSym1 (a6989586621679571611 :: Maybe a) :: a where ... Source #
Equations
| FromJustSym1 a6989586621679571611 = FromJust a6989586621679571611 |
data FromMaybeSym0 :: (~>) a ((~>) (Maybe a) a) Source #
Instances
| SingI (FromMaybeSym0 :: TyFun a (Maybe a ~> a) -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods | |
| SuppressUnusedWarnings (FromMaybeSym0 :: TyFun a (Maybe a ~> a) -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (FromMaybeSym0 :: TyFun a (Maybe a ~> a) -> Type) (a6989586621679571601 :: a) Source # | |
Defined in Data.Maybe.Singletons type Apply (FromMaybeSym0 :: TyFun a (Maybe a ~> a) -> Type) (a6989586621679571601 :: a) = FromMaybeSym1 a6989586621679571601 | |
data FromMaybeSym1 (a6989586621679571601 :: a) :: (~>) (Maybe a) a Source #
Instances
| SingI1 (FromMaybeSym1 :: a -> TyFun (Maybe a) a -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods 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 Methods sing :: Sing (FromMaybeSym1 d) | |
| SuppressUnusedWarnings (FromMaybeSym1 a6989586621679571601 :: TyFun (Maybe a) a -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (FromMaybeSym1 a6989586621679571601 :: TyFun (Maybe a) a -> Type) (a6989586621679571602 :: Maybe a) Source # | |
Defined in Data.Maybe.Singletons type Apply (FromMaybeSym1 a6989586621679571601 :: TyFun (Maybe a) a -> Type) (a6989586621679571602 :: Maybe a) = FromMaybe a6989586621679571601 a6989586621679571602 | |
type family FromMaybeSym2 (a6989586621679571601 :: a) (a6989586621679571602 :: Maybe a) :: a where ... Source #
Equations
| FromMaybeSym2 a6989586621679571601 a6989586621679571602 = FromMaybe a6989586621679571601 a6989586621679571602 |
data ListToMaybeSym0 :: (~>) [a] (Maybe a) Source #
Instances
| SingI (ListToMaybeSym0 :: TyFun [a] (Maybe a) -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods | |
| SuppressUnusedWarnings (ListToMaybeSym0 :: TyFun [a] (Maybe a) -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (ListToMaybeSym0 :: TyFun [a] (Maybe a) -> Type) (a6989586621679571592 :: [a]) Source # | |
Defined in Data.Maybe.Singletons type Apply (ListToMaybeSym0 :: TyFun [a] (Maybe a) -> Type) (a6989586621679571592 :: [a]) = ListToMaybe a6989586621679571592 | |
type family ListToMaybeSym1 (a6989586621679571592 :: [a]) :: Maybe a where ... Source #
Equations
| ListToMaybeSym1 a6989586621679571592 = ListToMaybe a6989586621679571592 |
data MaybeToListSym0 :: (~>) (Maybe a) [a] Source #
Instances
| SingI (MaybeToListSym0 :: TyFun (Maybe a) [a] -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods | |
| SuppressUnusedWarnings (MaybeToListSym0 :: TyFun (Maybe a) [a] -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (MaybeToListSym0 :: TyFun (Maybe a) [a] -> Type) (a6989586621679571596 :: Maybe a) Source # | |
Defined in Data.Maybe.Singletons type Apply (MaybeToListSym0 :: TyFun (Maybe a) [a] -> Type) (a6989586621679571596 :: Maybe a) = MaybeToList a6989586621679571596 | |
type family MaybeToListSym1 (a6989586621679571596 :: Maybe a) :: [a] where ... Source #
Equations
| MaybeToListSym1 a6989586621679571596 = MaybeToList a6989586621679571596 |
data CatMaybesSym0 :: (~>) [Maybe a] [a] Source #
Instances
| SingI (CatMaybesSym0 :: TyFun [Maybe a] [a] -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods | |
| SuppressUnusedWarnings (CatMaybesSym0 :: TyFun [Maybe a] [a] -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (CatMaybesSym0 :: TyFun [Maybe a] [a] -> Type) (a6989586621679571586 :: [Maybe a]) Source # | |
Defined in Data.Maybe.Singletons type Apply (CatMaybesSym0 :: TyFun [Maybe a] [a] -> Type) (a6989586621679571586 :: [Maybe a]) = CatMaybes a6989586621679571586 | |
type family CatMaybesSym1 (a6989586621679571586 :: [Maybe a]) :: [a] where ... Source #
Equations
| CatMaybesSym1 a6989586621679571586 = CatMaybes a6989586621679571586 |
data MapMaybeSym0 :: (~>) ((~>) a (Maybe b)) ((~>) [a] [b]) Source #
Instances
| SingI (MapMaybeSym0 :: TyFun (a ~> Maybe b) ([a] ~> [b]) -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods sing :: Sing MapMaybeSym0 | |
| SuppressUnusedWarnings (MapMaybeSym0 :: TyFun (a ~> Maybe b) ([a] ~> [b]) -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (MapMaybeSym0 :: TyFun (a ~> Maybe b) ([a] ~> [b]) -> Type) (a6989586621679571571 :: a ~> Maybe b) Source # | |
Defined in Data.Maybe.Singletons type Apply (MapMaybeSym0 :: TyFun (a ~> Maybe b) ([a] ~> [b]) -> Type) (a6989586621679571571 :: a ~> Maybe b) = MapMaybeSym1 a6989586621679571571 | |
data MapMaybeSym1 (a6989586621679571571 :: (~>) a (Maybe b)) :: (~>) [a] [b] Source #
Instances
| SingI1 (MapMaybeSym1 :: (a ~> Maybe b) -> TyFun [a] [b] -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing (MapMaybeSym1 x) | |
| SingI d => SingI (MapMaybeSym1 d :: TyFun [a] [b] -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods sing :: Sing (MapMaybeSym1 d) | |
| SuppressUnusedWarnings (MapMaybeSym1 a6989586621679571571 :: TyFun [a] [b] -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (MapMaybeSym1 a6989586621679571571 :: TyFun [a] [b] -> Type) (a6989586621679571572 :: [a]) Source # | |
Defined in Data.Maybe.Singletons type Apply (MapMaybeSym1 a6989586621679571571 :: TyFun [a] [b] -> Type) (a6989586621679571572 :: [a]) = MapMaybe a6989586621679571571 a6989586621679571572 | |
type family MapMaybeSym2 (a6989586621679571571 :: (~>) a (Maybe b)) (a6989586621679571572 :: [a]) :: [b] where ... Source #
Equations
| MapMaybeSym2 a6989586621679571571 a6989586621679571572 = MapMaybe a6989586621679571571 a6989586621679571572 |