Data.Singletons.Maybe

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.

Documentation

data family Sing a

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

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

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)

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

Equations

IsJust Nothing = False

IsJust (Just z) = True

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

type family IsNothing a :: Bool

Equations

IsNothing Nothing = True

IsNothing (Just z) = False

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

type family FromJust a :: a

Equations

FromJust Nothing = Error "Maybe.fromJust: Nothing"

FromJust (Just x) = x

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

type family FromMaybe a a :: a

Equations

FromMaybe d Nothing = d

FromMaybe z (Just v) = v

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

type family MaybeToList a :: [a]

Equations

MaybeToList Nothing = `[]`

MaybeToList (Just x) = `[x]`

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

type family ListToMaybe a :: Maybe a

Equations

ListToMaybe [] = Nothing

ListToMaybe ((:) a z) = Just a

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

type family CatMaybes a :: [a]

Equations

CatMaybes [] = `[]`

CatMaybes ((:) (Just x) xs) = (:) x (CatMaybes xs)

CatMaybes ((:) Nothing xs) = CatMaybes xs

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

type family MapMaybe a a :: [b]

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)