Copyright | (C) 2013-2014 Richard Eisenberg Jan Stolarek |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Richard Eisenberg (eir@cis.upenn.edu) |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
Data.Singletons.Prelude.Maybe
Description
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.
- data family Sing (a :: k)
- type SMaybe = (Sing :: Maybe a -> Type)
- 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 ...
- sMaybe_ :: forall t t t. 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 t. Sing t -> Sing (Apply IsJustSym0 t :: Bool)
- type family IsNothing (a :: Maybe a) :: Bool where ...
- sIsNothing :: forall t. Sing t -> Sing (Apply IsNothingSym0 t :: Bool)
- type family FromJust (a :: Maybe a) :: a where ...
- sFromJust :: forall t. Sing t -> Sing (Apply FromJustSym0 t :: a)
- type family FromMaybe (a :: a) (a :: Maybe a) :: a where ...
- sFromMaybe :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply FromMaybeSym0 t) t :: a)
- type family ListToMaybe (a :: [a]) :: Maybe a where ...
- sListToMaybe :: forall t. Sing t -> Sing (Apply ListToMaybeSym0 t :: Maybe a)
- type family MaybeToList (a :: Maybe a) :: [a] where ...
- sMaybeToList :: forall t. Sing t -> Sing (Apply MaybeToListSym0 t :: [a])
- type family CatMaybes (a :: [Maybe a]) :: [a] where ...
- sCatMaybes :: forall t. Sing t -> Sing (Apply CatMaybesSym0 t :: [a])
- type family MapMaybe (a :: TyFun a (Maybe b) -> Type) (a :: [a]) :: [b] where ...
- sMapMaybe :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply MapMaybeSym0 t) t :: [b])
- type NothingSym0 = Nothing
- data JustSym0 l
- type JustSym1 t = Just t
- data Maybe_Sym0 l
- data Maybe_Sym1 l l
- data Maybe_Sym2 l l l
- type Maybe_Sym3 t t t = Maybe_ t t t
- data IsJustSym0 l
- type IsJustSym1 t = IsJust t
- data IsNothingSym0 l
- type IsNothingSym1 t = IsNothing t
- data FromJustSym0 l
- type FromJustSym1 t = FromJust t
- data FromMaybeSym0 l
- data FromMaybeSym1 l l
- type FromMaybeSym2 t t = FromMaybe t t
- data ListToMaybeSym0 l
- type ListToMaybeSym1 t = ListToMaybe t
- data MaybeToListSym0 l
- type MaybeToListSym1 t = MaybeToList t
- data CatMaybesSym0 l
- type CatMaybesSym1 t = CatMaybes t
- data MapMaybeSym0 l
- data MapMaybeSym1 l l
- type MapMaybeSym2 t t = MapMaybe t t
Documentation
The singleton kind-indexed data family.
Instances
data Sing Bool # | |
data Sing Ordering # | |
data Sing * # | |
data Sing Nat # | |
data Sing Symbol # | |
data Sing () # | |
data Sing [a0] # | |
data Sing (Maybe a0) # | |
data Sing (NonEmpty a0) # | |
data Sing (Either a0 b0) # | |
data Sing (a0, b0) # | |
data Sing ((~>) k1 k2) # | |
data Sing (a0, b0, c0) # | |
data Sing (a0, b0, c0, d0) # | |
data Sing (a0, b0, c0, d0, e0) # | |
data Sing (a0, b0, c0, d0, e0, f0) # | |
data Sing (a0, b0, c0, d0, e0, f0, g0) # | |
Though Haddock doesn't show it, the Sing
instance above declares
constructors
SNothing :: Sing Nothing SJust :: Sing a -> Sing (Just a)
Singletons from Data.Maybe
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
.
sIsNothing :: forall t. Sing t -> Sing (Apply IsNothingSym0 t :: Bool) #
type family FromMaybe (a :: a) (a :: Maybe a) :: a where ... #
Equations
FromMaybe d x = Case_6989586621679970459 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_6989586621679970440) = 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]) #
sCatMaybes :: forall t. Sing t -> Sing (Apply CatMaybesSym0 t :: [a]) #
Defunctionalization symbols
type NothingSym0 = Nothing #
data Maybe_Sym0 l #
Instances
SuppressUnusedWarnings (TyFun b6989586621679969104 (TyFun (TyFun a6989586621679969105 b6989586621679969104 -> Type) (TyFun (Maybe a6989586621679969105) b6989586621679969104 -> Type) -> Type) -> *) (Maybe_Sym0 a6989586621679969105 b6989586621679969104) # | |
type Apply b6989586621679969104 (TyFun (TyFun a6989586621679969105 b6989586621679969104 -> Type) (TyFun (Maybe a6989586621679969105) b6989586621679969104 -> Type) -> Type) (Maybe_Sym0 a6989586621679969105 b6989586621679969104) l0 # | |
data Maybe_Sym1 l l #
Instances
SuppressUnusedWarnings (b6989586621679969104 -> TyFun (TyFun a6989586621679969105 b6989586621679969104 -> Type) (TyFun (Maybe a6989586621679969105) b6989586621679969104 -> Type) -> *) (Maybe_Sym1 a6989586621679969105 b6989586621679969104) # | |
type Apply (TyFun a6989586621679969105 b6989586621679969104 -> Type) (TyFun (Maybe a6989586621679969105) b6989586621679969104 -> Type) (Maybe_Sym1 a6989586621679969105 b6989586621679969104 l0) l1 # | |
data Maybe_Sym2 l l l #
Instances
SuppressUnusedWarnings (b6989586621679969104 -> (TyFun a6989586621679969105 b6989586621679969104 -> Type) -> TyFun (Maybe a6989586621679969105) b6989586621679969104 -> *) (Maybe_Sym2 a6989586621679969105 b6989586621679969104) # | |
type Apply (Maybe a6989586621679969105) b6989586621679969104 (Maybe_Sym2 a6989586621679969105 b6989586621679969104 l1 l0) l2 # | |
type Maybe_Sym3 t t t = Maybe_ t t t #
data IsJustSym0 l #
Instances
SuppressUnusedWarnings (TyFun (Maybe a6989586621679970358) Bool -> *) (IsJustSym0 a6989586621679970358) # | |
type Apply (Maybe a6989586621679970358) Bool (IsJustSym0 a6989586621679970358) l0 # | |
type IsJustSym1 t = IsJust t #
data IsNothingSym0 l #
Instances
SuppressUnusedWarnings (TyFun (Maybe a6989586621679970357) Bool -> *) (IsNothingSym0 a6989586621679970357) # | |
type Apply (Maybe a6989586621679970357) Bool (IsNothingSym0 a6989586621679970357) l0 # | |
type IsNothingSym1 t = IsNothing t #
data FromJustSym0 l #
Instances
SuppressUnusedWarnings (TyFun (Maybe a6989586621679970356) a6989586621679970356 -> *) (FromJustSym0 a6989586621679970356) # | |
type Apply (Maybe a6989586621679970356) a6989586621679970356 (FromJustSym0 a6989586621679970356) l0 # | |
type FromJustSym1 t = FromJust t #
data FromMaybeSym0 l #
Instances
SuppressUnusedWarnings (TyFun a6989586621679970355 (TyFun (Maybe a6989586621679970355) a6989586621679970355 -> Type) -> *) (FromMaybeSym0 a6989586621679970355) # | |
type Apply a6989586621679970355 (TyFun (Maybe a6989586621679970355) a6989586621679970355 -> Type) (FromMaybeSym0 a6989586621679970355) l0 # | |
data FromMaybeSym1 l l #
Instances
SuppressUnusedWarnings (a6989586621679970355 -> TyFun (Maybe a6989586621679970355) a6989586621679970355 -> *) (FromMaybeSym1 a6989586621679970355) # | |
type Apply (Maybe a6989586621679970355) a6989586621679970355 (FromMaybeSym1 a6989586621679970355 l0) l1 # | |
type FromMaybeSym2 t t = FromMaybe t t #
data ListToMaybeSym0 l #
Instances
SuppressUnusedWarnings (TyFun [a6989586621679970353] (Maybe a6989586621679970353) -> *) (ListToMaybeSym0 a6989586621679970353) # | |
type Apply [a6989586621679970353] (Maybe a6989586621679970353) (ListToMaybeSym0 a6989586621679970353) l0 # | |
type ListToMaybeSym1 t = ListToMaybe t #
data MaybeToListSym0 l #
Instances
SuppressUnusedWarnings (TyFun (Maybe a6989586621679970354) [a6989586621679970354] -> *) (MaybeToListSym0 a6989586621679970354) # | |
type Apply (Maybe a6989586621679970354) [a6989586621679970354] (MaybeToListSym0 a6989586621679970354) l0 # | |
type MaybeToListSym1 t = MaybeToList t #
data CatMaybesSym0 l #
Instances
SuppressUnusedWarnings (TyFun [Maybe a6989586621679970352] [a6989586621679970352] -> *) (CatMaybesSym0 a6989586621679970352) # | |
type Apply [Maybe a6989586621679970352] [a6989586621679970352] (CatMaybesSym0 a6989586621679970352) l0 # | |
type CatMaybesSym1 t = CatMaybes t #
data MapMaybeSym0 l #
Instances
SuppressUnusedWarnings (TyFun (TyFun a6989586621679970350 (Maybe b6989586621679970351) -> Type) (TyFun [a6989586621679970350] [b6989586621679970351] -> Type) -> *) (MapMaybeSym0 a6989586621679970350 b6989586621679970351) # | |
type Apply (TyFun a6989586621679970350 (Maybe b6989586621679970351) -> Type) (TyFun [a6989586621679970350] [b6989586621679970351] -> Type) (MapMaybeSym0 a6989586621679970350 b6989586621679970351) l0 # | |
data MapMaybeSym1 l l #
Instances
SuppressUnusedWarnings ((TyFun a6989586621679970350 (Maybe b6989586621679970351) -> Type) -> TyFun [a6989586621679970350] [b6989586621679970351] -> *) (MapMaybeSym1 a6989586621679970350 b6989586621679970351) # | |
type Apply [a6989586621679970350] [b6989586621679970351] (MapMaybeSym1 a6989586621679970350 b6989586621679970351 l0) l1 # | |
type MapMaybeSym2 t t = MapMaybe t t #