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.

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