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

License | BSD3 |

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

Safe Haskell | None |

Language | Haskell2010 |

## Synopsis

- data (xs :: [k]) :/ (h :: k -> Type) where
- EmbedAt :: !(Membership xs x) -> h x -> xs :/ h

- hoist :: (forall x. g x -> h x) -> (xs :/ g) -> xs :/ h
- embed :: x ∈ xs => h x -> xs :/ h
- strike :: forall h x xs. x ∈ xs => (xs :/ h) -> Maybe (h x)
- strikeAt :: forall h x xs. Membership xs x -> (xs :/ h) -> Maybe (h x)
- (<:|) :: (h x -> r) -> ((xs :/ h) -> r) -> ((x ': xs) :/ h) -> r
- exhaust :: ('[] :/ h) -> r
- embedAssoc :: Lookup xs k a => h (k :> a) -> xs :/ h

# Documentation

data (xs :: [k]) :/ (h :: k -> Type) where Source #

The extensible sum type

(:/) :: [k] -> (k -> Type) -> Type

EmbedAt :: !(Membership xs x) -> h x -> xs :/ h |

## Instances

strike :: forall h x xs. x ∈ xs => (xs :/ h) -> Maybe (h x) Source #

Try to extract something you want.

strikeAt :: forall h x xs. Membership xs x -> (xs :/ h) -> Maybe (h x) Source #

Try to extract something you want.