-
Notifications
You must be signed in to change notification settings - Fork 231
Indexed effects
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
if_then_else and subcomp are optional; if they are omitted from the effect definition, F* generates default subcomp and if_then_else that keep the effect indices of the two computations in subcomp (resp. if_then_else) the same.
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
F* supports another optional combinator called close. This combinator is truly optional---unlike subcomp and if_then_else, if the combinator is not defined, F* will not generate a default one.
The close combinator has the shape:
close : a:Type -> b:Type -> is:(b -> is_t) -> f:(x:b -> repr a (is x)) -> Type
and the body of close is a repr a js, where js may mention any of the is binders. The semantics of the close combinator is as follows: given a computation type M a is that has some x:b free in the effect arguments (is), F* will use the combinator to close over x:b and return a computation type that does not have x free.
F* currently does not support any free-form binders for close. In the absence of a defined close, F* uses other techniques to close over x.
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 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, andks, - unifies substituted
iswithes1, effect indices fore1 - unifies substituted
jswithes2(effect indices fore2), and - returns the final computation type as substituted
M b ks
Other combinators are similar.
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.
The indexed effects combinators described so far are quite free-form (except close, for which F* supports only the shape described above). 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 restrict the shapes of these effect combinators, then F* can solve the bs binders using only substitutions, and hence, without any additional typechecking and guards for unification solutions. This may also be better for performance.
These stricter indexed effects combinators are called substitutive 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.
The shape of a substitutive return remains 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.
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 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 : 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: a:Type -> f1:t1 -> f2:t2 -> g1:t1 -> g2:t2 -> bs -> f:repr a f1 f2 -> PURE (repr b g1 g2) wp
Suppose we want to lift this effect to N that has 3 indices. Then a substitutive lift would have the following shape:
lift_M_N : a:Type -> f1:t1 -> f2:t2 -> bs -> f:repr a f1 f2 -> PURE (n_repr b e1 e2 e3) lift_wp
In general, it is a:Type, followed by binders for source effect's repr, some optional binders, the f argument, and the return type.
close as defined above is already substitutive.
In practice, we have found that most combinators can be made substitutive, and making them so provides much better usability.
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.
F* supports another style of substitutive subcomp and if_then_else. In some cases, the effect may want to keep the indices of the two computations in subcomp (resp. if_then_else) the same. For such cases, a substitutive subcomp looks like (taking the same example with two effect indices):
subcomp : a:Type -> f1:t1 -> f2:t2 -> bs -> f:repr a f1 f2 -> Pure (repr a f1 f2) wp
Similarly:
if_then_else : a:Type -> f1:t1 -> f2:t2 -> bs -> f:repr a f1 f2 -> g:repr a f1 f2 -> Type
and the body of if_then_else is a repr as usual.
We call these as substiutive invariant combinators. Only subcomp and if_then_else are allowed to be substitutive invariant.
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).
F* also supports polymonadic binds ((M, N) |> P) and subcomp (M <: N).
In general, a polymonadic bind (M, N) |> P has the following shape:
polymoandic_bind : a:Type -> b:Type -> bs -> f:m_repr a is -> g:(x:a -> n_repr b js) -> Pure (p_repr b ks) wp_bind
As before, the binders bs are arbitrary, and solved using unification.
Polymonadic binds can also be made substitutive. Suppose M, N, and P all have two indices, then a substitutive polymonadic bind looks like:
polymonadic bind : a:Type -> b:Type -> f1 -> f2 -> g1:(a -> _) -> g2:(a -> _) -> f:m_repr a f1 f2 -> g:(x:a -> n_repr b (g1 x) (g2 x)) -> Pure (p_repr b p1 p2) bind_wp
A polymonadic subcomp M <: N has the following shape:
polymonadic subcomp : a:Type -> bs -> f:m_repr a is -> Pure (n_repr a js) wp
with substitutive combinator as (assuming M and N with two indices each):
polymonadic subcomp : a:Type -> f1 -> f2 -> g1 -> g2 -> f:m_repr a f1 f2 -> Pure (n_repr a g1 g2) wp
F* supports limited form of reification and extraction for indexed effects.
An indexed effect may be annotated with the reifiable qualifier. When annotated as such, the programmer can write reify e, where reify is a keyword in the language and e is a computation in the effect, to coerce the type of e to its underlying representation type. In other words, if e : M a is then, reify e : M.repr a is.
reify is just a coercion at the type level, and it can only be reasoned with its type. Think of it as an abstraction function from M a is to M.repr a is. SMT encoding, for example, doesn't know anything more about reify than just its type.
F* supports two forms of extraction of indexed effects (see examples/layeredeffects/extraction for some examples):
An indexed effect may be annotated with an attribute primitive_extraction. If so, the effect is extracted natively. For example, the M.bind applications are natively extracted to let bindings.
The primitive_extraction attribute is incompatible with the reifiable keyword; F* will error out if an effect definition is annotated with both.
The other mode of extraction for an indexed effect is via reification. But there are a few restrictions on the indexed effect for it to be extractable via reification:
- The effect must be annotated as
reifiable. - All the effect indices must be non-informative. Non-informative terms include:
Type_u,unit,squash p,erased t, any type witherasableattribute`, pure or ghost arrows whose return type is non-informative, arrows with erasable effect in their co-domain, and applications whose head term is non-informative. In other words, the effect indices must be erasable at extraction. - The
bindcombinator of the effect must be substitutive.
When an effect has these properties, F* typechecker marks an effect as extractable and extracts computations in the effect via reification.