Skip to content

Proposal: Indexed effects

Jump to bottom Edit New page
Aseem Rastogi edited this page Nov 21, 2022 · 1 revision

The following is an implementation plan from years back, see this for the current state of indexed effects in F*.

Effects in F* are currently specified in two ways:

  • Primitive effects are given WP-semantics directly
  • WP semantics for an effect are derived from the semantics of an underlying (restricted class of) computational monad (DM for free)

This note proposes a third way, a style of effect layering, obtained by combining aspects of the above two.

(The theory of yet another way of defined effects in F* is being worked out in the DM for All project, but this note is, as yet, unrelated)

Motivation: Error handling in Low*

Low* code is compiled to C. C lacks an exception-handling mechanism. So, error handling code in Low* is forced to handle errors manually. See, for example, https://github.com/project-everest/mitls-fstar/blob/master/src/tls/Negotiation.fst#L881

A standard way of dealing with this is to package exception handling as a monad. In fact, this is what we do sometimes in F* too, especially in an unverified setting. See, e.g, https://github.com/project-everest/QUIC-FStar/blob/master/QUICFrame.fst#L331

However, packaging up exception handling in a user-defined error monad does not work well in combination with WP inference, requires using ad hoc do-notation rather than F* built-in monadic-let syntax etc.

An effect for error handling + state layered on top of State

let st_exn_wp (a:Type) = wp:((post:option a -> mem -> Type) -> mem -> Type){monotone wp}
let st_exn (a:Type) (wp:st_exn_wp a) =
    unit -> State (option a) wp
let st_exn_return ...
let st_exn_bind ... f g = fun () ->
   match f () with
   | None -> None
   | Some x -> g x ()
let st_exn_if_then_else ...

[total reifiable reflectable] layered effect {
   StateExn : a:Type -> st_exn_wp a -> Effect
   repr = st_exn;
   return = st_exn_return;
   bind = st_exn_bind; 
   ...
}

These definitions and the layered effect declaration introduce a new effect constructor StateExn, whose WP semantics is defined by the return, bind, wp_ite, etc. combinators (just as they do for primitive effects like PURE). But, StateExn has a computational representation in terms of st_exn, and the reify and reflect coercions move between this representation and the effect.

During extraction, the StateExn computation type is reified to its underlying representation---the extracted code explicitly processes exceptions via their representation, but the source code need not.

An effect for a separation logic of resources

In https://github.com/FStarLang/FStar/blob/danel_lowstar_lens/ulib/LowStar.RST.fst#L131, we define RSTATE, an indexed effect layered again on FStar.HyperStack.ST.STATE, but this time encapsulating a separation logic of abstract resource.

At https://github.com/FStarLang/FStar/blob/danel_lowstar_lens/ulib/LowStar.RST.fst#L158 we define a custom rule for the sequential composition of RSTATE computations.

Whereas the StateExn example of the previous section encapsulated a certain computational monad, revealing it for extraction purposes, here the new effect layer simply packages new reasoning principles for RSTATE computations that are proven sound in terms of their underlying STATE represenations.

Some technical requirements and non-requirements of layered effects (Rest of this page is outdated, will be updated soon)

  1. Layered effects can carry an arbitrary number and structure of indices following the result type, i.e., we allow L a i1... in. Unlike the WP index of existing F* effects, these indices need not form a monad or obey any predetermined structure.

  2. For now we don't impose any restrictions on the generality of indices in the effect operations. For example, the bind may have the following shape, where l a i1..in is the representation of L a i1..in.

val bind_L #a #i1...#ip #b #j1 .. #jq #k1 .. #kn
        (f:l a i1 ... ip ... in)  //where indices from p+1 to n are computed somehow from i1 ... ip 
        (g: (x:a -> l b (j1 x) ... (jq x) ... (jn x)))  //where again indices beyond q, including jn, are some function of j1 ... jq
        (l b k1 ... kn)  //the indices k1 ... kn could also unconstrained here (the context may determine them)

This may make unification problems trickier (as opposed to if we enforce that the indices of f and g are all general), but we will see what kind of problems arise in practice.

  1. Same goes for return, it could be of the form:
val return #a (x:a) : l a i1...in

or be general in some of the indices.

  1. Sub effects between layered and non-layered effects are allowed, and again with no requirements on the indices generality.

E.g., this is allowed

sub_effect
 PURE ~> StateExn = st_exn_return

or sub-effecting with a layered effect on the left:

sub_effect
 L ~> M = (lift_L_M : #a #ii ... #in (f:l a i1...n) : m a j1 ... jn

Once again the lift could be general in any subset of the involved indices.

Some observations

With this proposal, we are beginning to approach the generality of polymonads (in that indices have no prescribed structure) ... but not quite. Polymonads are even more unrestricted. http://www.cs.bham.ac.uk/~pbl/msfp2014/polymonad.pdf

This is also reminiscent of prior aborted attempts at indexed effects. But, again, not quite. For instance, prior attempts were trying to define and use a generic state monad as a computation type, juggle argument orders of effects etc. which led to many implementation pitfalls. But, it is quite close ...

Next level of implementation details:

Below we get into the next level of details, in particular how the layered effects are specified, how are they type checked, (each type checking requirement is specified as TCn), and how does the typechecker code change.

Let's take an example of implementing ST a req ens as a layered effect on top of STATE a wp.

ST has two indices in the form of the requires and the ensures clauses with the following type:

type req_t = heap -> Type0
type ens_t (a:Type) = heap -> a -> heap -> Type0

Below we represent the indices as tuples. In general, should we enforce that the indices are n-tuples? It makes it a little easier to write the types.

type indices (a:Type) = req_t * ens_t a

Following is how the programmer would specify the effect, we define each of the functions and their intent below.

layered_effect {
  ST : result:Type -> indices result -> Effect

  with
    base_effect    = STATE;
    repr_indices   = repr_indices;
    repr_comp      = repr_comp;
    return_indices = return_indices;
    return_repr    = return_repr;
    bind_indices   = bind_indices;
    bind_repr      = bind_repr;
    if_then_else   = if_then_else;
    ...            = ...  //other combinators
}

(*
 * Div is also a layered effect with requires and ensures as its indices
 *)
let lift_div_st (a:Type) (is:div_indices a) : indices a =
  fun _       -> fst is
  fun h0 r h1 -> snd is r /\ h0 == h1

sub_effect Div ~> ST = lift_div_st

TC1. A layered effect has form: a:Type -> <.. n tuple indices ..> -> Effect

We now describe what each of the functions are and their typechecking obligations.

In its full generality, the base effect over which the current effect is layered, could itself be an indexed effect (rather than a standard wp-based effect). repr_indices computes the base effect indices from the current effect indices.

In the current example, the repr effect has just one index: wp.

let repr_indices (a:Type) ((pre, post):indices a) : st_wp a =
  fun p h0 -> pre h0 /\ (forall r h1. post r h1 ==> p r h1)

TC2. repr_indices has the type: a:Type -> indices a -> <.. some number of optional implicits ..> -> (base_effect indices a). The optional implicits allow some of the base effect indices to be left unspecified.

repr_comp is the representation of the layered computation.

let repr_comp (a:Type) (is:indices a) : Type =
  unit -> STATE a (repr_indices a is)

TC3. repr_comp has the type: a:Type -> is:indices a -> Type, and its definition is an arrow ending in base_effect a (repr_indices a is).

return_indices specify the indices of a monadic return.

let return_indices (a:Type) (x:a) : indices a =
  fun _       -> True,
  fun h0 r h1 -> r == x /\ h0 == h1

TC4. return_indices has type: a:Type -> x:a -> <.. optionally some implicit arguments ..> -> indices a. The optional implicit arguments leave open the possibility of leaving some returned indices unspecified, perhaps to be determined by the context.

return_repr is the representation of a return in the underlying effect:

let return_repr (a:Type) (x:a) : repr_comp a (return_indices a x) =
  fun _ -> x

TC5. return_repr has the type: a:Type -> x:a -> <.. optionally some implicit arguments ..> -> repr_comp a (return_indices a x). The implicit arguments in return_repr are same as those in return_indices?

Similarly bind_repr and bind_indices:

let bind_indices (a:Type) (b:Type) (is1:indices a) (is2:a -> indices b) : indices b =
  fun h0      -> fst is1 h0 /\ forall x h1. snd is1 h0 x h1 ==> fst (is2 x) h1,
  fun h0 y h2 -> forall x h1. snd is1 h0 x h1 ==> snd (is2 x) h1 y h2

let bind_repr (a:Type) (b:Type)
  (is1:indices a) (is2:a -> indices b)
  (c1:repr_comp a is1) (c2: x:a -> repr_comp b (is2 x))
  : repr_comp b (bind_indices a b is1 is2)
  = fun _ ->
    let x = c1 () in
    c2 () x

TC6. bind_indices has the type: a:Type -> b:Type -> indices a -> (a -> indices b) -> <.. optionally some implicit arguments ..> -> indices b.

TC7. bind_repr has the type: a:Type -> b:Type -> is1:indices a -> is2:(a -> indices b) -> c1:repr_comp a is1 -> c2:(x:a -> repr_comp b (is2 x)) -> <.. optionally some implicit arguments ..> -> repr_comp b (bind_indices a b is1 is2). The implicit arguments in bind_repr are same as those in bind_indices?

Coming to the combinators, e.g. if_then_else etc. now. Each of the combinators has a definition AND an associated proof for consistency of the combinator with the same combinator of the underlying effect. For example, here is the if_then_else combinator for our example:

let if_then_else (a:Type) (p:Type) (is_then:indices a) (is_else:indices a) : indices a =
  fun h0      -> l_ITE p (fst is_then h0) (fst is_else h0),
  fun h0 x h1 -> l_ITE p (snd is_then h0 x h1) (snd is_else h0 x h1)

TC8. if_then_else has the type: a:Type -> p:Type -> indices a -> indices a -> <.. optionally some implicit arguments ..> -> indices a.

To make sure that the combinator makes sense in the underlying effect, the combinator if_then_else is accompanied by the proof if_then_else_consistent with an expected type. The programmer has to provide such a proof for all the combinators: if_then_else, ite_indices, stronger, close, assert, assume, null, and trivial.

let if_then_else_is_consistent
  (a:Type) (p:Type) (is_then:indices a) (is_else:indices a)
  : Lemma (st_stronger (repr_indices a (if_then_else a p is_then is_else))
                       (st_if_then_else a p (repr_indices is_then) (repr_indices is_else)))
  = <.. proof ..>

TC9. if_then_else_consistent has the expected type.

... Similarly other combinators and their associated proofs ...

TC10. Lifts to this effect from some effect E have the type: a:Type -> <indices of E> -> <.. some optional implicits ..> -> indices a

Typechecker changes:

Changing TcUtil.bind and other functions:

We want to change these to work over layered effects and wp-based effects using the same code.

lift_and_destruct:

Currently lift_and_destruct returns:

let (eff_decl, _, _), (u_t1, t1, wp1), (u_t2, t2, wp2) = lift_and_destruct env c1 c2

It will now be instead:

let (eff_decl, _, _), (u_t1, t1, is1), (u_t2, t2, is2) = lift_and_destruct env c1 c2

where is1 and is2 are list of indices ... eff_decl may be a wp-based effect or layered effect, in which case is1 and is2 are singletons (wps).

Then bind will apply eff_decl.bind_wp to is1 and is2 with fresh uvars for implicit arguments.

The lattice of effects will now also contain layered effects and lifts to- and from them.

bind and other operators will never translate a layered effect to its underlying representation themselves? I.e. programmer must specify a lift OR we can take repr_indices and use it as a lift if required?

Implementation plan

I will start with AST changes for parsing and populating these layered effects, then typechecking them, and keeping them in the environment. And finally changing TcUtil functions to work over these.

Add a custom footer
Add a custom sidebar
Clone this wiki locally