Data.Extensible.Inclusion

Membership

data Membership xs x

The position of x in the type level set xs.

Instances

Typeable ([k] -> k -> *) (Membership k)

Eq (Membership k xs x)

Ord (Membership k xs x)

Show (Membership k xs x)

NFData (Membership k xs x)

runMembership :: Membership (y : xs) x -> ((x :~: y) -> r) -> (Membership xs x -> r) -> r

Embodies a type equivalence to ensure that the Membership points the first element.

type (∈) x xs = Member xs x

Unicode flipped alias for Member

class LookupTree (Head (Lookup x xs)) xs x => Member xs x where

Methods

membership :: Membership xs x

Instances

((~) * (Check k1 Nat x (Lookup k1 x xs)) (Expecting k one), ToInt k one, LookupTree k1 (Head Nat (Lookup k1 x xs)) xs x) => Member k xs x

data Expecting a

A type sugar to make type error more readable.

data Missing a

A type sugar to make type error more readable.

data Ambiguous a

A type sugar to make type error more readable.

ord :: Int -> Q Exp

Generates a Membership that corresponds to the given ordinal (0-origin).

Inclusion

type (⊆) xs ys = Include ys xs

Unicode alias for Include

type Include ys = Forall (Member ys)

ys contains xs

inclusion :: forall xs ys. Include ys xs => Membership ys :* xs

Reify the inclusion of type level sets.

shrink :: xs ⊆ ys => (h :* ys) -> h :* xs

O(m log n) Select some elements.

subset :: xs ⊆ ys => Lens' (h :* ys) (h :* xs)

A lens for a subset (inefficient)

spread :: xs ⊆ ys => (h :| xs) -> h :| ys

O(log n) Embed to a larger union.

Inverse

coinclusion :: (Include ys xs, Generate ys) => Nullable (Membership xs) :* ys

The inverse of inclusion.

wrench :: (Generate ys, xs ⊆ ys) => (h :* xs) -> Nullable h :* ys

Extend a product and fill missing fields by Null.

retrench :: (Generate ys, xs ⊆ ys) => (h :| ys) -> Nullable ((:|) h) xs

Narrow the range of the sum, if possible.

data Nullable h x

Poly-kinded Maybe

Constructors

Null

Eine (h x)

Instances

Typeable ((k -> *) -> k -> *) (Nullable k)

Eq (h x) => Eq (Nullable k h x)

Ord (h x) => Ord (Nullable k h x)

Show (h x) => Show (Nullable k h x)

nullable :: r -> (h x -> r) -> Nullable h x -> r

Destruct Nullable.

mapNullable :: (g x -> h y) -> Nullable g x -> Nullable h y

Apply a function to its content.