The syntax of arrow types and default effects

Syntax of arrow types

The arrow type x1:t1 -> ... -> xn:tn -> t is equivalent to x1:t1 -> Tot (... -> Tot (xn:tn -> Tot t))). That is, the effect annotation on every arrow defaults to Tot.

As a matter of style, we tend to omit the effect annotation on all but the last arrow, since functions of several arguments are so common.

However, with two exceptions, we recommend always writing the effect annotation on the last arrow, since it is typically very informative. The exceptions are:

The types of data constructors

We write

type t = 
 | C : int -> t

Rather than

type t = 
 | C : int -> Tot t

Since data constructors are always total.

The types of Type-returning functions

We tend to write t -> Type rather than t -> Tot Type, since non-total Type returning functions are very uncommon.

Default effects in function definitions

When defining a named function using a let binding, it is possible to annotate the result of the function using the following notation.

let f x : t = e

We expect t to always be a computation type, e.g., Tot t, ML t etc.

In case t is not a computation type, it is interpreted as Tot t. For example,

let f (x:nat) : nat = e

is interpreted as

let f (x:nat) : Tot nat = e

This is consistent with the notation for function arrows x:nat -> nat being interpreted as x:nat -> Tot nat, as well as the syntax of val declarations, i.e.,

val f (x:nat) : nat

is equivalent to

val f (x:nat) : Tot nat

Note, for let bindings where the defined term is not bound to an application pattern (an application pattern has the form f p1 ... pn, for some patterns p1 ... pn), e.g., let x : t = e, the annotated type is always a value type, not a computation type.