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]

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

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