Copyright	(C) 2013-2014 Richard Eisenberg Jan Stolarek
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (rae@cs.brynmawr.edu)
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.Prelude.Maybe

Contents

Singletons from Data.Maybe
Defunctionalization symbols

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.

Synopsis

Documentation

data family Sing (a :: k) #

The singleton kind-indexed data family.

Instances

data Sing Bool #
data Sing Bool where SFalse :: Sing Bool z STrue :: Sing Bool z
data Sing Ordering #
data Sing Ordering where SLT :: Sing Ordering z SEQ :: Sing Ordering z SGT :: Sing Ordering z
data Sing * #
data Sing * where STypeRep :: Sing * a
data Sing Nat #
data Sing Nat where SNat :: Sing Nat n
data Sing Symbol #
data Sing Symbol where SSym :: Sing Symbol n
data Sing () #
data Sing () where STuple0 :: Sing () z
data Sing [a] #
data Sing [a] where SNil :: Sing [a] z SCons :: Sing [a] z
data Sing (Maybe a) #
data Sing (Maybe a) where SNothing :: Sing (Maybe a) z SJust :: Sing (Maybe a) z
data Sing (NonEmpty a) #
data Sing (NonEmpty a) where (:%\|) :: Sing (NonEmpty a) z
data Sing (Either a b) #
data Sing (Either a b) where SLeft :: Sing (Either a b) z SRight :: Sing (Either a b) z
data Sing (a, b) #
data Sing (a, b) where STuple2 :: Sing (a, b) z
data Sing ((~>) k1 k2) #
data Sing ((~>) k1 k2) = SLambda { applySing :: forall (t :: k1). Sing k1 t -> Sing k2 ((@@) k1 k2 f t) }
data Sing (a, b, c) #
data Sing (a, b, c) where STuple3 :: Sing (a, b, c) z
data Sing (a, b, c, d) #
data Sing (a, b, c, d) where STuple4 :: Sing (a, b, c, d) z
data Sing (a, b, c, d, e) #
data Sing (a, b, c, d, e) where STuple5 :: Sing (a, b, c, d, e) z
data Sing (a, b, c, d, e, f) #
data Sing (a, b, c, d, e, f) where STuple6 :: Sing (a, b, c, d, e, f) z
data Sing (a, b, c, d, e, f, g) #
data Sing (a, b, c, d, e, f, g) where STuple7 :: Sing (a, b, c, d, e, f, g) z

Though Haddock doesn't show it, the Sing instance above declares constructors

SNothing :: Sing Nothing
SJust    :: Sing a -> Sing (Just a)

type SMaybe = (Sing :: Maybe a -> Type) #

SBool is a kind-restricted synonym for Sing: type SMaybe (a :: Maybe k) = Sing a

Singletons from `Data.Maybe`

maybe_ :: b -> (a -> b) -> Maybe a -> b #

type family Maybe_ (a :: b) (a :: TyFun a b -> Type) (a :: Maybe a) :: b where ... #

Equations

Maybe_ n _z_6989586621679443459 Nothing = n
Maybe_ _z_6989586621679443462 f (Just x) = Apply f x

sMaybe_ :: forall (t :: b) (t :: TyFun a b -> Type) (t :: Maybe a). 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.

type family IsJust (a :: Maybe a) :: Bool where ... #

Equations

IsJust Nothing = FalseSym0
IsJust (Just _z_6989586621679444671) = TrueSym0

sIsJust :: forall (t :: Maybe a). Sing t -> Sing (Apply IsJustSym0 t :: Bool) #

type family IsNothing (a :: Maybe a) :: Bool where ... #

Equations

IsNothing Nothing = TrueSym0
IsNothing (Just _z_6989586621679444664) = FalseSym0

sIsNothing :: forall (t :: Maybe a). Sing t -> Sing (Apply IsNothingSym0 t :: Bool) #

type family FromJust (a :: Maybe a) :: a where ... #

Equations

FromJust Nothing = Apply ErrorSym0 "Maybe.fromJust: Nothing"
FromJust (Just x) = x

sFromJust :: forall (t :: Maybe a). Sing t -> Sing (Apply FromJustSym0 t :: a) #

type family FromMaybe (a :: a) (a :: Maybe a) :: a where ... #

Equations

FromMaybe d x = Case_6989586621679444651 d x x

sFromMaybe :: forall (t :: a) (t :: Maybe a). 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_6989586621679444632) = Apply JustSym0 a

sListToMaybe :: forall (t :: [a]). 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 :: Maybe a). Sing t -> Sing (Apply MaybeToListSym0 t :: [a]) #

type family CatMaybes (a :: [Maybe a]) :: [a] where ... #

Equations

CatMaybes '[] = '[]
CatMaybes ((:) (Just x) xs) = Apply (Apply (:$) x) (Apply CatMaybesSym0 xs)
CatMaybes ((:) Nothing xs) = Apply CatMaybesSym0 xs

sCatMaybes :: forall (t :: [Maybe a]). Sing t -> Sing (Apply CatMaybesSym0 t :: [a]) #

type family MapMaybe (a :: TyFun a (Maybe b) -> Type) (a :: [a]) :: [b] where ... #

Equations

MapMaybe _z_6989586621679444584 '[] = '[]
MapMaybe f ((:) x xs) = Case_6989586621679444616 f x xs (Let6989586621679444603Scrutinee_6989586621679444573Sym3 f x xs)

sMapMaybe :: forall (t :: TyFun a (Maybe b) -> Type) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply MapMaybeSym0 t) t :: [b]) #

Defunctionalization symbols

type NothingSym0 = Nothing #

data JustSym0 (l :: TyFun a3530822107858468865 (Maybe a3530822107858468865)) #

Instances

SuppressUnusedWarnings (TyFun a3530822107858468865 (Maybe a3530822107858468865) -> *) (JustSym0 a3530822107858468865) #
Methods suppressUnusedWarnings :: Proxy (JustSym0 a3530822107858468865) t -> () #
type Apply a (Maybe a) (JustSym0 a) l #
type Apply a (Maybe a) (JustSym0 a) l = Just a l

type JustSym1 (t :: a3530822107858468865) = Just t #

data Maybe_Sym0 (l :: TyFun b6989586621679443437 (TyFun (TyFun a6989586621679443438 b6989586621679443437 -> Type) (TyFun (Maybe a6989586621679443438) b6989586621679443437 -> Type) -> Type)) #

Instances

SuppressUnusedWarnings (TyFun b6989586621679443437 (TyFun (TyFun a6989586621679443438 b6989586621679443437 -> Type) (TyFun (Maybe a6989586621679443438) b6989586621679443437 -> Type) -> Type) -> *) (Maybe_Sym0 a6989586621679443438 b6989586621679443437) #
Methods suppressUnusedWarnings :: Proxy (Maybe_Sym0 a6989586621679443438 b6989586621679443437) t -> () #
type Apply b6989586621679443437 (TyFun (TyFun a6989586621679443438 b6989586621679443437 -> Type) (TyFun (Maybe a6989586621679443438) b6989586621679443437 -> Type) -> Type) (Maybe_Sym0 a6989586621679443438 b6989586621679443437) l #
type Apply b6989586621679443437 (TyFun (TyFun a6989586621679443438 b6989586621679443437 -> Type) (TyFun (Maybe a6989586621679443438) b6989586621679443437 -> Type) -> Type) (Maybe_Sym0 a6989586621679443438 b6989586621679443437) l = Maybe_Sym1 a6989586621679443438 b6989586621679443437 l

data Maybe_Sym1 (l :: b6989586621679443437) (l :: TyFun (TyFun a6989586621679443438 b6989586621679443437 -> Type) (TyFun (Maybe a6989586621679443438) b6989586621679443437 -> Type)) #

Instances

SuppressUnusedWarnings (b6989586621679443437 -> TyFun (TyFun a6989586621679443438 b6989586621679443437 -> Type) (TyFun (Maybe a6989586621679443438) b6989586621679443437 -> Type) -> *) (Maybe_Sym1 a6989586621679443438 b6989586621679443437) #
Methods suppressUnusedWarnings :: Proxy (Maybe_Sym1 a6989586621679443438 b6989586621679443437) t -> () #
type Apply (TyFun a6989586621679443438 b6989586621679443437 -> Type) (TyFun (Maybe a6989586621679443438) b6989586621679443437 -> Type) (Maybe_Sym1 a6989586621679443438 b6989586621679443437 l1) l2 #
type Apply (TyFun a6989586621679443438 b6989586621679443437 -> Type) (TyFun (Maybe a6989586621679443438) b6989586621679443437 -> Type) (Maybe_Sym1 a6989586621679443438 b6989586621679443437 l1) l2 = Maybe_Sym2 a6989586621679443438 b6989586621679443437 l1 l2

data Maybe_Sym2 (l :: b6989586621679443437) (l :: TyFun a6989586621679443438 b6989586621679443437 -> Type) (l :: TyFun (Maybe a6989586621679443438) b6989586621679443437) #

Instances

SuppressUnusedWarnings (b6989586621679443437 -> (TyFun a6989586621679443438 b6989586621679443437 -> Type) -> TyFun (Maybe a6989586621679443438) b6989586621679443437 -> *) (Maybe_Sym2 a6989586621679443438 b6989586621679443437) #
Methods suppressUnusedWarnings :: Proxy (Maybe_Sym2 a6989586621679443438 b6989586621679443437) t -> () #
type Apply (Maybe a) b (Maybe_Sym2 a b l1 l2) l3 #
type Apply (Maybe a) b (Maybe_Sym2 a b l1 l2) l3 = Maybe_ a b l1 l2 l3

type Maybe_Sym3 (t :: b6989586621679443437) (t :: TyFun a6989586621679443438 b6989586621679443437 -> Type) (t :: Maybe a6989586621679443438) = Maybe_ t t t #

data IsJustSym0 (l :: TyFun (Maybe a6989586621679444550) Bool) #

Instances

SuppressUnusedWarnings (TyFun (Maybe a6989586621679444550) Bool -> *) (IsJustSym0 a6989586621679444550) #
Methods suppressUnusedWarnings :: Proxy (IsJustSym0 a6989586621679444550) t -> () #
type Apply (Maybe a) Bool (IsJustSym0 a) l #
type Apply (Maybe a) Bool (IsJustSym0 a) l = IsJust a l

type IsJustSym1 (t :: Maybe a6989586621679444550) = IsJust t #

data IsNothingSym0 (l :: TyFun (Maybe a6989586621679444549) Bool) #

Instances

SuppressUnusedWarnings (TyFun (Maybe a6989586621679444549) Bool -> *) (IsNothingSym0 a6989586621679444549) #
Methods suppressUnusedWarnings :: Proxy (IsNothingSym0 a6989586621679444549) t -> () #
type Apply (Maybe a) Bool (IsNothingSym0 a) l #
type Apply (Maybe a) Bool (IsNothingSym0 a) l = IsNothing a l

type IsNothingSym1 (t :: Maybe a6989586621679444549) = IsNothing t #

data FromJustSym0 (l :: TyFun (Maybe a6989586621679444548) a6989586621679444548) #

Instances

SuppressUnusedWarnings (TyFun (Maybe a6989586621679444548) a6989586621679444548 -> *) (FromJustSym0 a6989586621679444548) #
Methods suppressUnusedWarnings :: Proxy (FromJustSym0 a6989586621679444548) t -> () #
type Apply (Maybe a) a (FromJustSym0 a) l #
type Apply (Maybe a) a (FromJustSym0 a) l = FromJust a l

type FromJustSym1 (t :: Maybe a6989586621679444548) = FromJust t #

data FromMaybeSym0 (l :: TyFun a6989586621679444547 (TyFun (Maybe a6989586621679444547) a6989586621679444547 -> Type)) #

Instances

SuppressUnusedWarnings (TyFun a6989586621679444547 (TyFun (Maybe a6989586621679444547) a6989586621679444547 -> Type) -> *) (FromMaybeSym0 a6989586621679444547) #
Methods suppressUnusedWarnings :: Proxy (FromMaybeSym0 a6989586621679444547) t -> () #
type Apply a6989586621679444547 (TyFun (Maybe a6989586621679444547) a6989586621679444547 -> Type) (FromMaybeSym0 a6989586621679444547) l #
type Apply a6989586621679444547 (TyFun (Maybe a6989586621679444547) a6989586621679444547 -> Type) (FromMaybeSym0 a6989586621679444547) l = FromMaybeSym1 a6989586621679444547 l

data FromMaybeSym1 (l :: a6989586621679444547) (l :: TyFun (Maybe a6989586621679444547) a6989586621679444547) #

Instances

SuppressUnusedWarnings (a6989586621679444547 -> TyFun (Maybe a6989586621679444547) a6989586621679444547 -> *) (FromMaybeSym1 a6989586621679444547) #
Methods suppressUnusedWarnings :: Proxy (FromMaybeSym1 a6989586621679444547) t -> () #
type Apply (Maybe a) a (FromMaybeSym1 a l1) l2 #
type Apply (Maybe a) a (FromMaybeSym1 a l1) l2 = FromMaybe a l1 l2

type FromMaybeSym2 (t :: a6989586621679444547) (t :: Maybe a6989586621679444547) = FromMaybe t t #

data ListToMaybeSym0 (l :: TyFun [a6989586621679444545] (Maybe a6989586621679444545)) #

Instances

SuppressUnusedWarnings (TyFun [a6989586621679444545] (Maybe a6989586621679444545) -> *) (ListToMaybeSym0 a6989586621679444545) #
Methods suppressUnusedWarnings :: Proxy (ListToMaybeSym0 a6989586621679444545) t -> () #
type Apply [a] (Maybe a) (ListToMaybeSym0 a) l #
type Apply [a] (Maybe a) (ListToMaybeSym0 a) l = ListToMaybe a l

type ListToMaybeSym1 (t :: [a6989586621679444545]) = ListToMaybe t #

data MaybeToListSym0 (l :: TyFun (Maybe a6989586621679444546) [a6989586621679444546]) #

Instances

SuppressUnusedWarnings (TyFun (Maybe a6989586621679444546) [a6989586621679444546] -> *) (MaybeToListSym0 a6989586621679444546) #
Methods suppressUnusedWarnings :: Proxy (MaybeToListSym0 a6989586621679444546) t -> () #
type Apply (Maybe a) [a] (MaybeToListSym0 a) l #
type Apply (Maybe a) [a] (MaybeToListSym0 a) l = MaybeToList a l

type MaybeToListSym1 (t :: Maybe a6989586621679444546) = MaybeToList t #

data CatMaybesSym0 (l :: TyFun [Maybe a6989586621679444544] [a6989586621679444544]) #

Instances

SuppressUnusedWarnings (TyFun [Maybe a6989586621679444544] [a6989586621679444544] -> *) (CatMaybesSym0 a6989586621679444544) #
Methods suppressUnusedWarnings :: Proxy (CatMaybesSym0 a6989586621679444544) t -> () #
type Apply [Maybe a] [a] (CatMaybesSym0 a) l #
type Apply [Maybe a] [a] (CatMaybesSym0 a) l = CatMaybes a l

type CatMaybesSym1 (t :: [Maybe a6989586621679444544]) = CatMaybes t #

data MapMaybeSym0 (l :: TyFun (TyFun a6989586621679444542 (Maybe b6989586621679444543) -> Type) (TyFun [a6989586621679444542] [b6989586621679444543] -> Type)) #

Instances

SuppressUnusedWarnings (TyFun (TyFun a6989586621679444542 (Maybe b6989586621679444543) -> Type) (TyFun [a6989586621679444542] [b6989586621679444543] -> Type) -> *) (MapMaybeSym0 a6989586621679444542 b6989586621679444543) #
Methods suppressUnusedWarnings :: Proxy (MapMaybeSym0 a6989586621679444542 b6989586621679444543) t -> () #
type Apply (TyFun a6989586621679444542 (Maybe b6989586621679444543) -> Type) (TyFun [a6989586621679444542] [b6989586621679444543] -> Type) (MapMaybeSym0 a6989586621679444542 b6989586621679444543) l #
type Apply (TyFun a6989586621679444542 (Maybe b6989586621679444543) -> Type) (TyFun [a6989586621679444542] [b6989586621679444543] -> Type) (MapMaybeSym0 a6989586621679444542 b6989586621679444543) l = MapMaybeSym1 a6989586621679444542 b6989586621679444543 l

data MapMaybeSym1 (l :: TyFun a6989586621679444542 (Maybe b6989586621679444543) -> Type) (l :: TyFun [a6989586621679444542] [b6989586621679444543]) #

Instances

SuppressUnusedWarnings ((TyFun a6989586621679444542 (Maybe b6989586621679444543) -> Type) -> TyFun [a6989586621679444542] [b6989586621679444543] -> *) (MapMaybeSym1 a6989586621679444542 b6989586621679444543) #
Methods suppressUnusedWarnings :: Proxy (MapMaybeSym1 a6989586621679444542 b6989586621679444543) t -> () #
type Apply [a] [b] (MapMaybeSym1 a b l1) l2 #
type Apply [a] [b] (MapMaybeSym1 a b l1) l2 = MapMaybe a b l1 l2

type MapMaybeSym2 (t :: TyFun a6989586621679444542 (Maybe b6989586621679444543) -> Type) (t :: [a6989586621679444542]) = MapMaybe t t #

Documentation

Singletons from Data.Maybe

Defunctionalization symbols

Singletons from `Data.Maybe`