AbstractWe 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 Diamond 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 efficiency 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 embedded systems or automatic certification of resource bounds. We show that the functions expressible in the system are precisely those computable on a linearly space-bounded Turing machine with an unbounded stack. By a result of Cook this equals the complexity class 'exponential time'. A tail recursive fragment of the language captures the complexity class 'linear space'. We discuss various extensions, in particular an extension with FIFO queues admitting constant time catenation and enqueuing, and an extension of the type system to fully-fledged intuitionistic linear logic.
Categories and Subject Descriptors: D.1.1 [Programming Techniques]: Applicative (Functional) Programming; D.3.3 [Programming Languages]: Language Constructs and Features; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages; I.2.2 [Artificial Intelligence]: Automatic Programming
Additional Key Words and Phrases: C, compilers, computational complexity, functional programming, garbage collection, memory organization
Selected references
- Samson Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 111(1-2):3-57, 12 April 1993.
- Erik Barendsen and Sjaak Smetsers. Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Computer Science, 6(6):579-612, December 1996.
- Chih-Ping Chen and Paul Hudak. Rolling your own mutable ADT -- a connection between linear types and monads. In Conference Record of POPL '97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 54-66, Paris, France, 15-17 January 1997.
- Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. Bounded linear logic: a modular approach to polynomial-time. Theoretical Computer Science, 97(1):1-66, 20 April 1992. Fundamental study.
- Y. Lafont. The linear abstract machine. Theoretical Computer Science, 59(1-2):157-180, March 1988.
- Patrick Lincoln and John Mitchell. Operational aspects of linear lambda calculus. In Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 235-246, Santa Cruz, California, 22-25 June 1992. IEEE Computer Society Press.
- John C. Reynolds. Syntactic control of interference. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pages 39-46, Tucson, Arizona, January 1978.
- Mads Tofte and Jean-Pierre Talpin. Region-based memory management. Information and Computation, 132(2):109-176, 1 February 1997.