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 (possibly in DM) *) ;
  repr = (* a monad (possibly 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 monad must be in the DM fragment, the spec monad and interpretation are generated
• providing both repr and spec : the field interpretation must be provided to relate the runtime semantic to the predicate transformer monad. This last case is an extension of the previous system.

Examples

effect PrimitiveST {
  spec = {
    t = fun a -> (a -> st -> prop) -> st -> prop
    ret = ....;
    bind = ....;
  };

  (* no repr, no interp *)

  (* actions *)
  get = {
    spec = ....;
  } ;
  put = {
    spec = ....;
  }
}

effect ST4Free {
  repr = {
    t = fun a -> st -> M (a * st)
    ret = ....;
    bind = ....;
  };

  (* no spec, no interp *)

  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? *)
    t = fun a -> (unit -> M a)
    ret = fun #a (x:a) () -> x <: M a;
    bind = fun #a #b (m:t a) (f:(a -> t b)) () -> let x : a = m () in f x () <: M b;
  };

  repr = {
    (* finite sets *)
    t = 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 - spec for these could be derived from 'interpretation'   *)
  (*           but it may be useful to have the possibility to provide *)
  (*           them explicitly, for instance if 'interpretation' does  *)
  (*           not compute. *)
  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)
  }
}

open FStar.WellFounded
open FStar.List.Tot

(* Monad IO *)
type out
type input

noeq
type io (a:Type) =
  | IORet : a -> io a
  | Out : out -> io a -> io a
  | In : (input -> io a) -> io a

let ret_io #a (x:a) : io a= IORet x
let rec bind_io #a #b (m : io a) (f : a -> io b) : io b =
  match m with
  | IORet x -> f x
  | Out o m -> Out o (bind_io m f)
  | In g -> In (fun i -> axiom1 g i ; bind_io (g i) f)


(* Log transformer (DM) *)
type log (a:Type) = unit -> M (list out * a)

let ret_log #a (x:a) : log a =
  fun () -> ([], x)

let bind_log #a #b (m : log a) (f : a -> log b) : log b =
  fun () ->
  let (os, x) = m () in
  let (os', y) = f x () in
  (os @ os', y)

(* θ : IO -> LogT (Cont_Type)*)
let rec interpretation #a (m : io a) () (p : list out * a -> Type) : Tot Type (decreases m) =
  match m with
  | IORet x -> p ([], x)
  | Out o m -> interpretation m () (fun (os, x) -> p (o :: os, x))
  | In g -> forall (i : input). (axiom1 g i ; interpretation (g i) () p)


(* Actions and spec *)
open FStar.Tactics
let tau () = compute (); trefl ()


let read () : io input = In IORet

[@(postprocess_with tau)]
let read_spec () = interpretation (read ())

let write (o : out) : io unit = Out o (IORet ())

[@(postprocess_with tau)]
let write_spec o = interpretation (write o)


(* Proposal for effect introduction *)
effect IO {

  (* Underlying computational monad *)
  repr = { t = io ; ret = ret_io ; bind = bind_io } ;

  (* DM monad providing the monad transformer *)
  spec = { t = log ; ret = ret_log ; bind = bind_log } ;

  (* Monad morphism repr -> spec *)
  interpretation = interpretation;

  (* Actions to be available on the Dijkstra monad *)
  read = read ;
  write = write
}