As a starting point, example from Hofmann's paper:
append l m =
case l of
nil -> m
cons d h t -> cons c h (append t m)
First argument to cons
is a special diamond
type. It's linear and represents the space in memory of the cons cell. Each constructor expects a similar diamond argument.
Can implement cons
in C, where diamond d
is void *d
:
list_t cons(void *d, entry_t hd, list_t tl) {
d->head=hd;
d->tail=tl;
return d;
}
The language described in Hoffman's paper has the property that programs can only use the amount of space provided by their inputs, so there is no allocation and therefore no traditional memory management. This was a feature of that paper, because it apparently captures a space complexity class. But for our purposes, for writing realistic programs, we would want ways of allocating and deallocating memory, and therefore some way of tracking the lifetime of memory resources. This makes the re-use of memory more interesting, in my opinion, because it opens the door to re-using memory not just as a part of algorithm design (as in the in-place list algorithms from Hoffman's paper) but as a decision space for program design and compiler optimization.
A common pattern in low-level C/C++ programming is to have a buffer of memory and re-use it for multiple distinct parts of a program. This allows the program to avoid the overhead of repeated invocations of malloc
and free
(a property shared by moving GC/generational GC as well), but requires some care on the part of the programmer. A language that kept track of memory resource lifetime (by regions, perhaps, or some other mechanism like ordinary linear types) in combination with in-place updates could allow a safe use of this programming pattern.
TODO: more brainstorming here
A Type System for Bounded Space and Functional In-Place Update - Martin Hofmann, ESOP 2000
Multiple papers on Cyclone