Meta Issue for DM4F

[catalin-hritcu]

Moving this from the README in dm4free since with the locked master that's harder to edit and keep up to date compared to an issue.

• Code-review of the generated code vs currently used code.
  Some things that we expect to differ, but maybe that's ok:
  • order of arguments
  • extra thunking (e.g. for exception monad)
  • error labeling -- removed by Nik's new error reporting
  • (un)currying / subtyping on pairs
• change the elaboration of the match to push the return inside the branches
  instead of wrapping the whole branch on the outside (better for Z3)
• simplify the implementation of the subtyping rule for elaborated effects
• make this work with parametrized effects (i.e. ST) (Parameters on DM4F effects #706)
  • stop-gap nominal implementation in progress
  • longer term plans for indexed effects described on the wiki
• support implicit arguments (dm4f: support implicit arguments #721)
• try out more examples -- which ones precisely? please list !
  (i.e. more interesting IFC (More interesting IFC example using dm4f #720), IO, nondetermism, probabilities)
  (CH: this might belong below the line, actually.)
• inserting return on the fly when reflecting Tot computations
• generate lift from Pure to all DM4F effects (dm4f: generate lift from Pure to all DM4F effects #719)
• M not quite a synonym for Tot (dm4f: M not quite a synonym for Tot #710)
• M is sometimes erased to Tot during typechecking
  leading DM4F's elaboration to fail
• reification not computing for lifts and "monadic application"
  this makes even the simplest reification of exceptions not work;
  (IntST.ifc works despite this, but that's probably because the SMT solver can normalize too)
• it would be good to have a generic way of noticing that a WP
  combinator contains a branching construct within it and that it may
  lead to exponential blowup. In such a case, we should wrap the WP
  with a "name_continuation" combinator, which is currently called
  "wp_ite" and should be renamed. This is particularly important for
  the exceptions monad, where every bind contains a branch.
  (partially done ; it's not done when every bind includes a case analysis)
• fill out various TODOs in dmff.fs to faithfully check everything
  (right now, most checks are fairly lax);
• extraction of user defined effects (Extracting DM4F non-primitive effects #886)
• remove spurious quantifications on unit in wps (cf ghost_reify in FStar.Heap.ST)

---

The items below this line seem less urgent than the ones above:

• make the continuation effect work (dm4f: Cannot define continuations #713) -- still need to return to the things that almost worked
• we had some problems with refineST for the final version, should return to them at some point
• add some specific syntax in the decrease clause to capture other arguments
  of the effect monad (i.e. pass the current heap for ST)
• dreaming: can we also generate abbreviations for the "triples" form
  of an effect? (Generating triples and unconditional form for a DM4F effect #758)
• porting Wysteria to use dm4free (but first universes)
• reification of arbitrary lifts (currently only reifies lifts from pure)

---

    Syntactic simplifications of DM4F definitions

---

• removing the reifiable and reflectable keywords
  needs the ability for the module system to hide reify and reflect or replace them with noreifiable noreflectable
• allowing definition in a effect to be dependent on previously defined fields (in particular repr)
• fixing the bugs which prevents inlining the definition of effect members
• unifying new_effect and new_effect_for_free by automagically detecting in the compiler if some elaboration id needed
• remove with effect_actions label which is useless (anything apart repr, return and bind is an action)
• consider generating a total and divergent version of each effects and remove the total keyword

[catalin-hritcu]

@kyoDralliam @nikswamy Just a heads up that I've updated and moved this here for easier updating.

[aseemr]

We don't plan to address these any time soon, marking as wontfix and closing until we revisit.