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

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]

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]

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.