Type Inference for Sublinear Space Functional Programming

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. The study of algorithms operating on data too large to fit into memory has a long tradition in complexity theory; it comprises in particular the complexity classes LOGSPACE and...

• Type: Journal
• Year: 2010
• Where: APLAS
• Authors: Ugo Dal Lago, Ulrich Schöpp
• Keywords: Algorithms, APLAS 2010, Programming Language, Programming Languages, Type Inference