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 a), Eq (Union k f as)) => Eq (Union k f ((:) k a as))

Eq (Union k f ([] k))

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

Ord (Union k f ([] k))

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

Show (Union k f ([] k))

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

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

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

Methods

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

Instances

UElem k a ((:) k a as) Z

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

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

Methods

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

Instances

USubset k ([] k) bs ([] Nat)

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

type OpenUnion = Union Identity

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