Indexed effects

This proposal was put on hold after trying to implement it a couple of times (and failing). A lighter-weight proposal by Danel Ahman is currently under discussion: https://github.com/FStarLang/FStar/issues/1573

The problem

Computation types in F* currently must have the from M t wp, i.e., an effect label applied to a result type and a wp.

We would like instead to allow a computation type to carry other indices, i.e., to be of the form M i_1...i_n t wp.

This would allow us to treat families of related effects polymorphically, compensating somewhat for the lack of effect polymorphism in F*.

For example, we could type the action ST.get as h:Type -> unit -> ST h h (fun post h0 -> post (h0, h0))

This note summarizes several discussions between Danel, Catalin, Jonathan, Kenji, Tahina and Nik.

An initial proposal

1. Generalize FStar.Syntax.Syntax.comp_typ so that it is of the form:

comp_typ = {
  comp_univs:universes;
  effect_name:lident;
  effect_indices:list<term>; //this is the new field
  result_typ:typ;
  effect_args:args;
  flags:list<cflags>
}

We would need to propagate this change throughout the existing code. One difficulty is that some of the code makes an unfortunate implicit assumption that comp_univs is a singleton list and uses that to recover the universe of the result_typ. We would have to get rid of that assumption.

2. The sub_effect relation will be generalized to the form

sub_effect forall (i_1:t_1)...(i_n:t_n). M j_1 .. j_m ~> N k_1 ... k_l

where all the j_1 ... j_m are distinct and are included in the set {i_1, ..., i_n}. The k's are unconstrained, except for the obvious property that both the LHS and RHS of the relation have to be well-typed applications of effect labels to all their indices (excluding the result type and the wp).

There can be at most 1 sub_effect relation between M and N regardless of their indices.

Some examples

This will already let us define things like

sub_effect forall (h:Type). Exn ~> StExn h

lifting exceptions to state+exceptions, generically in the type of the state.

It will also allow us to define a generic pre-order indexed state monad as ST (h:Type) (r:pre_order h) and work with this as a computation type, which is currently not possible

A longer term solution

More generally, we would like to also support examples such as the following encoding of a frame rule for stateful computations.

In very rough DM pseudo-code (not accounting for dynamic allocation):

let fp = set aref //footprint
let mem (f:fp) = h:heap { dom h = f}
let st (f:fp) = mem f -> Tot (a * mem f)
let return : #a:Type -> #f:fp -> a -> st fp a =  ...
let bind : #a:Type -> #b:Type -> #f:fp -> st fp a -> (a -> st fp b) -> st fb b = ...
let get ...
let put ... //the usual ones

On top of this, one can define:

let (!) (r:ref a) : st {r} a = fun (h:mem {r}) -> returnT (sel h r, h)
let (:=) (r:ref a) (x:a) : st {r} a = fun (h:mem {r} -> returnT ((), upd h r x)

Next, we can define a lifting that allows widening the footprint of a computation:

let lift (f:fp) (g:fp{f `subseteq` g}) (a:Type) (x:st f a) = 
   fun (h0:mem g) -> 
   let h0, frame = un_star f h0 in
   let res, h1 = f h0 in
   res, star h1 frame

Using this, it should be possible to write code like

let old = !x in
x := 0;
y := old

and infer for it a type like st {x, y} unit

But, for this, we need some type-inference hints to compose the indexes of computation types.

We suggest including notation of the form:

join_effect forall fp1, fp2. ST fp1, ST fp2 ~> ST (fp1 `union` fp2)

where union is a function operating on the syntax of F* terms, i.e., some kind of tactic.

Using this join hint, the typechecker can sequentially compose effects and their indices, just as it does today on the effect labels, while using the tactic to join indices.

In this case, union can just be the simple FStar.Set.union. However, in other cases, we may want joins to be defined in more powerful ways, e.g., pattern matching on types and combining FStar.Heap.heap and FStar.HyperHeap.mem to the latter.