Type inference for sublinear space functional programming

Abstract

We consider programming language aspects of algorithms that operate on data too large to fit into memory. In previous work we have introduced intml, a functional programming language with primitives that support the implementation of such algorithms. We have shown that intml can express all logspace functions but have left open the question how easy it is in practice to program typical logspace algorithms in intml. In this paper we develop algorithms for intml type inference. We show that with type inference one can handle programs that could not be reasonably manipulated by hand. We do so by implementing in intml a typical logspace algorithm, a test for acyclicity of undirected graphs. Thus we show that with type inference intml can express typical algorithmic patterns of logspace easily and in a natural way. © 2010 Springer-Verlag.