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)

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 Member xs x where

Methods

membership :: Membership xs x

Instances

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

remember :: forall xs x r. Membership xs x -> (Member xs x => r) -> r

Remember that Member xs x from Membership.

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).

data Assoc k v

The kind of key-value pairs

Constructors

k :> v

Instances

Associate k k1 k2 v xs => Associated (Assoc k k) xs ((:>) k k k v)

class Associate k v xs | k xs -> v where

Associate k v xs is essentially identical to (k :> v) ∈ xs , but the type v is inferred from k and xs.

Methods

association :: Membership xs (k :> v)

Instances

((~) * (Check k Nat k2 (Lookup k k2 (AssocKeys k k1 xs))) (Expecting Nat one), ToInt Nat one, (~) (Assoc k k1) ((:>) k k1 k2 v) (ListIndex (Assoc k k1) one xs)) => Associate k k k v xs

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.

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

O(log n) Embed to a larger union.

Dictionary-like

type IncludeAssoc ys xs = Forall (Associated ys) xs

Similar to Include, but works nicely for key-value pairs.

class Associated xs t

Minimal complete definition

getAssociation

Instances

Associate k k1 k2 v xs => Associated (Assoc k k) xs ((:>) k k k v)

inclusionAssoc :: forall xs ys. IncludeAssoc ys xs => Membership ys :* xs

Reify the inclusion of type level sets.

shrinkAssoc :: IncludeAssoc ys xs => (h :* ys) -> h :* xs

O(m log n) Select some elements.

spreadAssoc :: IncludeAssoc ys xs => (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.