| Copyright | (C) 2013-2014 Richard Eisenberg Jan Stolarek |
|---|---|
| License | BSD-style (see LICENSE) |
| Maintainer | Ryan Scott |
| Stability | experimental |
| Portability | non-portable |
| Safe Haskell | None |
| Language | GHC2021 |
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 (a1 :: Maybe a) where
- maybe_ :: b -> (a -> b) -> Maybe a -> b
- type family Maybe_ (a1 :: b) (a2 :: a ~> b) (a3 :: Maybe a) :: b where ...
- sMaybe_ :: forall b a (t1 :: b) (t2 :: a ~> b) (t3 :: Maybe a). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Maybe_ t1 t2 t3)
- type family IsJust (a1 :: Maybe a) :: Bool where ...
- sIsJust :: forall a (t :: Maybe a). Sing t -> Sing (IsJust t)
- type family IsNothing (a1 :: Maybe a) :: Bool where ...
- sIsNothing :: forall a (t :: Maybe a). Sing t -> Sing (IsNothing t)
- type family FromJust (a1 :: Maybe a) :: a where ...
- sFromJust :: forall a (t :: Maybe a). Sing t -> Sing (FromJust t)
- type family FromMaybe (a1 :: a) (a2 :: Maybe a) :: a where ...
- sFromMaybe :: forall a (t1 :: a) (t2 :: Maybe a). Sing t1 -> Sing t2 -> Sing (FromMaybe t1 t2)
- type family ListToMaybe (a1 :: [a]) :: Maybe a where ...
- sListToMaybe :: forall a (t :: [a]). Sing t -> Sing (ListToMaybe t)
- type family MaybeToList (a1 :: Maybe a) :: [a] where ...
- sMaybeToList :: forall a (t :: Maybe a). Sing t -> Sing (MaybeToList t)
- type family CatMaybes (a1 :: [Maybe a]) :: [a] where ...
- sCatMaybes :: forall a (t :: [Maybe a]). Sing t -> Sing (CatMaybes t)
- type family MapMaybe (a1 :: a ~> Maybe b) (a2 :: [a]) :: [b] where ...
- sMapMaybe :: forall a b (t1 :: a ~> Maybe b) (t2 :: [a]). Sing t1 -> Sing t2 -> Sing (MapMaybe t1 t2)
- type family NothingSym0 :: Maybe a where ...
- data JustSym0 (a1 :: TyFun a (Maybe a))
- type family JustSym1 (a6989586621679050265 :: a) :: Maybe a where ...
- data Maybe_Sym0 (a1 :: TyFun b ((a ~> b) ~> (Maybe a ~> b)))
- data Maybe_Sym1 (a6989586621679387993 :: b) (b1 :: TyFun (a ~> b) (Maybe a ~> b))
- data Maybe_Sym2 (a6989586621679387993 :: b) (a6989586621679387994 :: a ~> b) (c :: TyFun (Maybe a) b)
- type family Maybe_Sym3 (a6989586621679387993 :: b) (a6989586621679387994 :: a ~> b) (a6989586621679387995 :: Maybe a) :: b where ...
- data IsJustSym0 (a1 :: TyFun (Maybe a) Bool)
- type family IsJustSym1 (a6989586621679390233 :: Maybe a) :: Bool where ...
- data IsNothingSym0 (a1 :: TyFun (Maybe a) Bool)
- type family IsNothingSym1 (a6989586621679390230 :: Maybe a) :: Bool where ...
- data FromJustSym0 (a1 :: TyFun (Maybe a) a)
- type family FromJustSym1 (a6989586621679390226 :: Maybe a) :: a where ...
- data FromMaybeSym0 (a1 :: TyFun a (Maybe a ~> a))
- data FromMaybeSym1 (a6989586621679390214 :: a) (b :: TyFun (Maybe a) a)
- type family FromMaybeSym2 (a6989586621679390214 :: a) (a6989586621679390215 :: Maybe a) :: a where ...
- data ListToMaybeSym0 (a1 :: TyFun [a] (Maybe a))
- type family ListToMaybeSym1 (a6989586621679390205 :: [a]) :: Maybe a where ...
- data MaybeToListSym0 (a1 :: TyFun (Maybe a) [a])
- type family MaybeToListSym1 (a6989586621679390209 :: Maybe a) :: [a] where ...
- data CatMaybesSym0 (a1 :: TyFun [Maybe a] [a])
- type family CatMaybesSym1 (a6989586621679390199 :: [Maybe a]) :: [a] where ...
- data MapMaybeSym0 (a1 :: TyFun (a ~> Maybe b) ([a] ~> [b]))
- data MapMaybeSym1 (a6989586621679390184 :: a ~> Maybe b) (b1 :: TyFun [a] [b])
- type family MapMaybeSym2 (a6989586621679390184 :: a ~> Maybe b) (a6989586621679390185 :: [a]) :: [b] where ...
Documentation
type family Sing :: k -> Type #
Instances
data SMaybe (a1 :: Maybe a) where Source #
Constructors
| SNothing :: forall a. SMaybe ('Nothing :: Maybe a) | |
| SJust :: forall a (n :: a). Sing n -> SMaybe ('Just n) |
Singletons from Data.Maybe
sMaybe_ :: forall b a (t1 :: b) (t2 :: a ~> b) (t3 :: Maybe a). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Maybe_ t1 t2 t3) 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.
sFromMaybe :: forall a (t1 :: a) (t2 :: Maybe a). Sing t1 -> Sing t2 -> Sing (FromMaybe t1 t2) Source #
type family ListToMaybe (a1 :: [a]) :: Maybe a where ... Source #
Equations
| ListToMaybe ('[] :: [a]) = NothingSym0 :: Maybe a | |
| ListToMaybe (a ': _1 :: [k1]) = Apply (JustSym0 :: TyFun k1 (Maybe k1) -> Type) a |
sListToMaybe :: forall a (t :: [a]). Sing t -> Sing (ListToMaybe t) Source #
type family MaybeToList (a1 :: Maybe a) :: [a] where ... Source #
sMaybeToList :: forall a (t :: Maybe a). Sing t -> Sing (MaybeToList t) Source #
type family CatMaybes (a1 :: [Maybe a]) :: [a] where ... Source #
Equations
| CatMaybes ('[] :: [Maybe a]) = NilSym0 :: [a] | |
| CatMaybes ('Just x ': xs :: [Maybe a]) = Apply (Apply ((:@#@$) :: TyFun a ([a] ~> [a]) -> Type) x) (Apply (CatMaybesSym0 :: TyFun [Maybe a] [a] -> Type) xs) | |
| CatMaybes (('Nothing :: Maybe a) ': xs :: [Maybe a]) = Apply (CatMaybesSym0 :: TyFun [Maybe a] [a] -> Type) xs |
sMapMaybe :: forall a b (t1 :: a ~> Maybe b) (t2 :: [a]). Sing t1 -> Sing t2 -> Sing (MapMaybe t1 t2) Source #
Defunctionalization symbols
type family NothingSym0 :: Maybe a where ... Source #
Equations
| NothingSym0 = 'Nothing :: Maybe a |
data JustSym0 (a1 :: TyFun a (Maybe a)) Source #
Instances
data Maybe_Sym0 (a1 :: TyFun b ((a ~> b) ~> (Maybe a ~> b))) Source #
Instances
| SingI (Maybe_Sym0 :: TyFun b ((a ~> b) ~> (Maybe a ~> b)) -> Type) Source # | |
| 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) (a6989586621679387993 :: b) Source # | |
Defined in Data.Maybe.Singletons | |
data Maybe_Sym1 (a6989586621679387993 :: b) (b1 :: TyFun (a ~> b) (Maybe a ~> b)) Source #
Instances
| SingI1 (Maybe_Sym1 :: b -> TyFun (a ~> b) (Maybe a ~> b) -> Type) Source # | |
| SingI d => SingI (Maybe_Sym1 d :: TyFun (a ~> b) (Maybe a ~> b) -> Type) Source # | |
Defined in Data.Maybe.Singletons | |
| SuppressUnusedWarnings (Maybe_Sym1 a6989586621679387993 :: TyFun (a ~> b) (Maybe a ~> b) -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (Maybe_Sym1 a6989586621679387993 :: TyFun (a ~> b) (Maybe a ~> b) -> Type) (a6989586621679387994 :: a ~> b) Source # | |
Defined in Data.Maybe.Singletons type Apply (Maybe_Sym1 a6989586621679387993 :: TyFun (a ~> b) (Maybe a ~> b) -> Type) (a6989586621679387994 :: a ~> b) = Maybe_Sym2 a6989586621679387993 a6989586621679387994 | |
data Maybe_Sym2 (a6989586621679387993 :: b) (a6989586621679387994 :: a ~> b) (c :: TyFun (Maybe a) b) Source #
Instances
| SingI2 (Maybe_Sym2 :: b -> (a ~> b) -> TyFun (Maybe a) b -> Type) Source # | |
Defined in Data.Maybe.Singletons | |
| SingI d => SingI1 (Maybe_Sym2 d :: (a ~> b) -> TyFun (Maybe a) b -> Type) Source # | |
Defined in Data.Maybe.Singletons | |
| (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 a6989586621679387993 a6989586621679387994 :: TyFun (Maybe a) b -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (Maybe_Sym2 a6989586621679387993 a6989586621679387994 :: TyFun (Maybe a) b -> Type) (a6989586621679387995 :: Maybe a) Source # | |
Defined in Data.Maybe.Singletons | |
type family Maybe_Sym3 (a6989586621679387993 :: b) (a6989586621679387994 :: a ~> b) (a6989586621679387995 :: Maybe a) :: b where ... Source #
Equations
| Maybe_Sym3 (a6989586621679387993 :: b) (a6989586621679387994 :: a ~> b) (a6989586621679387995 :: Maybe a) = Maybe_ a6989586621679387993 a6989586621679387994 a6989586621679387995 |
data IsJustSym0 (a1 :: TyFun (Maybe a) Bool) Source #
Instances
| SingI (IsJustSym0 :: TyFun (Maybe a) Bool -> Type) Source # | |
Defined in Data.Maybe.Singletons | |
| SuppressUnusedWarnings (IsJustSym0 :: TyFun (Maybe a) Bool -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (IsJustSym0 :: TyFun (Maybe a) Bool -> Type) (a6989586621679390233 :: Maybe a) Source # | |
Defined in Data.Maybe.Singletons | |
type family IsJustSym1 (a6989586621679390233 :: Maybe a) :: Bool where ... Source #
Equations
| IsJustSym1 (a6989586621679390233 :: Maybe a) = IsJust a6989586621679390233 |
data IsNothingSym0 (a1 :: TyFun (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 Methods suppressUnusedWarnings :: () # | |
| type Apply (IsNothingSym0 :: TyFun (Maybe a) Bool -> Type) (a6989586621679390230 :: Maybe a) Source # | |
Defined in Data.Maybe.Singletons | |
type family IsNothingSym1 (a6989586621679390230 :: Maybe a) :: Bool where ... Source #
Equations
| IsNothingSym1 (a6989586621679390230 :: Maybe a) = IsNothing a6989586621679390230 |
data FromJustSym0 (a1 :: TyFun (Maybe a) a) Source #
Instances
| SingI (FromJustSym0 :: TyFun (Maybe a) a -> Type) Source # | |
Defined in Data.Maybe.Singletons | |
| SuppressUnusedWarnings (FromJustSym0 :: TyFun (Maybe a) a -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (FromJustSym0 :: TyFun (Maybe a) a -> Type) (a6989586621679390226 :: Maybe a) Source # | |
Defined in Data.Maybe.Singletons | |
type family FromJustSym1 (a6989586621679390226 :: Maybe a) :: a where ... Source #
Equations
| FromJustSym1 (a6989586621679390226 :: Maybe a) = FromJust a6989586621679390226 |
data FromMaybeSym0 (a1 :: TyFun 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 Methods suppressUnusedWarnings :: () # | |
| type Apply (FromMaybeSym0 :: TyFun a (Maybe a ~> a) -> Type) (a6989586621679390214 :: a) Source # | |
Defined in Data.Maybe.Singletons type Apply (FromMaybeSym0 :: TyFun a (Maybe a ~> a) -> Type) (a6989586621679390214 :: a) = FromMaybeSym1 a6989586621679390214 | |
data FromMaybeSym1 (a6989586621679390214 :: a) (b :: TyFun (Maybe a) a) Source #
Instances
| SingI1 (FromMaybeSym1 :: a -> TyFun (Maybe a) a -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods liftSing :: forall (x :: a). 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 a6989586621679390214 :: TyFun (Maybe a) a -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (FromMaybeSym1 a6989586621679390214 :: TyFun (Maybe a) a -> Type) (a6989586621679390215 :: Maybe a) Source # | |
Defined in Data.Maybe.Singletons | |
type family FromMaybeSym2 (a6989586621679390214 :: a) (a6989586621679390215 :: Maybe a) :: a where ... Source #
Equations
| FromMaybeSym2 (a6989586621679390214 :: a) (a6989586621679390215 :: Maybe a) = FromMaybe a6989586621679390214 a6989586621679390215 |
data ListToMaybeSym0 (a1 :: TyFun [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 Methods suppressUnusedWarnings :: () # | |
| type Apply (ListToMaybeSym0 :: TyFun [a] (Maybe a) -> Type) (a6989586621679390205 :: [a]) Source # | |
Defined in Data.Maybe.Singletons type Apply (ListToMaybeSym0 :: TyFun [a] (Maybe a) -> Type) (a6989586621679390205 :: [a]) = ListToMaybe a6989586621679390205 | |
type family ListToMaybeSym1 (a6989586621679390205 :: [a]) :: Maybe a where ... Source #
Equations
| ListToMaybeSym1 (a6989586621679390205 :: [a]) = ListToMaybe a6989586621679390205 |
data MaybeToListSym0 (a1 :: TyFun (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 Methods suppressUnusedWarnings :: () # | |
| type Apply (MaybeToListSym0 :: TyFun (Maybe a) [a] -> Type) (a6989586621679390209 :: Maybe a) Source # | |
Defined in Data.Maybe.Singletons type Apply (MaybeToListSym0 :: TyFun (Maybe a) [a] -> Type) (a6989586621679390209 :: Maybe a) = MaybeToList a6989586621679390209 | |
type family MaybeToListSym1 (a6989586621679390209 :: Maybe a) :: [a] where ... Source #
Equations
| MaybeToListSym1 (a6989586621679390209 :: Maybe a) = MaybeToList a6989586621679390209 |
data CatMaybesSym0 (a1 :: TyFun [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 Methods suppressUnusedWarnings :: () # | |
| type Apply (CatMaybesSym0 :: TyFun [Maybe a] [a] -> Type) (a6989586621679390199 :: [Maybe a]) Source # | |
Defined in Data.Maybe.Singletons | |
type family CatMaybesSym1 (a6989586621679390199 :: [Maybe a]) :: [a] where ... Source #
Equations
| CatMaybesSym1 (a6989586621679390199 :: [Maybe a]) = CatMaybes a6989586621679390199 |
data MapMaybeSym0 (a1 :: TyFun (a ~> Maybe b) ([a] ~> [b])) Source #
Instances
| SingI (MapMaybeSym0 :: TyFun (a ~> Maybe b) ([a] ~> [b]) -> Type) Source # | |
Defined in Data.Maybe.Singletons | |
| 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) (a6989586621679390184 :: a ~> Maybe b) Source # | |
Defined in Data.Maybe.Singletons type Apply (MapMaybeSym0 :: TyFun (a ~> Maybe b) ([a] ~> [b]) -> Type) (a6989586621679390184 :: a ~> Maybe b) = MapMaybeSym1 a6989586621679390184 | |
data MapMaybeSym1 (a6989586621679390184 :: a ~> Maybe b) (b1 :: TyFun [a] [b]) Source #
Instances
| SingI1 (MapMaybeSym1 :: (a ~> Maybe b) -> TyFun [a] [b] -> Type) Source # | |
Defined in Data.Maybe.Singletons | |
| SingI d => SingI (MapMaybeSym1 d :: TyFun [a] [b] -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods sing :: Sing (MapMaybeSym1 d) # | |
| SuppressUnusedWarnings (MapMaybeSym1 a6989586621679390184 :: TyFun [a] [b] -> Type) Source # | |
Defined in Data.Maybe.Singletons Methods suppressUnusedWarnings :: () # | |
| type Apply (MapMaybeSym1 a6989586621679390184 :: TyFun [a] [b] -> Type) (a6989586621679390185 :: [a]) Source # | |
Defined in Data.Maybe.Singletons type Apply (MapMaybeSym1 a6989586621679390184 :: TyFun [a] [b] -> Type) (a6989586621679390185 :: [a]) = MapMaybe a6989586621679390184 a6989586621679390185 | |
type family MapMaybeSym2 (a6989586621679390184 :: a ~> Maybe b) (a6989586621679390185 :: [a]) :: [b] where ... Source #
Equations
| MapMaybeSym2 (a6989586621679390184 :: a ~> Maybe b) (a6989586621679390185 :: [a]) = MapMaybe a6989586621679390184 a6989586621679390185 |