STACKABILITY IN THE SIMPLY-TYPED CALL-BY-VALUE LAMBDA-CALCULUS

This paper addresses two issues: (1) What it means for a higher-order, eager functional language to be implemented with a single, global, st ack-based environment and (2) how the existence of such an environment can be predicted statically. The central theme is the use of the lamb da-abstraction to control the extent or lifetime of bindings. All prog rams in a higher-order, call-by-name language can be implemented with a stack environment. The reason: soundness of eta-expansion and decurr ying for call-by-name. However, eta-expansion is unsound for call-by-v alue. Hence, we must identify a subset of the simply typed, call-by-va lue lambda-calculus, where the lambda-abstraction can serve as the blo ck construct for a stack implementation. The essence of environment st ackability is that the shape of the environment remains the same befor e and after the execution of an expression. Thus, if a closure is retu rned as a value, the environment trapped in it must be a subenvironmen t of the global environment. This yields a dynamic criterion for stack ability - indeed, it is the downwards funargs criterion of the LISP co mmunity. A safe static criterion can now be found via closure analysis . (C) 1998 Published by Elsevier Science B.V. All rights reserved.