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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abramsky, S., Jagadeesan, R., Malacaria, P.: Full Abstraction for PCF. Inf. Comput. 163(2), 409–470 (2000)
Atassi, V., Baillot, P., Terui, K.: Verification of ptime reducibility for system F terms: Type inference in dual light affine logic. Logical Methods in Computer Science 3(4) (2007)
Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 445–532. Elsevier and MIT Press (2001)
Burrell, M.J., Cockett, R., Redmond, B.F.: Pola: a language for PTIME programming. In: Workshop on Logic and Computational Complexity, LCC (2009)
Cook, S., McKenzie, P.: Problems complete for deterministic logarithmic space. Journal of Algorithms 8(3), 385–394 (1987)
Dal Lago, U., Schöpp, U.: Functional programming in sublinear space. In: Gordon, A.D. (ed.) Programming Languages and Systems. LNCS, vol. 6012, pp. 205–225. Springer, Heidelberg (2010)
Hermann, M., Kolaitis, P.G.: Computational complexity of simultaneous elementary matching problems. J. Autom. Reasoning 23(2), 107–136 (1999)
Kapur, D., Narendran, P.: Complexity of unification problems with associative-commutative operators. J. Autom. Reasoning 9(2), 261–288 (1992)
Pottier, F., Rémy, D.: The essence of ML type inference. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages, pp. 389–489. MIT Press, Cambridge (2005)
Tidén, E., Arnborg, S.: Unification problems with one-sided distributivity. J. Symb. Comput. 3(1/2), 183–202 (1987)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dal Lago, U., Schöpp, U. (2010). Type Inference for Sublinear Space Functional Programming. In: Ueda, K. (eds) Programming Languages and Systems. APLAS 2010. Lecture Notes in Computer Science, vol 6461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17164-2_26
Download citation
DOI: https://doi.org/10.1007/978-3-642-17164-2_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17163-5
Online ISBN: 978-3-642-17164-2
eBook Packages: Computer ScienceComputer Science (R0)