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:
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:
Note that it is unspecified in ATS as to which of the first two bindings (connected by the keyword and) 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. To see this issue from a different angle, we can try to typecheck the following code:
The error message reported in this case indicates that the name (or dynamic identifier) x in the expression x + 1 is unbound. In particular, the two occurrences of x in the above code are unrelated.