Data.OpenUnion1.Clean

Documentation

data family Union s a

Instances

type f |> (Union s) = Union ((:>) (* -> *) f s)

data Union (Empty (* -> *)) = Exhausted (Union (Empty (* -> *)) a)

data Union ((:>) (* -> *) f s)

• = Single (f a)
• | Union (Union s a)

type Nil = Union Empty

An uninhabited union.

data List a

Poly-kinded list

Constructors

Empty

a :> (List a) infixr 5

type family f |> s :: * -> * infixr 5

Append a new element to a union.

Instances

type f |> (Union s) = Union ((:>) (* -> *) f s)

(@>) infixr 0

Arguments

:: (f x -> r)

first case

-> (Union s x -> r)

otherwise

-> Union (f :> s) x -> r

matching function

Perform type-safe matching.

exhaust :: Nil x -> m r

class f ∈ s infix 4

Constraint f ∈ s indicates that f is an element of a type-level list s.

Minimal complete definition

query

Instances

(∈) k f s => (∈) k f ((:>) k g s)

(∈) k f ((:>) k f s)

type Member f s = f ∈ s

liftU :: forall s f a. f ∈ s => f a -> Union s a

Lift some value into a union.

class s ⊆ t where infix 4

Type-level inclusion characterized by reunion.

Methods

reunion :: Union s a -> Union t a

Lift a union into equivalent or larger one, permuting elements if necessary.

Instances

(Empty (* -> *)) ⊆ t

Every set has an empty set as its subset.

((∈) (* -> *) f t, (⊆) s t) => ((:>) (* -> *) f s) ⊆ t

type Include s t = s ⊆ t