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_6989586621679677502 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_6989586621679677483) = 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 b6989586621679676147 (TyFun (TyFun a6989586621679676148 b6989586621679676147 -> Type) (TyFun (Maybe a6989586621679676148) b6989586621679676147 -> Type) -> Type) -> *) (Maybe_Sym0 a6989586621679676148 b6989586621679676147) # | |
type Apply b6989586621679676147 (TyFun (TyFun a6989586621679676148 b6989586621679676147 -> Type) (TyFun (Maybe a6989586621679676148) b6989586621679676147 -> Type) -> Type) (Maybe_Sym0 a6989586621679676148 b6989586621679676147) l0 # | |
data Maybe_Sym1 l l #
Instances
SuppressUnusedWarnings (b6989586621679676147 -> TyFun (TyFun a6989586621679676148 b6989586621679676147 -> Type) (TyFun (Maybe a6989586621679676148) b6989586621679676147 -> Type) -> *) (Maybe_Sym1 a6989586621679676148 b6989586621679676147) # | |
type Apply (TyFun a6989586621679676148 b6989586621679676147 -> Type) (TyFun (Maybe a6989586621679676148) b6989586621679676147 -> Type) (Maybe_Sym1 a6989586621679676148 b6989586621679676147 l0) l1 # | |
data Maybe_Sym2 l l l #
Instances
SuppressUnusedWarnings (b6989586621679676147 -> (TyFun a6989586621679676148 b6989586621679676147 -> Type) -> TyFun (Maybe a6989586621679676148) b6989586621679676147 -> *) (Maybe_Sym2 a6989586621679676148 b6989586621679676147) # | |
type Apply (Maybe a6989586621679676148) b6989586621679676147 (Maybe_Sym2 a6989586621679676148 b6989586621679676147 l1 l0) l2 # | |
type Maybe_Sym3 t t t = Maybe_ t t t #
data IsJustSym0 l #
Instances
SuppressUnusedWarnings (TyFun (Maybe a6989586621679677401) Bool -> *) (IsJustSym0 a6989586621679677401) # | |
type Apply (Maybe a6989586621679677401) Bool (IsJustSym0 a6989586621679677401) l0 # | |
type IsJustSym1 t = IsJust t #
data IsNothingSym0 l #
Instances
SuppressUnusedWarnings (TyFun (Maybe a6989586621679677400) Bool -> *) (IsNothingSym0 a6989586621679677400) # | |
type Apply (Maybe a6989586621679677400) Bool (IsNothingSym0 a6989586621679677400) l0 # | |
type IsNothingSym1 t = IsNothing t #
data FromJustSym0 l #
Instances
SuppressUnusedWarnings (TyFun (Maybe a6989586621679677399) a6989586621679677399 -> *) (FromJustSym0 a6989586621679677399) # | |
type Apply (Maybe a6989586621679677399) a6989586621679677399 (FromJustSym0 a6989586621679677399) l0 # | |
type FromJustSym1 t = FromJust t #
data FromMaybeSym0 l #
Instances
SuppressUnusedWarnings (TyFun a6989586621679677398 (TyFun (Maybe a6989586621679677398) a6989586621679677398 -> Type) -> *) (FromMaybeSym0 a6989586621679677398) # | |
type Apply a6989586621679677398 (TyFun (Maybe a6989586621679677398) a6989586621679677398 -> Type) (FromMaybeSym0 a6989586621679677398) l0 # | |
data FromMaybeSym1 l l #
Instances
SuppressUnusedWarnings (a6989586621679677398 -> TyFun (Maybe a6989586621679677398) a6989586621679677398 -> *) (FromMaybeSym1 a6989586621679677398) # | |
type Apply (Maybe a6989586621679677398) a6989586621679677398 (FromMaybeSym1 a6989586621679677398 l0) l1 # | |
type FromMaybeSym2 t t = FromMaybe t t #
data ListToMaybeSym0 l #
Instances
SuppressUnusedWarnings (TyFun [a6989586621679677396] (Maybe a6989586621679677396) -> *) (ListToMaybeSym0 a6989586621679677396) # | |
type Apply [a6989586621679677396] (Maybe a6989586621679677396) (ListToMaybeSym0 a6989586621679677396) l0 # | |
type ListToMaybeSym1 t = ListToMaybe t #
data MaybeToListSym0 l #
Instances
SuppressUnusedWarnings (TyFun (Maybe a6989586621679677397) [a6989586621679677397] -> *) (MaybeToListSym0 a6989586621679677397) # | |
type Apply (Maybe a6989586621679677397) [a6989586621679677397] (MaybeToListSym0 a6989586621679677397) l0 # | |
type MaybeToListSym1 t = MaybeToList t #
data CatMaybesSym0 l #
Instances
SuppressUnusedWarnings (TyFun [Maybe a6989586621679677395] [a6989586621679677395] -> *) (CatMaybesSym0 a6989586621679677395) # | |
type Apply [Maybe a6989586621679677395] [a6989586621679677395] (CatMaybesSym0 a6989586621679677395) l0 # | |
type CatMaybesSym1 t = CatMaybes t #
data MapMaybeSym0 l #
Instances
SuppressUnusedWarnings (TyFun (TyFun a6989586621679677393 (Maybe b6989586621679677394) -> Type) (TyFun [a6989586621679677393] [b6989586621679677394] -> Type) -> *) (MapMaybeSym0 a6989586621679677393 b6989586621679677394) # | |
type Apply (TyFun a6989586621679677393 (Maybe b6989586621679677394) -> Type) (TyFun [a6989586621679677393] [b6989586621679677394] -> Type) (MapMaybeSym0 a6989586621679677393 b6989586621679677394) l0 # | |
data MapMaybeSym1 l l #
Instances
SuppressUnusedWarnings ((TyFun a6989586621679677393 (Maybe b6989586621679677394) -> Type) -> TyFun [a6989586621679677393] [b6989586621679677394] -> *) (MapMaybeSym1 a6989586621679677393 b6989586621679677394) # | |
type Apply [a6989586621679677393] [b6989586621679677394] (MapMaybeSym1 a6989586621679677393 b6989586621679677394 l0) l1 # | |
type MapMaybeSym2 t t = MapMaybe t t #