Bounded Linear Types in a Resource Semiring
Bounded linear types have proved to be useful for automated resource analysis and control in functional programming languages. In this paper we introduce a bounded linear typing discipline on a general notion of resource which can be modeled in a semiring
- PDF / 346,731 Bytes
- 20 Pages / 439.363 x 666.131 pts Page_size
- 29 Downloads / 186 Views
Abstract. Bounded linear types have proved to be useful for automated resource analysis and control in functional programming languages. In this paper we introduce a bounded linear typing discipline on a general notion of resource which can be modeled in a semiring. For this type system we provide both a general type-inference procedure, parameterized by the decision procedure of the semiring equational theory, and a (coherent) categorical semantics. This could be a useful type-theoretic and denotational framework for resource-sensitive compilation, and it represents a generalization of several existing type systems. As a nontrivial instance, motivated by hardware compilation, we present a complex new application to calculating and controlling timing of execution in a (recursion-free) higher-order functional programming language with local store.
1
Resource-Aware Types and Semantics
The two important things about a computer program are what it computes and what resources it needs to carry out the computation successfully. Correctness of the input-output behavior of programs has been, of course, the object of much research from various conceptual angles: logical, semantical, type-theoretical and so on. Resource analysis has been conventionally studied for algorithms, such as time and space complexity, and for programs has long been a part of research in compiler optimization. An exciting development was the introduction of semantic [1] and especially type theoretic [14] characterizations of resource consumption in functional programming languages. Unlike algorithmic analyses, type based analysis are formal and can be statically checked for implementations of algorithms in concrete programming languages. Unlike static analysis, a typing mechanism is compositional which means that it supports, at least in principle, separate compilation and even a foreign function interface: it is an analysis based on signatures rather than implementations. Linear logic and typing, because of the fine-grained treatment of resourcesensitive structural rules, constitute an excellent framework for resource analysis, especially in its bounded fragment [13], which can logically characterize polynomial time computation. Bounded Linear Logic (BLL) was subsequently extended to improve its flexibility while retaining poly-time [5] and further extensions to linear dependent typing were used to completely characterize complexity of evaluation of functional programs [4]. Z. Shao (Ed.): ESOP 2014, LNCS 8410, pp. 331–350, 2014. c Springer-Verlag Berlin Heidelberg 2014
332
D.R. Ghica and A.I. Smith
Such analyses use time as a motivating example, but can be readily adapted to other consumable resources such as energy or network traffic. What they have in common is a monadic view of resources, tracking their global usage throughout the execution of the term. A complementary view on resource sensitivity is the co-monadic one, as advocated by Melli`es and Tabareau [18]. The intuition is that the type system tracks how much resource a term needs in
Data Loading...
