Safe is a first-order eager functional language with facilities for programmer-controlled destruction and copying of data structures. It provides also regions, i.e. disjoint parts of the heap where the compiler allocates data structures.
Most functional languages abstract the programmer from the memory management. Should the memory be exhausted, the garbage collector will copy/mark the live part of the heap and will consider the rest as free. This normally implies the suspension of program execution for some time. Occasionally, not enough free memory has been recovered and the program simply aborts.
In some contexts, this scheme may not be acceptable. Safe does not use a garbage collector and is equipped with a set of compile-time analyses aimed at inferring an upper bound on memory consumption. Additionally the compiler will (hopefully) provide a formal certificate proving this property.
The Safe project has been funded by the Spanish grants TIN2004-07943-C04-04 (SELF), S-0505/TIC/0407 (PROMESAS), and is currently funded by the grants TIN2008-06622-C03-01 (STAMP) and S2009/TIC-1465 (PROMETIDOS).
Overview of the Safe language
Safe is a strict functional language whose syntax is similar to that of first-order Haskell, being its main difference the memory management features, namely destructive pattern matching and regions.
Destructive pattern matching
Consider the functional algorithm for appending two lists:
concat (x:xs) ys = x : concat xs ys
In terms of memory consumption, what it really happens when calling the concat function is that a copy of the first list is created and linked with the second list. The input list received as a first parameter is still available after the function's call.
If the first input list is not needed after the appending, its memory can be recovered by using the destructive version of concat:
concat (x:xs)! ys = x : concat xs ys
The exclamation mark (!) after the patterns specifies that, in addition to the pattern matching, the corresponding cons-nil cell will be removed from the heap. In each destructive pattern matching, only the first cell of the cons-nil spine is disposed of; the remaining ones will be removed in the subsequent recursive calls.
Therefore, the destructive version of concat requires no extra heap space
A type system guarantees that this feature is used in a safe way.
Region-based memory management
A region is a part of the memory where a data structure may be built. Region creation and destruction are bound to function calls: a working region is created when entering the function call and removed when exiting it. Those temporary data structures that are not part of function's result may be built there and therefore, will be removed after the function's execution.
As an example, consider the following definition of a list sorting function by using the treesort algorithm:
where mkTree builds a binary search tree with the elements of the list given a as parameter and inorder does an inorder traversal of a binary search tree.
The binary search tree does not belong to the output's result, so it is inferred to live in the working region.
It is inferred by the compiler whether a data structure is built in the working region or not. Regions cannot be handled directly by the programmer.
References
-
M. Tofte, J-P. Talpin
Region-based memory management
Information and Computation, 132(2):109–176, 1997.
Author's page MLKit's home page