Data.Union

Extensible type-safe unions.

Documentation

data Union f as where

A union is parameterized by a universe u, an interpretation f and a list of labels as. The labels of the union are given by inhabitants of the kind u; the type of values at any label a :: u is given by its interpretation f a :: *.

Constructors

This :: !(f a) -> Union f (a ': as)

That :: !(Union f as) -> Union f (a ': as)

Instances

(Eq (f a1), Eq (Union a f as)) => Eq (Union a f ((:) a a1 as))

Methods

(==) :: Union a f ((a ': a1) as) -> Union a f ((a ': a1) as) -> Bool

(/=) :: Union a f ((a ': a1) as) -> Union a f ((a ': a1) as) -> Bool

Eq (Union u f ([] u))

Methods

(==) :: Union u f [u] -> Union u f [u] -> Bool

(/=) :: Union u f [u] -> Union u f [u] -> Bool

(Ord (f a1), Ord (Union a f as)) => Ord (Union a f ((:) a a1 as))

Methods

compare :: Union a f ((a ': a1) as) -> Union a f ((a ': a1) as) -> Ordering

(<) :: Union a f ((a ': a1) as) -> Union a f ((a ': a1) as) -> Bool

(<=) :: Union a f ((a ': a1) as) -> Union a f ((a ': a1) as) -> Bool

(>) :: Union a f ((a ': a1) as) -> Union a f ((a ': a1) as) -> Bool

(>=) :: Union a f ((a ': a1) as) -> Union a f ((a ': a1) as) -> Bool

max :: Union a f ((a ': a1) as) -> Union a f ((a ': a1) as) -> Union a f ((a ': a1) as)

min :: Union a f ((a ': a1) as) -> Union a f ((a ': a1) as) -> Union a f ((a ': a1) as)

Ord (Union u f ([] u))

Methods

compare :: Union u f [u] -> Union u f [u] -> Ordering

(<) :: Union u f [u] -> Union u f [u] -> Bool

(<=) :: Union u f [u] -> Union u f [u] -> Bool

(>) :: Union u f [u] -> Union u f [u] -> Bool

(>=) :: Union u f [u] -> Union u f [u] -> Bool

max :: Union u f [u] -> Union u f [u] -> Union u f [u]

min :: Union u f [u] -> Union u f [u] -> Union u f [u]

(Show (f a1), Show (Union a f as)) => Show (Union a f ((:) a a1 as))

Methods

showsPrec :: Int -> Union a f ((a ': a1) as) -> ShowS

show :: Union a f ((a ': a1) as) -> String

showList :: [Union a f ((a ': a1) as)] -> ShowS

Show (Union u f ([] u))

Methods

showsPrec :: Int -> Union u f [u] -> ShowS

show :: Union u f [u] -> String

showList :: [Union u f [u]] -> ShowS

((~) (* -> *) f Identity, Exception a, Typeable [*] as, Exception (Union * f as)) => Exception (Union * f ((:) * a as))

Methods

toException :: Union * f ((* ': a) as) -> SomeException

fromException :: SomeException -> Maybe (Union * f ((* ': a) as))

displayException :: Union * f ((* ': a) as) -> String

(~) (* -> *) f Identity => Exception (Union * f ([] *))

Methods

toException :: Union * f [*] -> SomeException

fromException :: SomeException -> Maybe (Union * f [*])

displayException :: Union * f [*] -> String

(NFData (f a1), NFData (Union a f as)) => NFData (Union a f ((:) a a1 as))

Methods

rnf :: Union a f ((a ': a1) as) -> ()

NFData (Union u f ([] u))

Methods

rnf :: Union u f [u] -> ()

union :: (Union f as -> c) -> (f a -> c) -> Union f (a ': as) -> c

Case analysis for unions.

absurdUnion :: Union f '[] -> a

Since a union with an empty list of labels is uninhabited, we can recover any type from it.

umap :: (forall a. f a -> g a) -> Union f as -> Union g as

_This :: Prism (Union f (a ': as)) (Union f (b ': as)) (f a) (f b)

_That :: Prism (Union f (a ': as)) (Union f (a ': bs)) (Union f as) (Union f bs)

class i ~ RIndex a as => UElem a as i where

Minimal complete definition

uprism | ulift, umatch

Methods

uprism :: Prism' (Union f as) (f a)

ulift :: f a -> Union f as

umatch :: Union f as -> Maybe (f a)

Instances

UElem a a1 ((:) a a1 as) Z

Methods

uprism :: (Choice p, Applicative f) => p (f ((a ': a1) as)) (f (f ((a ': a1) as))) -> p (Union a1 f Z) (f (Union a1 f Z))

ulift :: f ((a ': a1) as) -> Union a1 f Z

umatch :: Union a1 f Z -> Maybe (f ((a ': a1) as))

((~) Nat (RIndex a a1 ((:) a b as)) (S i), UElem a a1 as i) => UElem a a1 ((:) a b as) (S i)

Methods

uprism :: (Choice p, Applicative f) => p (f ((a ': b) as)) (f (f ((a ': b) as))) -> p (Union a1 f (S i)) (f (Union a1 f (S i)))

ulift :: f ((a ': b) as) -> Union a1 f (S i)

umatch :: Union a1 f (S i) -> Maybe (f ((a ': b) as))

class is ~ RImage as bs => USubset as bs is where

Minimal complete definition

usubset | urelax, urestrict

Methods

usubset :: Prism' (Union f bs) (Union f as)

urelax :: Union f as -> Union f bs

urestrict :: Union f bs -> Maybe (Union f as)

Instances

USubset u ([] u) bs ([] Nat)

Methods

usubset :: (Choice p, Applicative f) => p (Union [u] f bs) (f (Union [u] f bs)) -> p (Union [u] f [Nat]) (f (Union [u] f [Nat]))

urelax :: Union [u] f bs -> Union [u] f [Nat]

urestrict :: Union [u] f [Nat] -> Maybe (Union [u] f bs)

(UElem u a bs i, USubset u as bs is) => USubset u ((:) u a as) bs ((:) Nat i is)

Methods

usubset :: (Choice p, Applicative f) => p (Union ((u ': a) as) f bs) (f (Union ((u ': a) as) f bs)) -> p (Union ((u ': a) as) f ((Nat ': i) is)) (f (Union ((u ': a) as) f ((Nat ': i) is)))

urelax :: Union ((u ': a) as) f bs -> Union ((u ': a) as) f ((Nat ': i) is)

urestrict :: Union ((u ': a) as) f ((Nat ': i) is) -> Maybe (Union ((u ': a) as) f bs)

type OpenUnion = Union Identity

openUnion :: forall a as. UElem a as (RIndex a as) => Prism' (OpenUnion as) a