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

Given a type T and an integer N, the syntax @[T][N] stands for a flat array consisting N elements of the type T. Please note that a value of the type @[T][N] is of the size N*sizeof(T). If a function has a parameter representing an array, then this parameter is most liklely call-by-reference. For instance, the following code implements a function that takes two arrays of doubles to compute their dot product (also knowns as inner product):

fun dotprod ( A: &(@[double][3]) , B: &(@[double][3]) ) : double = ( A[0] * B[0] + A[1] * B[1] + A[2] * B[2] )

Note that both array arguments of dotprod are call-by-reference.