Portability | GHC |
---|---|

Stability | experimental |

Maintainer | emw4@rice.edu |

Proofs regarding membership of a type in a type list.

- data Member ctx a where
- Member_Base :: Member (ctx :> a) a
- Member_Step :: Member ctx a -> Member (ctx :> b) a

- toEq :: Member (Nil :> a) b -> b :=: a
- weakenL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a
- same :: Member r a -> Member r b -> Maybe (a :=: b)
- weakenR :: Member r1 a -> Append r1 r2 r -> Member r a
- split :: Append r1 r2 r -> Member r a -> Either (Member r1 a) (Member r2 a)

# Abstract data types

A `Member ctx a`

is a "proof" that the type `a`

is in the type
list `ctx`

, meaning that `ctx`

equals

t0 ':>' a ':>' t1 ':>' ... ':>' tn

for some types `t0,t1,...,tn`

.

Member_Base :: Member (ctx :> a) a | |

Member_Step :: Member ctx a -> Member (ctx :> b) a |