Indexed effects

Indexed effects definition

An indexed effect is defined as a representation repr and effect combinators return, bind, if_then_else, and subcomp. F* requires these combinators to have a certain shape. For example, bind for an indexed effect must have the shape:

bind : a:Type -> b:Type -> bs -> f:repr a is -> g:(x:a -> repr b js) -> repr b ks

where bs are some binders and is, js, and ks are terms for effect indices of the computations f, g, and the resulting computation. As is usual with dependent arrows, binders bs may occur free in is, js, and ks.

Similarly, return, if_then_else, and subcomp have the following expected shapes:

return : a:Type -> x:a -> bs -> repr a is

if_then_else : a:Type -> bs -> f:repr a is -> g:repr a js -> p:bool -> Type

and the body of if_then_else definition must be a repr.

subcomp : a:Type -> bs -> f:repr a is -> PURE (repr a js) wp

There are also lifts whose general shape is (for a lift from effect M1 to M2):

lift_M1_M2 : a:Type -> bs -> f:m1_repr a is -> PURE (m2_repr a js) wp

For wp-based effects, say PURE, the representation is: unit -> PURE a wp. So a lift from PURE to M may look like:

lift_PURE_M : a:Type -> bs -> f:(unit -> PURE a wp_term) -> PURE (repr a is) wp_res

Applying indexed effects combinators

Once an indexed effect is defined, F* uses these combinators to typecheck computations in the effect. For example, for some code like:

let x = e1 in
e2

where e1 : M a es1 and e2 : M b es2, F* would use the bind combinator of M to compute the resulting computation type.

The way a bind combinator is applied is as follows. Suppose the bind has the shape:

bind: a:Type -> b:Type -> bs -> f:repr a is -> g:(x:a -> repr b js) -> repr b ks

F* then:

• creates fresh unification variables for the binders bs,
• substitutes those binders with corresponding unification variables in indices is, js, and ks,
• unifies substituted is with es1, effect indices for e1
• unifies substituted js with es2 (effect indices for e2), and
• returns the final computation type as substituted M b ks

Other combinators are similar.

Typechecking the unification solutions

The unification variables for these bs binders are solved by the unifier. As is the case with all the unifier solutions, these solutions are typechecked by the core typechecker, which could potentially result in smt guards.

Substitutive indexed effects

The indexed effects combinators are quite free-form. There is no restriction on the binders bs, so they are quite flexible.

However, this flexibility comes at a cost. The implementation solves these binders using unification, and then those solution are core typechecked, potentially resulting in more proof obligations.

Instead if we follow a stricter shape on these effect combinators, then F* can solve these bs binders using only substitutions, and hence, without any additional typechecking and guards for unification solutions. This is also better for performance.

These stricter indexed effects are called substitutive indexed effects and have following shapes.

Let's take the example of an effect with two indices of types t1 and t2, generalization to arbitrary number of indices is straightforward.

return

The shape of a substitutive return remains the same as the general indexed effects case:

return : a:Type -> x:a -> bs -> repr a e1 e2

The binders in bs are still solved using unification, e1 and e2 are the effect indices of the return.

bind

The shape of a substitutive bind is as follows:

bind : a:Type -> b:Type -> f1:t1 -> f2:t2 -> g1:(a -> t1) -> g2:(a -> t2) -> bs -> f:repr a f1 f2 -> g:(x:a -> repr b (g1 x) (g2 x)) -> repr b ks

I.e.: the two type binders, binders for indices of the f computation (in order), binders for indices of the g computation abstracted over x:a (in order), some optional bs binders, and then the f and g computations. In this case, only bs are solved using unification, f1, f2, g1, g2 are solved by substitution.

Sometimes it may be the case that only some of the g_i binders can be abstracted over x:a. For example, bind for a graded state monad looks like:

bind : a:Type -> b:Type -> grade_f:grade -> grade_g:grade -> f:repr a grade_f -> g:(x:a -> repr b grade_g) : repr b grade_g

To allow for such cases, in substitutive indexed bind, the g_i binders may be mixed, i.e. some may be abstracted over x:a, and some may not be. Those that are abstracted over are solved by substitution, but those that are not fallback to unification. Note that they still need to be in the order though.

if_then_else

if_then_else : a:Type -> f1:t1 -> f2:t2 -> g1:t1 -> g2:t2 -> bs -> f:repr a f1 f2 -> g:repr b g1 g2 -> p:bool -> Type

with the body being a repr term as usual. As before, f1, f2, g1, g2 are solved by substitution, and (optional) bs by unification.

subcomp

subcomp: a:Type -> f1:t1 -> f2:t2 -> g1:t1 -> g2:t2 -> bs -> f:repr a f1 f2 -> PURE (repr b g1 g2) wp

In practice, we have found that most effects can be made substitutive.

If an indexed effect combinator is not substitutive, then F* emits a warning at the time of typechecking that combinator. An indexed effect may have only some combinators substitutive.

Effect parameters

Indexed effects also support a notion of effect parameters: indices that remain invariant for all the computations in an effect instance.

Take for example a state effect, that's parametric over the state:

type repr (a:Type) (st:Type u#1) (pre:st -> prop) (post:st -> a -> st -> prop) = s0:st -> Pure (a & st) (pre s0) (fun (x, s1) -> post s0 x s1)

A bind for such an effect, even if written in the substitutive style would be:

bind : a:Type -> b:Type -> st:Type u#1 -> pre_f:_ -> post_f:_ -> pre_g:(a -> st -> prop) -> post_g:_ -> f:repr a st pre_f post_f -> g:(x:a -> repr b st (pre_g x) (post_g x)) -> repr b pre_bind post_bind

But this doesn't match the expected shape that we have described. The st:Type u#1 parameter appears in the indices of both f and g, but appears just once in the binders of bind.

We may play some tricks, by having two binders st_f and st_g, and then having a binder that's a proof of st_f == st_g, and perhaps solving that binder with a tactic --- but this is quite complicated for a simple state parametric state effect.

Instead, F* allows marking some effect indices as parameters at the time of effect definition:

effect {
  ST (a:Type) ([@@@ effect_param] st:Type u#1) (pre:st -> prop) (post:st -> a -> st -> prop)
  with { ...}
}

By using a binder attribute effect_param. An effect may have multiple effect parameters, but all of them must appear upfront in the effect signature.

If an effect index is specified as an effect parameter, then the expected shape of bind, for example, is:

bind : a:Type -> b:Type -> bs_params -> bs_f -> bs_g -> bs -> f -> g -> repr ...

I.e. binders for effect parameters appear upfront and specified just once (f and g share them). Rest remains same.

The effect parameter binders must appear upfront in all the effect combinators (for them to be substitutive).