singletons-2.3.1: A framework for generating singleton types

Copyright(C) 2013-2014 Richard Eisenberg Jan Stolarek
LicenseBSD-style (see LICENSE)
MaintainerRichard Eisenberg (rae@cs.brynmawr.edu)
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Singletons.Prelude.Maybe

Contents

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
data Sing Ordering # 
data Sing * # 
data Sing * where
data Sing Nat # 
data Sing Nat where
data Sing Symbol # 
data Sing Symbol where
data Sing () # 
data Sing () where
data Sing [a] # 
data Sing [a] where
data Sing (Maybe a) # 
data Sing (Maybe a) where
data Sing (NonEmpty a) # 
data Sing (NonEmpty a) where
data Sing (Either a b) # 
data Sing (Either a b) where
data Sing (a, b) # 
data Sing (a, b) where
data Sing ((~>) k1 k2) # 
data Sing ((~>) k1 k2) = SLambda {}
data Sing (a, b, c) # 
data Sing (a, b, c) where
data Sing (a, b, c, d) # 
data Sing (a, b, c, d) where
data Sing (a, b, c, d, e) # 
data Sing (a, b, c, d, e) where
data Sing (a, b, c, d, e, f) # 
data Sing (a, b, c, d, e, f) where
data Sing (a, b, c, d, e, f, g) # 
data Sing (a, b, c, d, e, f, g) where

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_1627823911 Nothing = n 
Maybe_ _z_1627823914 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_1627825123) = 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_1627825116) = 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_1627825103 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_1627825084) = 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_1627825036 '[] = '[] 
MapMaybe f ((:) x xs) = Case_1627825068 f x xs (Let1627825055Scrutinee_1627825025Sym3 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 a822083585 (Maybe a822083585)) #

Instances

SuppressUnusedWarnings (TyFun a822083585 (Maybe a822083585) -> *) (JustSym0 a822083585) # 

Methods

suppressUnusedWarnings :: Proxy (JustSym0 a822083585) t -> () #

type Apply a (Maybe a) (JustSym0 a) l # 
type Apply a (Maybe a) (JustSym0 a) l = Just a l

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

data Maybe_Sym0 (l :: TyFun b1627823889 (TyFun (TyFun a1627823890 b1627823889 -> Type) (TyFun (Maybe a1627823890) b1627823889 -> Type) -> Type)) #

Instances

SuppressUnusedWarnings (TyFun b1627823889 (TyFun (TyFun a1627823890 b1627823889 -> Type) (TyFun (Maybe a1627823890) b1627823889 -> Type) -> Type) -> *) (Maybe_Sym0 a1627823890 b1627823889) # 

Methods

suppressUnusedWarnings :: Proxy (Maybe_Sym0 a1627823890 b1627823889) t -> () #

type Apply b1627823889 (TyFun (TyFun a1627823890 b1627823889 -> Type) (TyFun (Maybe a1627823890) b1627823889 -> Type) -> Type) (Maybe_Sym0 a1627823890 b1627823889) l # 
type Apply b1627823889 (TyFun (TyFun a1627823890 b1627823889 -> Type) (TyFun (Maybe a1627823890) b1627823889 -> Type) -> Type) (Maybe_Sym0 a1627823890 b1627823889) l = Maybe_Sym1 a1627823890 b1627823889 l

data Maybe_Sym1 (l :: b1627823889) (l :: TyFun (TyFun a1627823890 b1627823889 -> Type) (TyFun (Maybe a1627823890) b1627823889 -> Type)) #

Instances

SuppressUnusedWarnings (b1627823889 -> TyFun (TyFun a1627823890 b1627823889 -> Type) (TyFun (Maybe a1627823890) b1627823889 -> Type) -> *) (Maybe_Sym1 a1627823890 b1627823889) # 

Methods

suppressUnusedWarnings :: Proxy (Maybe_Sym1 a1627823890 b1627823889) t -> () #

type Apply (TyFun a1627823890 b1627823889 -> Type) (TyFun (Maybe a1627823890) b1627823889 -> Type) (Maybe_Sym1 a1627823890 b1627823889 l1) l2 # 
type Apply (TyFun a1627823890 b1627823889 -> Type) (TyFun (Maybe a1627823890) b1627823889 -> Type) (Maybe_Sym1 a1627823890 b1627823889 l1) l2 = Maybe_Sym2 a1627823890 b1627823889 l1 l2

data Maybe_Sym2 (l :: b1627823889) (l :: TyFun a1627823890 b1627823889 -> Type) (l :: TyFun (Maybe a1627823890) b1627823889) #

Instances

SuppressUnusedWarnings (b1627823889 -> (TyFun a1627823890 b1627823889 -> Type) -> TyFun (Maybe a1627823890) b1627823889 -> *) (Maybe_Sym2 a1627823890 b1627823889) # 

Methods

suppressUnusedWarnings :: Proxy (Maybe_Sym2 a1627823890 b1627823889) 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 :: b1627823889) (t :: TyFun a1627823890 b1627823889 -> Type) (t :: Maybe a1627823890) = Maybe_ t t t #

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

Instances

SuppressUnusedWarnings (TyFun (Maybe a1627825002) Bool -> *) (IsJustSym0 a1627825002) # 

Methods

suppressUnusedWarnings :: Proxy (IsJustSym0 a1627825002) t -> () #

type Apply (Maybe a) Bool (IsJustSym0 a) l # 
type Apply (Maybe a) Bool (IsJustSym0 a) l = IsJust a l

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

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

Instances

SuppressUnusedWarnings (TyFun (Maybe a1627825001) Bool -> *) (IsNothingSym0 a1627825001) # 

Methods

suppressUnusedWarnings :: Proxy (IsNothingSym0 a1627825001) t -> () #

type Apply (Maybe a) Bool (IsNothingSym0 a) l # 
type Apply (Maybe a) Bool (IsNothingSym0 a) l = IsNothing a l

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

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

Instances

SuppressUnusedWarnings (TyFun (Maybe a1627825000) a1627825000 -> *) (FromJustSym0 a1627825000) # 

Methods

suppressUnusedWarnings :: Proxy (FromJustSym0 a1627825000) t -> () #

type Apply (Maybe a) a (FromJustSym0 a) l # 
type Apply (Maybe a) a (FromJustSym0 a) l = FromJust a l

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

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

Instances

SuppressUnusedWarnings (TyFun a1627824999 (TyFun (Maybe a1627824999) a1627824999 -> Type) -> *) (FromMaybeSym0 a1627824999) # 

Methods

suppressUnusedWarnings :: Proxy (FromMaybeSym0 a1627824999) t -> () #

type Apply a1627824999 (TyFun (Maybe a1627824999) a1627824999 -> Type) (FromMaybeSym0 a1627824999) l # 
type Apply a1627824999 (TyFun (Maybe a1627824999) a1627824999 -> Type) (FromMaybeSym0 a1627824999) l = FromMaybeSym1 a1627824999 l

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

Instances

SuppressUnusedWarnings (a1627824999 -> TyFun (Maybe a1627824999) a1627824999 -> *) (FromMaybeSym1 a1627824999) # 

Methods

suppressUnusedWarnings :: Proxy (FromMaybeSym1 a1627824999) 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 :: a1627824999) (t :: Maybe a1627824999) = FromMaybe t t #

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

Instances

SuppressUnusedWarnings (TyFun [a1627824997] (Maybe a1627824997) -> *) (ListToMaybeSym0 a1627824997) # 

Methods

suppressUnusedWarnings :: Proxy (ListToMaybeSym0 a1627824997) t -> () #

type Apply [a] (Maybe a) (ListToMaybeSym0 a) l # 
type Apply [a] (Maybe a) (ListToMaybeSym0 a) l = ListToMaybe a l

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

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

Instances

SuppressUnusedWarnings (TyFun (Maybe a1627824998) [a1627824998] -> *) (MaybeToListSym0 a1627824998) # 

Methods

suppressUnusedWarnings :: Proxy (MaybeToListSym0 a1627824998) t -> () #

type Apply (Maybe a) [a] (MaybeToListSym0 a) l # 
type Apply (Maybe a) [a] (MaybeToListSym0 a) l = MaybeToList a l

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

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

Instances

SuppressUnusedWarnings (TyFun [Maybe a1627824996] [a1627824996] -> *) (CatMaybesSym0 a1627824996) # 

Methods

suppressUnusedWarnings :: Proxy (CatMaybesSym0 a1627824996) t -> () #

type Apply [Maybe a] [a] (CatMaybesSym0 a) l # 
type Apply [Maybe a] [a] (CatMaybesSym0 a) l = CatMaybes a l

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

data MapMaybeSym0 (l :: TyFun (TyFun a1627824994 (Maybe b1627824995) -> Type) (TyFun [a1627824994] [b1627824995] -> Type)) #

Instances

SuppressUnusedWarnings (TyFun (TyFun a1627824994 (Maybe b1627824995) -> Type) (TyFun [a1627824994] [b1627824995] -> Type) -> *) (MapMaybeSym0 a1627824994 b1627824995) # 

Methods

suppressUnusedWarnings :: Proxy (MapMaybeSym0 a1627824994 b1627824995) t -> () #

type Apply (TyFun a1627824994 (Maybe b1627824995) -> Type) (TyFun [a1627824994] [b1627824995] -> Type) (MapMaybeSym0 a1627824994 b1627824995) l # 
type Apply (TyFun a1627824994 (Maybe b1627824995) -> Type) (TyFun [a1627824994] [b1627824995] -> Type) (MapMaybeSym0 a1627824994 b1627824995) l = MapMaybeSym1 a1627824994 b1627824995 l

data MapMaybeSym1 (l :: TyFun a1627824994 (Maybe b1627824995) -> Type) (l :: TyFun [a1627824994] [b1627824995]) #

Instances

SuppressUnusedWarnings ((TyFun a1627824994 (Maybe b1627824995) -> Type) -> TyFun [a1627824994] [b1627824995] -> *) (MapMaybeSym1 a1627824994 b1627824995) # 

Methods

suppressUnusedWarnings :: Proxy (MapMaybeSym1 a1627824994 b1627824995) 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 a1627824994 (Maybe b1627824995) -> Type) (t :: [a1627824994]) = MapMaybe t t #