Left-Values and Call-by-Reference

In its simplest form, a left-value is just a pointer paired with a linear proof attesting to a value (of some type) being stored at the location to which the pointer points. The name left-value stems from such a value being allowed to appear on the left-hand side of an assignment statement (in languages like C). Often, a left-value is intuitively explained as a value with an address attached to it. Note that whatever representation chosen for a left-value must make it possible to identify both the pointer and the linear proof (of some at-view) that are associated with the left-value.

In ATS, the simplest expression representing a left-value is !p, where ! is a special symbol and p a value of the type ptr(L) for some address L. When this expression is typechecked, a proof of T@L for some type T is required to be found among the currently available proofs. I will introduce additional forms of left values gradually.

The default strategy for passing a function argument in ATS is call-by-value. However, it is also allowed in ATS to specify that call-by-reference is chosen for passing a particular function argument. By call-by-reference, it is meant that the argument to be passed must be a left-value and what is actually passed is the address of the left-value (instead of the value stored at the address). For example, the following defined function swap2 makes essential use of call-by-reference:

fn{a:t@ype}
swap2 (
  x1: &a, x2: &a
) : void = let
  val tmp = x1 in x1 := x2; x2 := tmp
end // end of [swap2]

Note that the special symbol & in front of the type of a function argument indicates that the argument needs to be passed according to the call-by-reference strategy. The following code implements swap1 based on swap2:

fn{a:t@ype}
swap1 {l1,l2:addr} (
  pf1: !a @ l1, pf2: !a @ l2 | p1: ptr l1, p2: ptr l2
) : void = swap2 (!p1, !p2)

When the call swap2 (!p1, !p2) is evaluated at run-time, the parameters actually being passed are the two pointers p1 and p2 (rather than the values stored at the locations to which these two pointers point).