Uniform effects

F* currently possesses 2 slightly different effect declaration mechanisms: primitive effects and DMForFree effects. This proposal tries 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.

The proposal is to provide the following interface for defining new effects :

effect MyEffect {
  spec = (* a monad in DM *) ;
  repr = (* either a plain monad or a monad in DM *) ;
  interpretation = (* only necessary if both repr and spec are provided *) ;
  actions (* for primitive effects, it would be the same as axioms *)
}

where a monad is a record providing the following data

type monad = { 
  t : Type -> Type ;
  ret : #a -> (x:a) -> t a ;
  bind : #a -> #b -> t a -> (a -> t b) -> t b
}

Examples

effect PrimitiveST {
  spec = {
    (* cont into prop, or should it just be the identity transformer here? *)
    type = fun a -> (a -> st -> prop) -> st -> prop
    ret_spec = ....;
    bind_spec = ....;
  };

  (* no repr, no interp *)

  actions = {
    get = {
      spec = ....;
    }
    put = {
      spec = ....;
    }
  }
}

effect ST4Free {
  repr = {
    (* cont into prop, or should it just be the identity transformer here? *)
    type = fun a -> st -> M (a * st)
    ret = ....;
    bind = ....;
  };

  (* no spec, no interp *)

  actions = {
    get = {
      repr = fun s -> (s, s)
    }
    put = {
      repr = fun s _s0 -> ((), s)
    }
  }
}

effect ND {
  spec = {
    (* cont into prop, or should it just be the identity transformer here? *)
    type = fun a -> (a -> prop) -> prop
    ret_spec = ret_cont;
    bind_spec = bind_cont;
  };

  repr = {
    (* finite sets *)
    type = fset;
    ret = singleton;
    bind = fun m f -> union (map f m);
  };

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

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

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