Portability | GHC |
---|---|
Stability | experimental |
Maintainer | emw4@rice.edu |
Safe Haskell | None |
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 |