A type system for bounded space and functional in-place update
Martin O. Hofmann · 2000
We show how linear typing can be used to obtain functional programs which modify heap-allocated data structures in place. We present this both as a "design pattern" for writing C-code in a functional style and as a compilation process from linearly typed first-order functional programs into malloc()-free C code. The main technical result is the correctness of this compilation. The crucial innovation over previous linear typing schemes consists of the introduction of a resource type # which controls the number of constructor symbols such as cons in recursive definitions and ensures linear space while restricting expressive power surprisingly little. While the space e#ciency brought about by the new typing scheme and the compilation into C can also be realised by with state-of-the-art optimising compilers for functional languages such as Ocaml [16], the present method provides guaranteed bounds on heap space which will be of use for applications such as languages for embedd...