Skip to content

Instantly share code, notes, and snippets.

@vollmerm
Created March 17, 2021 13:00
Show Gist options
  • Save vollmerm/758df689059017c268454d235c9fea9f to your computer and use it in GitHub Desktop.
Save vollmerm/758df689059017c268454d235c9fea9f to your computer and use it in GitHub Desktop.
Some brainstorming on in-place updates and memory layout

In-place updates and memory layout

Diamond types for in-place updates, extended with lifetimes

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.

Tracking memory size and layout in types

TODO: more brainstorming here

Related work

A Type System for Bounded Space and Functional In-Place Update - Martin Hofmann, ESOP 2000

Multiple papers on Cyclone

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment