Stack-Allocated Variables

Given a type T and an address L, how can a proof of the view T@L be obtained in the first place? There are actually a variety of methods for obtaining such proofs in practice, and I present one as follows that is based on stack-allocation of local variables.

In the body of the following function foo, some stack-allocated local variables are declared:

fn foo (): void = let var x0: int // view@(x0): int? @ x0 val () = x0 := 0 // view@(x0): int(0) @ x0 var x1: int = 1 // view@(x1): int(1) @ x1 // // [with] is a keyword in ATS // var y: int with pfy // pfy is an alias of view@(y): int? @ y val () = y := 2 // pfy = view@(y): int(2) @ y var z: int with pfz = 3 // pfz is an alias of view@(z): int(3) @ z in // nothing end // end of [foo]

The keyword var is for declaring a local variable. When a variable is declared, either its type or its initial value needs to be given. If a variable is declared without a type, then the type of its initial value is assumed to be its type. Assume that a variable x is declared of type T. Then the pointer to the location of the variable is denoted by addr@(x), where addr@ is a keyword, and its associated linear proof (of some at-view) can be referred to as view@(x), where view@ is a keyword. A variable is another form of left-value in ATS. In the body of foo, x0 is declared to be a variable of the type int and then it is initialized with the integer 0; x1 is declared to be a variable of the type int that is given the initial value 1; y is declared to be a variable of the type int while pfy is introduced as an alias for view@(y), and then y is initialized with the integer 2; z is declared to be a variable of the type int that is given the initial value 3 while pfz is introduced as an alias for view@(z).

The following code gives an implementation of the factorial function:

fn fact{n:nat} (n: int (n)): int = let fun loop{n:nat}{l:addr} .<n>. (pf: !int @ l | n: int n, res: ptr l): void = if n > 0 then let val () = !res := n * !res in loop (pf | n-1, res) end // end of [if] // end of [loop] var res: int with pf = 1 val () = loop (pf | n, addr@res) // addr@res: the pointer to res in res end // end of [fact]

Note that the variable res holds the intermediate result during the execution of the loop. As res is stack-allocated, there is no garbage generated after a call to fact is evaluated. When this style of programming is done in C, there is often a concern about the pointer to res being derefenced after a call to fact returns, which is commonly referred to as derefencing a dangling pointer. This concern is completely eliminated in ATS as it is required by the type system of ATS that a linear proof of the at-view associated with the variable res be present at the end of legal scope for res. More specifically, if x is a declared variable of the type T, then a linear proof of the view T?@L, where L is the address of x, must be available when typechecking reaches the end of the scope for x. This requirement ensures that a variable can no longer be accessed after the portion of the stack in which it is allocated is reclaimed as no linear proof of the at-view associated with the variable is ever available from that point on.

Arrays in ATS can also be stack-allocated. For instance, the following code allocates two arrays of doubles in the frame of the function main0 and then passes them to dotprod to compute their dot product:

implement main0 () = { // var A = @[double][3](1.0) // initialized with 1.0, 1.0, 1.0 var B = @[double](1.0, 2.0, 3.0) // initialized with 1.0, 2.0, 3.0 // val () = println! ("A * B = ", dotprod (A, B)) // A * B = 6.0 // } (* end of [main0] *)

The at-view associated with the variable A is (@[double][3])@A, where A also refers to the address of the variable A. Similarly, the at-view associated with the variable B is (@[double][3])@B. For the sake of completeness, I mention the syntax for uninitialized arrays as follows: Given a type T and an integer N, the syntax @[T][N]() is for an array consisting of N uninitialized values of type T.

Note that allocating large arrays in the call frame of a function may not be a good practice as doing so can greatly increase the likelihood of stack-overflow at run-time.

It is also allowed in ATS to allocate a closure in the call frame of a function. For instance, the following code implements a function named foo that stores a flat closure-function in a stack-allocated variable named bar:

fun foo ( x: int, y: int ) : int = let // var bar = lam@ (): int => x * y // in bar () end // end of [foo]

Note that the special keyword lam@ should be used to form a flat closure-function. For the sake of completeness, I present another example as follows to show that a recursive closure-function can also be stored in a stack-allocated variable:

fun foo2 ( x: int, y: int ) : int = let // var bar2 = fix@ f (x: int): int => if x > 0 then y + f(x-1) else 0 // in bar2 (x) end // end of [foo]

Note that the special keyword fix@ should be used to form a flat recursive closure-function.

In a setting where dynamic memory allocation is not allowed, stack-allocated closures can play a pivotal role in supporting programming with higher-order functions.