The Effect of Total Computations

At the very bottom of the effect label hierarchy is Tot, used to describe pure, total functions. Since they are at the bottom of the hierarchy, Tot computations can only depend on other Tot computations, ensuring that F*’s logical core remains total.

Every term in F* is typechecked to have a computation type. This includes the total terms we have been working with. Such terms are classified in the default effect called Tot, the effect of total computations that do not have any observable effect, aside from the value they return. Any meaning or intuition that we have ascribed to typing e:t extends to e:Tot t. For example, if e:Tot t, then at runtime, e terminates and produces a value of type t. In addition, since its effect label is Tot, it has no side-effect.

In fact, as we have already seen, notationally x:t0 -> t1 is a shorthand for x:t0 -> Tot t1 (where t1 could itself be an arrow type). More generally, arrow types in F* take the form x:t -> C, representing a function with argument type t0 and body computation type C (which may depend on x).

Similarly, the return type annotation that we have seen in the let definitions is also a shorthand, e.g., the id function

let id (a:Type) (x:a) : a = x

is a shorthand for

let id (a:Type) (x:a) : Tot a = x  //the return type annotation is a computation type

and the type of id is a:Type -> a -> Tot a. More generally, the return type annotations on let definitions are computation types C.

The explicit annotation syntax e <: t behaves a little differently. F* allows writing e <: C, and checks that e indeed has computation type C. But when the effect label is omitted, e <: t, it is interpreted as e <: _ t, where the omitted effect label is inferred by F* and does not default to Tot.

Evaluation order

For pure functions, the evaluation order is irrelevant. [1] F* provides abstract machines to interpret pure terms using either a lazy evaluation strategy or a call-by-value strategy (see a forthcoming chapter on F*’s normalizers). Further, compiling pure programs to OCaml, F* inherits the OCaml’s call-by-value semantics for pure terms.

When evaluating function calls with effectful arguments, the arguments are reduced to values first, exhibiting their effects, if any, prior to the function call. That is, where e1 and e2 may be effectful, the application e1 e2 is analogous to bind f = e1 in bind x = e2 in f x: in fact, internally this is what F* elaborates e1 e2 to, when either of them may have non-trivial effects. As such, for effectful terms, F* enforces a left-to-right, call-by-value semantics for effectful terms.

Since only the value returned by a computation is passed as an argument to a function, function argument types in F* are always value types. That is, they always have the form t -> C. To pass a computation as an argument to another function, you must encapsulate the computation in a function, e.g., in place of C -> C, one can write (unit -> C) -> C'. Since functions are first-class values in F*, including functions whose body may have non-trivial effects, one can always do this.