singletons-1.0: A framework for generating singleton types

Copyright(C) 2013-2014 Richard Eisenberg, Jan Stolarek
LicenseBSD-style (see LICENSE)
MaintainerRichard Eisenberg (eir@cis.upenn.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 Source

The singleton kind-indexed data family.

Instances

TestCoercion * (Sing *) 
SDecide k (KProxy k) => TestEquality k (Sing k) 
data Sing Bool where 
data Sing Ordering where 
data Sing * where 
data Sing Nat where 
data Sing Symbol where 
data Sing () where 
data Sing [a0] where 
data Sing (Maybe a0) where 
data Sing (TyFun k1 k2 -> *) = SLambda {} 
data Sing (Either a0 b0) where 
data Sing ((,) a0 b0) where 
data Sing ((,,) a0 b0 c0) where 
data Sing ((,,,) a0 b0 c0 d0) where 
data Sing ((,,,,) a0 b0 c0 d0 e0) where 
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where 
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where 

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

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

type SMaybe z = Sing z Source

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

Singletons from Data.Maybe

maybe_ :: forall b a. b -> (a -> b) -> Maybe a -> b Source

type family Maybe_ a a a :: b Source

Equations

Maybe_ n z Nothing = n 
Maybe_ z f (Just x) = Apply f x 

sMaybe_ :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Maybe_Sym0 t) t) t) 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.

type family IsJust a :: Bool Source

sIsJust :: forall t. Sing t -> Sing (Apply IsJustSym0 t) Source

type family IsNothing a :: Bool Source

type family FromJust a :: a Source

Equations

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

sFromJust :: forall t. Sing t -> Sing (Apply FromJustSym0 t) Source

type family FromMaybe a a :: a Source

Equations

FromMaybe d x = Case_1628117042 d x (Let_1628117033Scrutinee_1628116954Sym2 d x) 

sFromMaybe :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply FromMaybeSym0 t) t) Source

type family ListToMaybe a :: Maybe a Source

Equations

ListToMaybe [] = NothingSym0 
ListToMaybe ((:) a z) = Apply JustSym0 a 

type family MaybeToList a :: [] a Source

Equations

MaybeToList Nothing = [] 
MaybeToList (Just x) = Apply (Apply (:$) x) [] 

type family CatMaybes a :: [] a Source

Equations

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

type family MapMaybe a a :: [] b Source

Equations

MapMaybe z [] = [] 
MapMaybe f ((:) x xs) = Case_1628116999 f x xs (Let_1628116985Scrutinee_1628116956Sym3 f x xs) 

sMapMaybe :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply MapMaybeSym0 t) t) Source

Defunctionalization symbols

data JustSym0 l Source

Instances

SuppressUnusedWarnings (TyFun k (Maybe k) -> *) (JustSym0 k) 
type Apply (Maybe k) k (JustSym0 k) l0 = JustSym1 k l0 

type JustSym1 t = Just t Source

data Maybe_Sym0 l Source

Instances

SuppressUnusedWarnings (TyFun k (TyFun (TyFun k k -> *) (TyFun (Maybe k) k -> *) -> *) -> *) (Maybe_Sym0 k k) 
type Apply (TyFun (TyFun k1 k -> *) (TyFun (Maybe k1) k -> *) -> *) k (Maybe_Sym0 k1 k) l0 = Maybe_Sym1 k k1 l0 

data Maybe_Sym1 l l Source

Instances

SuppressUnusedWarnings (k -> TyFun (TyFun k k -> *) (TyFun (Maybe k) k -> *) -> *) (Maybe_Sym1 k k) 
type Apply (TyFun (Maybe k) k1 -> *) (TyFun k k1 -> *) (Maybe_Sym1 k1 k l1) l0 = Maybe_Sym2 k1 k l1 l0 

data Maybe_Sym2 l l l Source

Instances

SuppressUnusedWarnings (k -> (TyFun k k -> *) -> TyFun (Maybe k) k -> *) (Maybe_Sym2 k k) 
type Apply k (Maybe k1) (Maybe_Sym2 k k1 l1 l2) l0 = Maybe_Sym3 k k1 l1 l2 l0 

type Maybe_Sym3 t t t = Maybe_ t t t Source

data IsJustSym0 l Source

Instances

data FromJustSym0 l Source

Instances

SuppressUnusedWarnings (TyFun (Maybe k) k -> *) (FromJustSym0 k) 
type Apply k (Maybe k) (FromJustSym0 k) l0 = FromJustSym1 k l0 

data FromMaybeSym0 l Source

Instances

SuppressUnusedWarnings (TyFun k (TyFun (Maybe k) k -> *) -> *) (FromMaybeSym0 k) 
type Apply (TyFun (Maybe k) k -> *) k (FromMaybeSym0 k) l0 = FromMaybeSym1 k l0 

data FromMaybeSym1 l l Source

Instances

SuppressUnusedWarnings (k -> TyFun (Maybe k) k -> *) (FromMaybeSym1 k) 
type Apply k (Maybe k) (FromMaybeSym1 k l1) l0 = FromMaybeSym2 k l1 l0 

data ListToMaybeSym0 l Source

Instances

data MaybeToListSym0 l Source

Instances

data CatMaybesSym0 l Source

Instances

SuppressUnusedWarnings (TyFun [Maybe k] [k] -> *) (CatMaybesSym0 k) 
type Apply [k] [Maybe k] (CatMaybesSym0 k) l0 = CatMaybesSym1 k l0 

data MapMaybeSym0 l Source

Instances

SuppressUnusedWarnings (TyFun (TyFun k (Maybe k) -> *) (TyFun [k] [k] -> *) -> *) (MapMaybeSym0 k k) 
type Apply (TyFun [k1] [k] -> *) (TyFun k1 (Maybe k) -> *) (MapMaybeSym0 k k1) l0 = MapMaybeSym1 k k1 l0 

data MapMaybeSym1 l l Source

Instances

SuppressUnusedWarnings ((TyFun k (Maybe k) -> *) -> TyFun [k] [k] -> *) (MapMaybeSym1 k k) 
type Apply [k] [k1] (MapMaybeSym1 k k1 l1) l0 = MapMaybeSym2 k k1 l1 l0