Copyright	(C) 2013 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (eir@cis.upenn.edu)
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.Maybe

Contents

Singletons from Data.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.

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 SFalse :: (~) Bool z False => Sing Bool z STrue :: (~) Bool z True => Sing Bool z
data Sing Ordering where SLT :: (~) Ordering z LT => Sing Ordering z SEQ :: (~) Ordering z EQ => Sing Ordering z SGT :: (~) Ordering z GT => Sing Ordering z
data Sing * where STypeRep :: Typeable * a => Sing * a
data Sing Nat where SNat :: KnownNat n => Sing Nat n
data Sing Symbol where SSym :: KnownSymbol n => Sing Symbol n
data Sing () where STuple0 :: (~) () z () => Sing () z
data Sing [a0] where SNil :: (~) [a] z ([] a) => Sing [a] z SCons :: (~) [a] z ((:) a n n) => Sing a n -> Sing [a] n -> Sing [a] z
data Sing (Maybe a0) where SNothing :: (~) (Maybe a) z (Nothing a) => Sing (Maybe a) z SJust :: (~) (Maybe a) z (Just a n) => Sing a n -> Sing (Maybe a) z
data Sing (Either a0 b0) where SLeft :: (~) (Either a b) z (Left a b n) => Sing a n -> Sing (Either a b) z SRight :: (~) (Either a b) z (Right a b n) => Sing b n -> Sing (Either a b) z
data Sing ((,) a0 b0) where STuple2 :: (~) ((,) a b) z ((,) a b n n) => Sing a n -> Sing b n -> Sing ((,) a b) z
data Sing ((,,) a0 b0 c0) where STuple3 :: (~) ((,,) a b c) z ((,,) a b c n n n) => Sing a n -> Sing b n -> Sing c n -> Sing ((,,) a b c) z
data Sing ((,,,) a0 b0 c0 d0) where STuple4 :: (~) ((,,,) a b c d) z ((,,,) a b c d n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing ((,,,) a b c d) z
data Sing ((,,,,) a0 b0 c0 d0 e0) where STuple5 :: (~) ((,,,,) a b c d e) z ((,,,,) a b c d e n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing ((,,,,) a b c d e) z
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where STuple6 :: (~) ((,,,,,) a b c d e f) z ((,,,,,) a b c d e f n n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing f n -> Sing ((,,,,,) a b c d e f) z
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where STuple7 :: (~) ((,,,,,,) a b c d e f g) z ((,,,,,,) a b c d e f g n n n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing f n -> Sing g n -> 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 z = Sing z Source

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

Singletons from `Data.Maybe`

type family Maybe_ a a a :: b Source

Equations

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

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

Equations

IsJust Nothing = False
IsJust (Just z) = True

sIsJust :: forall t. Sing t -> Sing (IsJust t) Source

type family IsNothing a :: Bool Source

Equations

IsNothing Nothing = True
IsNothing (Just z) = False

sIsNothing :: forall t. Sing t -> Sing (IsNothing t) Source

type family FromJust a :: a Source

Equations

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

sFromJust :: forall t. Sing t -> Sing (FromJust t) Source

type family FromMaybe a a :: a Source

Equations

FromMaybe d Nothing = d
FromMaybe z (Just v) = v

sFromMaybe :: forall t t. Sing t -> Sing t -> Sing (FromMaybe t t) Source

type family MaybeToList a :: [a] Source

Equations

MaybeToList Nothing = `[]`
MaybeToList (Just x) = `[x]`

sMaybeToList :: forall t. Sing t -> Sing (MaybeToList t) Source

type family ListToMaybe a :: Maybe a Source

Equations

ListToMaybe [] = Nothing
ListToMaybe ((:) a z) = Just a

sListToMaybe :: forall t. Sing t -> Sing (ListToMaybe t) Source

type family CatMaybes a :: [a] Source

Equations

CatMaybes [] = `[]`
CatMaybes ((:) (Just x) xs) = (:) x (CatMaybes xs)
CatMaybes ((:) Nothing xs) = CatMaybes xs

sCatMaybes :: forall t. Sing t -> Sing (CatMaybes t) Source

type family MapMaybe a a :: [b] Source

Equations

MapMaybe z [] = `[]`
MapMaybe f ((:) x xs) = (:++) (MaybeToList (f x)) (MapMaybe f xs)

sMapMaybe :: forall t t. (forall t. Sing t -> Sing (t t)) -> Sing t -> Sing (MapMaybe t t) Source

Documentation

Singletons from Data.Maybe

Singletons from `Data.Maybe`