Type-based memory safety without manual memory manage or runtime garbage collection?

Question

Let's say we wanted a typeful, pure functional programming language, like Haskell or Idris, that is aimed at systems programming without garbage collection and has no runtime (or at least not more than the C and Rust "runtimes"). Something that can run, more or less, on bare metal.

What are some of the options for static memory safety that don't require manual memory management or runtime garbage collection, and how might the problem be solved using the type system of a pure functional similar to Haskell or Idris?

Answer 1

Roughly speaking, there are two main strategies for safe manual memory management.

1. The first approach is to use some substructural logic like linear logic to control resource usage. This idea has floated around basically since linear logic's inception, and basically works on the observation that by banning the structural rule of contraction, every variable is used at most once, and so there is no aliasing. As a result, the difference between in-place update and re-allocation is invisible to the program, and so you can implement your language with manual memory management.

   This is what Rust does (it uses an affine type system). If you are interested in the theory of Rust-style languages, one of the best papers to read is Ahmed et al's L3: A Linear Language with Locations. As an aside, the LFPL calculus Damiano Mazza mentioned is also linear, has a full language derived from it in the RAML language.

   If you are interested in Idris-style verification, you should look at Xi et al's ATS language, which is a Rust/L3 style language with support for verification based on Haskell-style indexed types, only made proof-irrelevant and linear to give more control over performance.

   An even more aggressively dependent approach is the F-star language developed at Microsoft Research, which is a full dependent type theory. This language has a monadic interface with pre- and post-conditions in the spirit of Nanevski et al's Hoare Type Theory (or even my own Integrating Linear and Dependent Types), and has a defined subset which can be compiled to low-level C code -- in fact, they are shipping verified crypto code as part of Firefox already!

   To be clear, neither F-star nor HTT are linearly-typed languages, but the index language for their monads are usually based on Reynold and O'Hearn's separation logic, which is a substructural logic related to linear logic that has seen great success as the assertion language for Hoare logics for pointer programs.

2. The second approach is to simply specify what assembly (or whatever low level IR you want) does, and then use some form of linear or separation logic to reason about its behaviour in a proof assistant directly. Essentially, you can use the proof assistant or dependently-typed language as a very fancy macro assembler that only generates correct programs.

   Jensen et al's High-level separation logic for low-level code is a particularly pure example of this -- it builds separation logic for x86 assembly! However, there are many projects in this vein, like the Verified Software Toolchain at Princeton and the CertiKOS project at Yale.

All of these approaches will "feel" like a bit like Rust, since tracking ownership by restricting the usage of variables is key to them all.

Answer 2

Linear types and separation logic are both great, but can require quite a bit of programmer effort. Writing a safe linked list in Rust could be pretty hard, for instance.

But there is an alternative that requires much less programmer effort, although with less strict guarantees. A (pretty old) stream of work is to guarantee memory safety by using (usually a stack of) regions. Using region inference, a compiler can statically decide which region a piece of allocated data should go into, and deallocate the region when it goes out of scope.

Region inference is provably safe (can't deallocate reachable memory) and requires minimal programmer interference, but it is not "total" (i.e. it still can leak memory, although definitely much better than "do nothing"), so it's usually combined with GC in practice. The MLton ML Kit compiler uses regions to eliminate most GC calls, but it still has a GC because it would still leak memory otherwise. According to some of the early pioneers on regions, region inference wasn't actually invented for this purpose (it was for automatic parallelization, I think); but it just turned out it could be used for memory management as well.

For a starting point, I would say go for the paper "Implementation of the Typed Call-by-Value λ-calculus using a Stack of Regions" by Mads Tofte and Jean-Pierre Talpin. For more papers on region inference, look for other papers by M. Tofte and J.-P. Talpin, some of Pierre Jouvelot's work, as well as Greg Morrisett, Mike Hicks, and Dan Grossman's series of papers on Cyclone.

Answer 3

A trivial scheme for the "bare metal" systems is to simply disallow all runtime memory allocations. Remember, even the C malloc/free pair requires a runtime library. But even when all objects are defined at compile time, they can be defined in a typesafe way.

The chief problem here is the fiction of immutable values in pure functional languages, which are created while the program runs. Real hardware (and certainly bare metal systems) rely on mutable RAM, which is in limited supply. The runtime of a functional language implementation in practice dynamically allocates RAM as new "immutable" values are created, and garbage collects them when the "immutable" value is no longer needed.

And for most interesting problems, the lifetime of at least some values depends on runtime (user) input, so lifetimes can't be statically determined. But even if the lifetime doesn't depend on input, it can be highly non-trivial. Take the simple program repeatedly finding primes simply by checking every number in order, checking against all primes up to sqrt(N). Clearly this needs keeps the primes and can recycle the memory used for the non-primes.