Copyright | (c) Fumiaki Kinoshita 2015 |
---|---|

License | BSD3 |

Maintainer | Fumiaki Kinoshita <fumiexcel@gmail.com> |

Stability | experimental |

Portability | non-portable |

Safe Haskell | None |

Language | Haskell2010 |

- data Membership xs x
- runMembership :: Membership (y : xs) x -> ((x :~: y) -> r) -> (Membership xs x -> r) -> r
- type (∈) x xs = Member xs x
- class LookupTree (Head (Lookup x xs)) xs x => Member xs x where
- membership :: Membership xs x

- data Expecting a
- data Missing a
- data Ambiguous a
- ord :: Int -> Q Exp
- type (⊆) xs ys = Include ys xs
- type Include ys = Forall (Member ys)
- inclusion :: forall xs ys. Include ys xs => Membership ys :* xs
- shrink :: xs ⊆ ys => (h :* ys) -> h :* xs
- subset :: xs ⊆ ys => Lens' (h :* ys) (h :* xs)
- spread :: xs ⊆ ys => (h :| xs) -> h :| ys
- coinclusion :: (Include ys xs, Generate ys) => Nullable (Membership xs) :* ys
- wrench :: (Generate ys, xs ⊆ ys) => (h :* xs) -> Nullable h :* ys
- retrench :: (Generate ys, xs ⊆ ys) => (h :| ys) -> Nullable ((:|) h) xs
- data Nullable h x
- nullable :: r -> (h x -> r) -> Nullable h x -> r
- mapNullable :: (g x -> h y) -> Nullable g x -> Nullable h y

# Membership

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.

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

membership :: Membership xs x Source

# Inclusion

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

Reify the inclusion of type level sets.

# Inverse

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.

Poly-kinded Maybe

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

Apply a function to its content.