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 = (* a monad morphism from repr to spec *) ;
  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
}

Among the spec and repr fields, the following 3 cases are admissible :

• only providing spec : this correspond to a primitive effect (at extraction, it is erased)
• only providing repr : this corresponds to a DMForFree effect, the spec monad and interpretation are generated
• providing both repr and spec : the field interpretation has to be provided to relate the runtime semantic to the predicate transformer monad

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)
    }
  }
}