-
Notifications
You must be signed in to change notification settings - Fork 234
Indexed effects
This proposal was put on hold after trying to implement is a couple of times. A lighter-weight proposal by Danel Ahman is currently under discussion: https://github.com/FStarLang/FStar/issues/1573
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.
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.
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.
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
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.