Strengthen internal types and laws via gdp?

[spacekitteh]

(Discussion)

So, I've been thinking about how to instil confidence in the higher-order nature of Polysemy. In addition to the HasLaws machinery that was recently added, an orthogonal approach which might be quite useful (for internal modules, anyway) is to use the library gdp. If you aren't familiar with this, it is a handy library for zero-runtime-cost refinement typing entirely in Haskell, and much lighter-weight than, say, singletons.

I'm currently in the process of strengthening the internals of my SAT solver with it, you can see a bit of it e.g. here https://gitlab.com/spacekitteh/cosmothought/blob/master/thought-effects/src/Logic/Symbolic/SAT/Representations/CNF.hs

What does everyone think? Would you be up for trying it out?

[isovector]

I'm wildly excited about gdp. What did you have in mind?

[spacekitteh]

Well, I'm not sure - Polysemy's internals are still a mystery to me. Perhaps one starting point might be NonDet?

[KingoftheHomeless]

NonDet's probably not a good idea seeing how runNonDet is broken.

Maybe the Weaving machinery, and what makes use of it? I.e. Tactics and Final. Then again, from what I can tell Effect Handlers In Scope doesn't define any laws for the weave abstraction.

[spacekitteh]

NonDet's probably not a good idea seeing how runNonDet is broken.

That's exactly why I suggested it :D

[isovector]

It's not immediately clear to me how to throw gdp at polysemy. I'd appreciate some hints in that direction!

[spacekitteh]

Here's one example: when you interpret an effect, you may add it to a list of effects which have already been handled. So, say I create an effect which must not be handled after an effect which is used for communicating with another process - I could consult the list of already handled effects, and raise a custom type error.

Another example: You might want to prove that some effects are commutative with eachother in the effect row, and provide some rewrite rules such that the handlers are rearranged into the most efficient, yet semantically equivalent order.

I've found using 'Fact' quite useful for accumulating invariants, but until GHC 8.10 lands with the dictionary patch, it might not be zero-cost.