search

polysemy-research / polysemy

:gemini: higher-order, no-boilerplate monads
BSD 3-Clause "New" or "Revised" License
1.04k stars 73 forks source link

Strengthen internal types and laws via `gdp`? #284

Open spacekitteh opened 5 years ago

spacekitteh commented 5 years ago

(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 commented 5 years ago

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

spacekitteh commented 5 years ago

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

KingoftheHomeless commented 5 years ago

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 commented 5 years ago

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

That's exactly why I suggested it :D

isovector commented 5 years ago

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

spacekitteh commented 5 years ago

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.