# 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.

1

Since F* is an extensional type theory, pure F* terms are only weakly normalizing. That is, some evaluation strategies (e.g., repeatedly reducing a recursive function deep in an infeasible code path) need not terminate. However, for every closed, pure term, there is a reduction strategy that will reduce it fully. As such, the evaluation order for pure functions is irrelevant, except that some choices of evaluation order may lead to non-termination.