Uniform effects

F* currently possess 2 slightly different effect declaration mechanisms : primitive effects and DMForFree effects. This proposal try to unify and generalize the 2 presentations.

High-level plan

On the one hand, both DMForFree and primitive effects specify a predicate transformer monad. Among the current examples of effect definitions, these predicate transformer monads seem to always be provided by the application of a monad transformer to the monotonic continuation monad to Prop (or Type). These monad transformers can succintly be generated by a monad in DM.

On the other hand, DMForFree effects rely on a (automatically generated but provided) monadic runtime representation, whereas primitive effects are plainly erased during extraction and the (axiomatised) operations in these effects are assumed to be realized in the target languages.

Examples

new_effect {
  ND
  with
  repr = fset; (* finite sets *)
  ret_repr = singleton;
  bind_repr = fun m f -> union (map f m);
  
  spec = M;
  ret_spec = retM;
  bind_spec = bindM;

  (* optional *)
  interpretation = fun m p -> forall_in_set p m; (* GM: Kenji correct me if this is wrong *)

  choose = fun #a (m1 m2 : a) -> union (singleton m1) (singleton m2);
  choose_spec = fun #a m1 m2 (p : a -> prop) -> p m1 /\ p m2; (* correct w.r.t interpretation (if present) *)

  fail = fun #a -> empty;
  fail_spec = fun #a (p : a -> prop) -> True; (idem)
}