consider declaring the effects of a function

We are used to having functions that declare a return type. In java, it's common to also declare any exceptions that can be thrown. However, there could be other effects, such as passage of time, elevation of privilege, consumption of resources, etc. Knowing these effects (and lack thereof) could influence the provability of code in profound ways.

Consider this passage from a tutorial about a language called F*, being developed at Microsoft Research (https://www.fstar-lang.org/tutorial/):

Although we didn't write down any types for functions like canRead or canWrite, F* (like other languages in the ML family) infers types for your program (if F* believes it is indeed type correct). However, what is inferred by F* is more precise than what can be expressed in ML. For instance, in addition to inferring a type, F* also infers the side-effects of an expression (e.g., exceptions, state, etc).

For instance, in ML (canRead "foo.txt") is inferred to have type bool. However, in F*, we infer (canRead "foo.txt" : Tot bool). This indicates that canRead "foo.txt" is a total expression, which always evaluates to a boolean. For that matter, any expression that is inferred to have type-and-effect Tot t, is guaranteed (provided the computer has enough resources) to evaluate to a t-typed result, without entering an infinite loop; reading or writing the program's state; throwing exceptions; performing input or output; or, having any other effect whatsoever.

On the other hand, an expression like (System.IO.read "foo.txt") is inferred to have type-and-effect ML string, meaning that this term may have arbitrary effects (it may loop, do IO, throw exceptions, mutate the heap, etc.), but if it returns, it always returns a string. The effect name ML is chosen to represent the default, implicit effect in all ML programs.

Tot and ML are just two of the possible effects. Some others include: Dv, the effect of a computation that may diverge; ST, the effect of a computation that may diverge, read, write or allocate new references in the heap; Exn, the effect of a computation that may diverge or raise an exception. The effects {Tot, Dv, ST, Exn, ML} are arranged in a lattice, with Tot at the bottom (less than all the others), ML at the top (greater than all the others), and with ST unrelated to Exn. This means that a computation with a particular effect can be treated as having any other effect that is greater than it in the effect ordering—we call this feature sub-effecting.

In fact, you can configure F* with your own family of effects and effect ordering and have F* infer those effects for your programs—but that's more advanced and beyond the scope of this tutorial.

dhh1128 / intent

consider declaring the effects of a function #116