search

joshvera / effects

An implementation of "Freer Monads, More Extensible Effects".
Other
20 stars 5 forks source link

Membership constraints can’t be used to deduce other membership constraints #35

Closed robrix closed 6 years ago

robrix commented 6 years ago

Because our redesign of Member to support fast(ish) compiled with Unions of hundreds of elements involved defining it using an ElemIndex type family where each branch is effectively a complete unrolling, there’s no relationship between different branches: you can’t infer Member t (U ': ts) from Member T ts, or vice versa.

While this is acceptable in cases where we aren’t dynamically extending the members (e.g. when used for à la carte ASTs), it’s counterproductive in its original use in Eff: you often end up having to carry around both the Member T ts and Member T (U ': ts) constraints, and this gets compounded every time you want to use T at a different level of embedding.

robrix commented 6 years ago

I think we should explore extracting Data.Union as it exists herein for use in à la carte ASTs, and restoring recursively-defined membership constraints that should (hopefully) make it possible for ghc to deduce the relationships between the indices of T in ts and U ': ts.

robrix commented 6 years ago

Fixed by #39.