Names and Bindings

A crucial aspect of a programming language is the mechanism it provides for binding names, which are themselves expressions, to expressions. For instance, a declaration is introduced by the following syntax that declares a binding between the name x, which is also referred to as a variable, and the expression 1+2:

val x = 1 + 2

Note that val is a keyword in ATS, and the declaration is classified as a val-declaration. Conceptually, what happens at run-time in a call-by-value language such as ATS is that the expression 1+2 is first evaluated to the value 3, and then the binding between x and 1+2 is finalized into a binding between x and 3. Essentially, call-by-value means that a binding between a name and an expression needs to be finalized into one between the name and the value of the expression before it can be used in evaluation subsequently. As another example, the following syntax declares three bindings, two of which are formed simultaneously in the first line:

val PI = 3.14 and radius = 10.0
val area = PI * radius * radius

Note that it is unspecified in ATS as to which of the first two bindings is finalized ahead of the other at run-time. However, it is guaranteed that the third binding is finalized after the first two are done.