extensible-0.3: Extensible, efficient, lens-friendly data types

Copyright(c) Fumiaki Kinoshita 2015
MaintainerFumiaki Kinoshita <fumiexcel@gmail.com>
Safe HaskellNone







data Membership xs x Source

The position of x in the type level set xs.


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 Source

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

type (∈) x xs = Member xs x Source

Unicode flipped alias for Member

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


((~) * (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 Source

A type sugar to make type error more readable.

data Missing a Source

A type sugar to make type error more readable.

data Ambiguous a Source

A type sugar to make type error more readable.

ord :: Int -> Q Exp Source

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


type (⊆) xs ys = Include ys xs Source

Unicode alias for Include

type Include ys = Forall (Member ys) Source

ys contains xs

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

Reify the inclusion of type level sets.

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

O(m log n) Select some elements.

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

A lens for a subset (inefficient)

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

O(log n) Embed to a larger union.


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

The inverse of inclusion.

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

Extend a product and fill missing fields by Null.

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

Narrow the range of the sum, if possible.

data Nullable h x Source

Poly-kinded Maybe


Eine (h x) 


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 Source

Destruct Nullable.

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

Apply a function to its content.