Amortised Resource Analysis for Lazy Functional Programs
Full text
Hugo Miguel Oliveira Romualdo Sim˜ oes Amortised Resource Analysis for Lazy Functional Programs Departamento de Ciˆ encia de Computadores Faculdade de Ciˆ encias da Universidade do Porto Fevereiro de 2014
Hugo Miguel Oliveira Romualdo Sim˜ oes Amortised Resource Analysis for Lazy Functional Programs Tese submetida ` a Faculdade de Ciˆ encias da Universidade do Porto para obtenc¸ ˜ ao do grau de Doutor em Ciˆ encia de Computadores Supervisors: Prof. M´ ario Florido and Prof. Kevin Hammond Departamento de Ciˆ encia de Computadores Faculdade de Ciˆ encias da Universidade do Porto Fevereiro de 2014
To my wife and sons. v
Acknowledgements I would like to express my deepest thanks to the people who directly contributed to the conclusion of this thesis. First, I would like to thank my supervisors M´ ario Florido and Kevin Hammond for their encouragement, support and optimism. I especially thank Kevin and his wife for a warm welcome and making me feel at home during my stay in bonnie St Andrews together with my wife. My thanks extend to the functional programming group in St Andrews for valuable discussions and, in particular, I would also like to thank Steffen Jost and Armelle Bonenfant, and their respective families, for our hiking trips across Scotland and for putting our shared interests in board gaming into practice. A very special thanks goes to my friends and colleagues Steffen Jost and Pedro Vasconcelos for their continuous help in pursuing a practical approach to the problem of resource analysis for lazy functional programs. Our long collaboration formed the basis for this thesis. I would like to thank M´ ario, Kevin, Steffen and Pedro for reviewing drafts of this thesis, with special thanks to Sandra Alves and Olivier Danvy for also actually volunteering for that task. Many thanks to the external examiners present at my viva, Vasco Thudichum Vasconcelos and Ricardo Pe˜ na, for their kind comments and interesting observations. After my research grant was over, I was able to regularly work on my thesis, while developing mobile applications, thanks to Lu´ ıs Damas and Michel Ferreira at Geolink Lda. Similarly, I would like to thank Eduardo Carqueja at AppGeneration for gracefully handling my indecision over setting the end date of my leave of absence while I was finishing writing this thesis. Financial support is acknowledged from the “Fundac¸ ˜ ao para a Ciˆ encia e Tecnologia”, for the Ph.D. grant SFRH/BD/17096/2004 and for a research grant at project RESCUE (REliable and Safe Code execUtion for Embedded systems) PTDC/EIA/65862/2006, and also from the LIACC (Laboratory of Artificial Intelligence and Computer Science) of the University of Porto, Portugal. Finally, I thank my wife, not only for her unconditional support during this long Ph.D. period, but also for sharing the happiest days of my life together with our three sons. To happiness! vii
Resumo Esta tese descreve a primeira tentativa bem-sucedida, de que temos conhecimento, de definir uma an´ alise est´ atica, automatizada e baseada em sistemas de tipos, capaz de encontrar majorantes relativos ` a quantidade de recursos utilizados em programas funcionais lazy. A avaliac¸ ˜ ao lazy permite melhorar a composic¸ ˜ ao de programas, mas dificulta quase sempre as previs˜ oes de recursos. A nossa an´ alise utiliza a abordagem de amortizac¸ ˜ ao automatizada desenvolvida por Hofmann e Jost, que estava anteriormente restringida ` a avaliac¸ ˜ ao eager. Nesta tese, estendemos este trabalho a sistemas lazy atrav´ es da captura em anotac¸ ˜ oes de tipos dos custos de express˜ oes por avaliar e da amortizac¸ ˜ ao do pagamento destes custos utilizando uma noc¸ ˜ ao de potencial lazy. Apresentamos a nossa an´ alise como um sistema de demonstrac¸ ˜ ao que prevˆ e (em tempo de compilac¸ ˜ ao) a quantidade total de alocac¸ ˜ oes de mem´ oria heap de uma linguagem funcional m´ ınima (incluindo func¸ ˜ oes de ordem superior e tipos de dados recursivos) e definimos um modelo de custos formal baseado na semˆ antica de Launchbury para avaliac¸ ˜ ao lazy. Provamos a correc¸ ˜ ao da nossa an´ alise face ao modelo de custos. A nossa abordagem ´ e ilustrada atrav´ es de derivac¸ ˜ oes de tipos de exemplos representativos e n˜ ao triviais, que foram analisados utilizando um prot´ otipo da implementac¸ ˜ ao da nossa an´ alise. Palavras-chave: avaliac¸ ˜ ao lazy, an´ alise amortizada, an´ alise de recursos, sistema de tipos, call-by-need, an´ alise est´ atica viii
Abstract This thesis describes the first successful attempt, of which we are aware, to define an automatic, type-based static analysis of resource bounds for lazy functional programs. Lazy evaluation allows improved modularity of programs, but often makes resource usage difficult to predict. Our analysis uses the automatic amortisation approach developed by Hofmann and Jost, which was previously restricted to eager evaluation. In this thesis, we extend this work to a lazy setting by capturing the costs of unevaluated expressions in type annotations and by amortising the payment of these costs using a notion of lazy potential. We present our analysis as a proof system for predicting (at compile-time) total heap allocations of a minimal functional language (including higher-order functions and recursive data types) and define a formal cost model based on Launchbury’s natural semantics for lazy evaluation. We prove the soundness of our analysis with respect to the cost model. Our approach is illustrated by type derivations of a number of representative and non-trivial examples that have been analysed using a prototype implementation of our analysis. Keywords: lazy evaluation, amortized analysis, resource analysis, type system, call-byneed, static analysis ix
A.3 Annotatedtypes ..................................104 A.4 Sharingrelation...................................104 A.5 Syntax directed type rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 A.6 Structuraltyperules ................................105 A.7 Potential.......................................106 B.1 Type derivation for a non-strict evaluation example . . . . . . . . . . . . . . . 115 B.2 Type derivation for a lazy-evaluation example . . . . . . . . . . . . . . . . . . 116 B.3 Type derivation for map applied to a list with potential . . . . . . . . . . . . . . 117 B.4 Auxiliary type derivation for map applied to a list with potential . . . . . . . . . 118 B.5 Auxiliary type derivation for map applied to a list with potential (cont.) . . . . . 119 B.6 Type derivation for map applied to a list with no potential . . . . . . . . . . . . 120 B.7 Auxiliary type derivation for map applied to a list with no potential . . . . . . . 121 B.8 Auxiliary type derivation for map applied to a list with no potential (cont.) . . . 122 xvi
List of Theorems and Definitions 4.1 Definition (Bound Variables of Fun Expressions) . . . . . . . . . . . . . . . . 19 4.2 Definition(Freshness) ............................... 20 4.3 Lemma (Invariant Locations Under Evaluation) . . . . . . . . . . . . . . . . . 22 5.1 Definition (Idempotent Types and Idempotent Contexts) . . . . . . . . . . . . 31 5.2 Lemma(Substitution) ............................... 37 5.3 Lemma (CONS Inversion) ............................. 37 5.4 Lemma (ABS Inversion) .............................. 38 5.5 Lemma (Context Splitting) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 5.6 Definition(Potential) ................................ 39 5.7 Lemma (Potential Splitting) . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 5.8 Corollary (Potential Remaining) . . . . . . . . . . . . . . . . . . . . . . . . . . 41 5.9 Corollary (Potential Subtype) . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 5.10 Definition (Type Consistency of Locations) . . . . . . . . . . . . . . . . . . . . 41 5.11 Definition (Type Consistency of Heaps) . . . . . . . . . . . . . . . . . . . . . 42 5.12 Definition (Global Compatibility) . . . . . . . . . . . . . . . . . . . . . . . . . . 42 5.13Theorem(Soundness)............................... 42 5.14 Lemma (Subtyping is a partial order) . . . . . . . . . . . . . . . . . . . . . . . 45 xvii
5.15 Lemma (Idempotent Subtypes) . . . . . . . . . . . . . . . . . . . . . . . . . . 45 5.16 Definition (Reachability) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 5.17 Lemma (Idempotent Cycles) . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 5.18 Theorem (Soundness of the Eager System) . . . . . . . . . . . . . . . . . . . 70 A.1 Definition (Type Consistency of Locations) . . . . . . . . . . . . . . . . . . . . 106 A.2 Definition (Type Consistency of Heaps) . . . . . . . . . . . . . . . . . . . . . 106 xviii
1. Introduction Non-strict functional programming languages, such as Haskell [PAB+99], offer important benefits over more conventional eagerly-evaluated languages in terms of modularity and abstraction [Hug89] through exploiting lazy evaluation. A key practical obstacle to their wider use, however, is that extra-functional properties, such as timeand space-behaviour, are often difficult to determine prior to actually running the program. This is largely because the effects of lazy evaluation are hard to predict without actually running a program, since evaluation order is determined dynamically: reduction is carried out if and when it is found to be needed and consequently memory is allocated only if and when needed. Given this difficulty, providing guarantees about memory usage or time performance would both increase confidence in software reliability and performance of lazily-evaluated programs, and open new resource-critical applications such as real-time, memory-limited systems. Recent advances in static cost analyses, such as sized types [VH05, SHFV07, Vas08] and type-based amortisation [HJ03, HAH11] have enabled the automatic prediction of resource bounds for eager functional programs, including uses of higher-order functions [JLHH10]. This thesis develops a new mechanism, lazy potential, that allows execution costs to be transferred from one point of a program to another, as part of an amortised analysis. By exploiting this mechanism, we are then able to extend type-based amortisation to lazy evaluation, describing a static analysis for determining a-priori worst-case bounds on execution costs (specifically, dynamic memory allocations). Our amortised analysis derives costs with respect to a cost semantics for lazy evaluation that derives from Launchbury’s natural operational semantics of graph reduction [Lau93]. It deals with both first-order and higher-order functions, but does not consider polymorphism. Moreover, the analysis is compositional, i.e. it can be applied to program fragments as well as to complete programs. For simplicity, we restrict our attention to total heap allocation, but previous results have shown that the amortised analysis approach also extends to other 1
2FCUP 999. 1. Introduction countable resources, such as worst-case execution time [JLH+09]. In order to ensure a good separation of concerns, our analysis assumes the availability of Hindley-Milner type information [Mil78]. We extend Hofmann and Jost’s type annotations for capturing potential costs [HJ03] with information about the latent costs of unevaluated expressions. The analysis produces a set of constraints over cost variables that we solve in our prototype implementation using an external LP-solver. We have thus demonstrated all the steps that are necessary to produce a fully-automatic analysis for determining bounds on resource usage for lazily-evaluated programs. Although we do not directly address the issue of algorithmic type reconstruction in this thesis, a prototype implementation∗and previous work in the strict setting [HJ03, JLHH10, HAH11] suggests that our analysis should be fully automatable, e.g. by performing a standard Damas-Milner type inference [DM82] with types decorated with fresh annotation variables and producing a set of linear inequalities that can then be automatically solved by a standard LP solver. No guidance from the programmer is necessary. 1.1 Contributions This thesis makes the following novel contributions: •we present the first successful attempt, of which we are aware, to produce an automatic, efficient, type-based, static analysis with formally guaranteed data-dependent resource bounds for lazy evaluation; •we introduce a cost model for heap allocations for a lazy functional language based on Launchbury’s natural semantics for lazy evaluation [Lau93], and use this as the basis for developing a resource analysis; •we prove the soundness of our analysis with respect to the cost-instrumented semantics; •we develop an analysis for eager functional programs with the purpose of better contrasting the analysis for laziness; and ∗Pedro Vasconcelos implemented in Haskell a publicly accessible web-prototype for our analysis (available at http://www.dcc.fc.up.pt/~pbv/cgi/aalazy.cgi) — a much welcome relief from the burden of manually testing program examples.
FCUP 3 1.1. Contributions 999. •we demonstrate the effectiveness of the analysis by deriving costs for some non-trivial examples. The research on which this thesis is based was done in collaboration with others. In particular, the automatic amortised analysis for lazily-evaluated functional programs has previously been reported in a published paper [SVF+12] which was jointly authored by Pedro Vasconcelos, Steffen Jost, my two supervisors M´ ario Florido and Kevin Hammond, and myself: Hugo Sim˜ oes, Pedro Vasconcelos, M´ ario Florido, Steffen Jost, and Kevin Hammond. Automatic Amortised Analysis of Dynamic Memory Allocation for Lazy Functional Programs. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP’12), pages 165–176, Copenhagen, Denmark, September 2012. The technical differences to the published paper are that this thesis: •fixes a minor problem in the soundness proof (caused by rule LET of our type system); •changes the language to be compatible with Launchbury’s semantics (replaces match with case expressions, removes parentheses of constructor applications and merges letcons with let expressions); •simplifies annotations by replacing the double cost annotations with a single cost annotation (this is possible since we are analysing a monotonic resource: total heap allocations); •restricts the inversion lemmas of Section 5.5.1 to have zero on the turnstile of the type judgements (otherwise those lemmas would not hold); •adds a side-condition to rule WEAK of our type system; •contrasts the lazy system with an eager system that is specifically tailored to emphasise the key elements of the novel analysis; and •illustrates the effectiveness of the analysis with detailed derivations of some non-trivial examples; Note that meanwhile the soundness proof was double checked in detail, since the first five items above forced almost all of the previous technical work (including proofs) to be rewritten in this thesis.
4FCUP 999. 1. Introduction Also in the course of his PhD plan, during the introductory studies on the field of static resource analysis, the author contributed to another paper [SHFV07]: Hugo R. Sim˜ oes, Kevin Hammond, M´ ario Florido, and Pedro Vasconcelos. Using Intersection Types for Cost-Analysis of Higher-Order Polymorphic Functional Programs. In Thorsten Altenkirch and Conor McBride, editors, Revised Selected Papers of the International Workshop on Types for Proofs and Programs (TYPES’06), Nottingham, UK, April, 2006, volume 4502 of Lecture Notes in Computer Science, pages 221–236. Springer, 2007. This paper improves the quality of a previous analysis for eagerly evaluated programs by showing how discrete polymorphism helps reduce the problem of size aliasing. However, since it is not a direct contribution to the field of analysis for lazy evaluation (the core topic of this thesis), the result is simply referenced here. 1.2 Overview In the remainder of this thesis we start by reviewing some related work in Chapter 2. Next, in Chapter 3, we review some background on amortisation, covering the description of the general technique and its application to type-based analyses. Then, in Chapter 4, we define a simple functional language and present a cost model for measuring the total heap allocations under a call-by-need semantics of programs written in this language. In Chapter 5 we develop a type-based amortised analysis for lazy evaluation and provide a soundness proof as the main contribution of this thesis, guaranteeing that the cost bound of the analysis is observed with respect to the cost model. An experimental assessment of the analysis is given in Chapter 6 through a range of illustrative examples. Finally, Chapter 7 concludes.
2. Related Work 2.1 Semantics for Lazy Evaluation We build heavily on Launchbury’s natural semantics for lazy evaluation [Lau93], as subsequently adapted by Sestoft [Ses97], and exploit ideas that were developed by Encina and Pe˜ na [EP02, EP03a]. There is a significant body of other work on the semantics of callby-need evaluation. Pre-dating Launchbury’s work, Josephs [Jos89] gave a denotational semantics of lazy evaluation, using a continuation-based semantics to model sharing, and including an explicit store. However, this approach does not fit well with standard proof techniques. Maraist et al. [MOW98] subsequently defined both natural and reduction semantics for the call-by-need lambda calculus, so enabling equational reasoning, and a similar approach was independently described by Ariola and Felleisen [AF97]. Like Encina and Pe˜ na [EP03a, EP09], Mountjoy [Mou98] derived an operational semantics for the Spineless Tagless G-Machine from the natural semantics of Launchbury and Sestoft, including poly-applicative λ-expressions. The main differences between these approaches are that Encina and Pe˜ na correct some mistakes in Mountjoy’s presentation; that they provide correctness proofs; that their semantics correctly deals with partial applications in the Spineless Tagless G-Machine; that they deal with partial applications as normal forms; and that they consider two distinct implementation variants, based on push/enter versus apply/eval. More recently, Pirog and Biernacki [PB10] have established the equivalence between the Spineless Tagless G-Machine and an extended version of the natural semantics of Launchbury and Sestoft as evidenced by Danvy et al.’s [ADM04] functional correspondence between abstract machines and evaluators. Bakewell and Runciman [BR01] have previously defined an operational semantics for Core Haskell that gives time and space execution costs in terms of Sestoft’s semantics for his 5
6FCUP 999. 2. Related Work Mark 1 abstract machine. The work has subsequently been extended to give a model that can be used to determine space leaks by comparing the space usage for two evaluators using a bisimulation approach [BR00]. Gustavsson and Sands [GS99] have similarly defined a space-improvement relation that guarantees that some optimisation can never lead to asymptotically worse space behaviour for call-by-need programs and Moran and Sands [MS99] have defined an improvement relation for call-by-need programs that can be used to determine whether one terminating program improves another in all possible contexts. Finally, given that compilers for lazy evaluation eventually generate optimised code based on information from strictness analysis [Myc81, BHA86, MN92, WH87] or cheapness analysis [Myc80, Fax00] and thus implement in fact a non-strict semantics rather than call-byneed, it is worth noting an alternative non-strict reduction strategy by Ennals et al. [EP03b, Enn03], called optimistic evaluation, that, in an attempt to improve the average time performance against call-by-need, is based on speculatively evaluating expressions that are considered to be usually used and usually cheap to evaluate and aborting if an embedded profiler determines that it is not the case. Although the approach promised to achieve considerable performance improvements, its development is currently suspended from industrystrenght compilers given the difficulties in maintaining the supporting framework (i.e. speculation, profiling and abortion) while implementing other features. Our own work differs from this body of earlier work in that we provide a cost semantics from which we derive a static analysis to automatically determine upper bounds on the memory requirements of lazily evaluated programs. 2.2 Resource Analyses for Lazy Evaluation Resource analysis based on profiling and manual code inspection has long formed the state-of-the-art and still is current practice in many cases. Indeed, for non-strict functional languages, such as Haskell, ad-hoc techniques, manual analysis or symbolic profiling are the only currently viable approaches: the dynamic demand-driven nature of lazy functional programming creates particular problems for resource analysis, whether manual or automatic. There has therefore been very little work on static resource analysis for lazy functional programs, and, to our knowledge, no previous automatic static analysis has ever been produced. The most significant previous work in the area is that by Sands [San90a,
FCUP 7 2.2. Resource Analyses for Lazy Evaluation 999. San90b], whose PhD thesis proposed a cost calculus for reasoning about sufficient and necessary execution time for lazily evaluated higher-order programs, using an approach based on evaluation contexts [Wad88, San98] to capture information about evaluation degree and appropriate projections [WH87] to project this information to the required approach. Wadler [Wad88] had earlier proposed a similar approach to that taken by Sands, but limited to first-order functions and using only strictness analysis combined with appropriate projections, rather than the neededness analysis that Sands also uses. Around the same time, Bjerner and Holmstr¨ om [BH89] developed an approach using demand analysis which requires, a-priori, a domain structure describing an approximation of the output of the analysed program. A primary disadvantage of such approaches lies in the complexity of the domain structure and associated projections that must be used when analysing even simple data structures such as lists. In contrast, our approach easily extends to algebraic data structures. A secondary disadvantage is that a demand analysis approach requires knowing in advance much information about the output value and, unlike the self-contained analysis we have described, projection-based approaches rely on the existence of a complex and powerful external neededness analysis to determine evaluation contexts for expressions. These are serious practical disadvantages: in fact, to date, we are not aware of any fully automatic static analysis that has been produced using these techniques. Transforming lazy programs into eager ones would be a possible approach to producing an analysis for lazily evaluated programs. The resulting programs would then be analysed using (simpler) techniques for eagerly evaluated programs. Unlike our work, these approaches would suffer from the problems that they would produce very poor quality bounds (many programs requiring a small finite amount of resources under lazy evaluation, would require an infinite amount if evaluated eagerly), that they would be, in general, not cost-preserving, that they would lead to potentially exponential code explosion, and that, because they would alter the program, they would not be suitable for use with standard compilers for lazy functional languages. Perhaps because of such drawbacks, no one appears to have actually done this. Several authors have proposed approaches where programs are annotated with additional cost parameters. For example, Albert et al. [ASV03] describes how to automatically construct recurrence relations by adding extra cost parameters to each function under a call-byname semantics and suggests extending the approach to call-by-need through an additional linearisation phase together with guarded constraints (to handle sharing and so avoid cost
14 FCUP 999. 3. Amortisation analysed, made the approach interesting. Since then, keeping the fundamental idea, their technique has been successfully applied in the analyses of stack usage [Cam09], generic resource metrics [JLH+09], higher-order and polymorphic functions [JLHH10] and in efficiently finding multivariate polynomial bounds [HAH11] through using non-linear potential functions. 3.2.1 Informal Description In the classical amortisation technique, the first step in developing an amortised analysis is to define the potential function — the mapping from configurations to numbers. In Hofmann and Jost’s approach, this corresponds to defining the annotated types the type system will handle. The annotated data types, in particular, carry the contributions of a node in a particular data structure to the overall potential of the memory configuration. For example, a red-black binary tree [Bay72] is a binary tree data structure that is easier to maintain balanced than its regular counterpart. It consists of three possible constructors: a Red and aBlack binary constructors having a left and a right red-black binary tree as arguments, and a zero-arity Leaf constructor. Consider the following annotated data type for red-black binary trees of Ints: RBTree(qr, qb, ql,Int) In a tree with this type, where qr,qband qlare non-negative rational numbers, each Red and Black node contributes with qrand qb, respectively, and each Leaf node contributes with qlto the potential of the tree. Given a tree with nrred nodes, nbblack nodes and nlleaf nodes, the potential of such tree is nr×qr+nb×qb+nl×ql. Note that the potential of the tree is linear with respect to its number of nodes. Restricting to linear potential with respect to the number of constructors in a data structure is common in type systems following the approach of Hofmann and Jost, with a notable exception [HH10, HAH11]. Since our main concern here is to extend the approach to a lazy setting, we keep the linear restriction, leaving as further work the adoption of super-linear bounds in our analysis. Also, recall from Section 3.1 that the goal of any amortised analysis is to find a constant that bounds the fluctuations of the successive actual operation costs (in order to simplify the overall bounding expression). That is the purpose of the annotated type systems following Hofmann and Jost’s approach: to ensure the amortised costs are zero, so that the potential
FCUP 15 3.2. Automatic Amortised Analysis 999. of the initial configuration is an upper bound of the overall actual cost. Once the type system is defined, these type-based amortised analyses obtain their result automatically by performing the following 4 steps: 1) perform a Damas-Milner type inference [DM82] to obtain a type derivation (without annotation variables); 2) decorate the Hindley-Milner types [Mil78] with fresh annotation variables; 3) traverse the type derivation, gathering linear constraints among annotation variables according to the rules of the type system; 4) feed the linear constraints to a standard linear programming solver with the objective of minimising the overall expression cost. Note that only the first or the last step may fail, i.e. either the program being analysed is not well-typed or the gathered linear constraints cannot be solved. Each solution to the generated linear program corresponds to a particular bound on the execution cost. However, these bounds are then only useful provided a correctness guarantee exists. As such, a soundness proof is the key result of these systems, since it establishes the link between cost model and type system. This ensures the run-time actual costs never exceed the compile-time predicted bounds. It is important to note that the analysis produces data-dependent bounds. For example, using an automatic amortised analysis, Loidl and Jost [LJ09] learned that insertion, in their cost model, is generally more expensive for a red-black tree having many black nodes, since coefficient qbwas about 3 times higher than qr. In this thesis we present a type-based amortised analysis for lazy functional programs following Hofmann and Jost’s approach and show its complete development in Chapter 5 — from the chosen annotated types, to the invariants required for the soundness proof.
16 FCUP 999. 3. Amortisation
4. Cost Model In this chapter we present a cost model that allows us to measure total heap allocations. It is given as an operational semantics that formalises the cost of evaluating an expression. We define a cost model for two reasons: to prove the soundness of our analysis (Chapter 5), i.e. to prove that evaluating an expression never costs more than the analysis predicted, and to measure the quality of our analysis against a range of examples (Chapter 6), i.e. to compare the costs of evaluating an expression with the costs predicted by the analysis for the same expression. The cost model we present is built on Encina and Pe˜ na’s corrected version [EP02] of Sestoft’s revision [Ses97] of Launchbury’s natural semantics for lazy evaluation [Lau93]. Launchbury’s semantics forms one of the earliest and most widely-used operational accounts of lazy evaluation for the λ-calculus. Encina and Pe˜ na [EP02] [EP03a] subsequently proved that the Spineless Tagless G-Machine [Jon92] is sound and complete with respect to one of Sestoft’s abstract machines. More recently, Pirog and Biernacki [PB10] have established the equivalence between the Spineless Tagless G-Machine and their extended version of the natural semantics of Launchbury and Sestoft. This equivalence is evidenced by Danvy et al.’s [ADM04] functional correspondence between abstract machines and evaluators. We therefore have a high degree of confidence that the cost model for lazy evaluation developed in this thesis is not just theoretically sound, but also that it could, in principle, be extended to model real implementations of lazy evaluation, such as the GHC implementation of Haskell. Before looking at the cost model in Section 4.3, we will see in detail the operational semantics on which it is based. However, we first need to define the language to be used on both the cost model and the analysis. 17
18 FCUP 999. 4. Cost Model 4.1 Language Syntax The Fun language (Figure 4.1) is similar to the one found in Sestoft’s revision [Ses97] of Launchbury’s natural semantics for lazy evaluation [Lau93]. The reader unfamiliar with the mentioned references should note that arguments to both applications and constructor applications are restricted to variables and that this can be achieved through a process called normalisation [Lau93], which consists of naming the arguments using let expressions. We have thus a normalised λ-calculus extended with (possibly recursive) local bindings, (saturated) constructor applications and case expressions. In contrast to Launchbury and Sestoft’s language, we consider only (for simplicity) singlevariable let-bindings (multiple let-bindings can be encoded, if needed, using pairs and projections). Also, constructor applications appear only in let-bindings as in Encina and Pe˜ na’s semantics for lazy evaluation [EP09]. However, Encina and Pe˜ na’s motivation for such restriction was different from ours: they wanted to be as close as possible to the STG language, while we simply need to distinguish between allocating a constructor and merely referencing an existing one, since these are handled differently by our analysis. As in Sestoft’s language, we do not require bound variables (either lambda-, letor casebound) to be distinct, except that, for each case expression, each element in multiset {−→ xi} must be distinct, for i= 1, . . . , n. For example, case eof c1x y -> x, c2y-> y would be a valid program, whereas the following would not case eof c1x x -> x, c2y-> y 4.2 Operational Semantics Our big-step operational semantics is based on Launchbury’s natural semantics for lazy evaluation [Lau93], as subsequently adapted by Sestoft [Ses97], as corrected for case expressions by Encina and Pe˜ na [EP02]. Figure 4.2 shows the set of rules that define our operational semantics.
FCUP 19 4.2. Operational Semantics 999. – Variables v::= x|y– bound variable |l– free variable (location) – Expressions e::= v– variable |λx. e – lambda abstraction |e v – application |let x=bein e– (possibly recursive) let-binding |case eof {ci−→ xi-> ei}n i=1 – case expression – Augmented expressions be::= c ~v – (saturated) constructor application |e– expression – Weak head normal forms w::= λx. e – lambda abstraction |c~ l– constructor application Figure 4.1: Language Fun Judgements of the form H,S,Lbe⇓w, H′should be read as “in the heap H, (augmented) expression beevaluates to whnf (weak head normal form) w, producing the new heap H′”, where a heap is a partial function mapping distinct variable names to thunks and athunk is an augmented expression (bound in the heap) that may be further evaluated to whnf. Note that, as usual (and seen in Figure 4.1), weak head normal forms are expressions whose outermost structure is a lambda or a constructor. The auxiliary set Lof locations under evaluation was one of the changes introduced by Sestoft∗to improve the renaming mechanism of Launchbury’s semantics. The auxiliary set Swas introduced by Encina and Pe˜ na†in order to fix a freshness property of Sestoft’s rules, and, although in their paper it contains the alternatives of case expressions {ci−→ xi-> ei}n i=1, we simply keep the bound variables of such alternatives, since these are sufficient to fix the problem. We next define the set of bound variables contained in a Fun expression in order to later formalise the notion of freshness of variables. Definition 4.1 (Bound Variables of Fun Expressions).The bound variables of a Fun expression be, denoted by BV(be), are defined in the usual way as shown in Figure 4.3. ∗In [Ses97] this set is called A. †In [EP02] this set is called C.
20 FCUP 999. 4. Cost Model wis in whnf H,S,Lw⇓w, H(WHNF⇓) ℓ6∈ L H,S,L∪ {ℓ}H(ℓ)⇓w, H′ H,S,Lℓ⇓w, H′[ℓ7→ w](VAR⇓) H,S,Le⇓λx. e′,H′H′,S,Le′[ℓ/x]⇓w, H′′ H,S,Le ℓ ⇓w, H′′ (APP⇓) ℓis fresh H[ℓ7→ be[ℓ/x]],S,Le[ℓ/x]⇓w, H′ H,S,Llet x=bein e⇓w, H′(LET⇓) H,S∪Sn i=1 ({−→ xi} ∪ BV(ei)) ,Le⇓ck~ ℓ, H′ H′,S,Lek[~ ℓ/−→ xk]⇓w, H′′ H,S,Lcase eof {ci−→ xi-> ei}n i=1 ⇓w, H′′ (CASE⇓) Figure 4.2: Lazy operational semantics BV(v) = ∅ BV(λx. e) = {x} ∪ BV(e) BV(e v) = BV(e) BV(let x=bein e) = {x} ∪ BV(be)∪BV(e) BV(case eof {ci−→ xi-> ei}n i=1) = BV(e)Sn i=1({−→ xi} ∪ BV(ei)) BV(c ~v) = ∅ Figure 4.3: Bound variables of Fun expressions The following auxiliary definition of freshness of variables is due to Encina and Pe˜ na [EP02]: Definition 4.2 (Freshness).In a judgement H,S,Lbe⇓w, H′a variable is fresh if it is not in dom(H)nor Snor Land it is not bound in either ran(H)or be. Expressions in whnf (lambda abstractions and constructor applications) are already values and should therefore evaluate to themselves, keeping the heap unchanged. This is reflected in rule WHNF⇓. Rule VAR⇓states that in order to evaluate a location ℓ, present in a heap H, we evaluate H(ℓ)with ℓincluded in the set of locations under evaluation. If, as a result, we obtain awhnf wand a heap H′, then evaluating ℓin Hevaluates to the same wand the new heap produced is H′with a mapping updating ℓto w. Note that once ℓis updated its
FCUP 21 4.2. Operational Semantics 999. subsequent accesses obtain the corresponding whnf immediately, effectively implementing sharing of named expressions. Also note that if ℓdepends directly on itself before evaluating to whnf, when attempting to evaluate ℓfor the second time, no rule will apply, since ℓwill be marked as being under evaluation in rule VAR⇓. This situation is known as a “blackhole”: a detectably self-dependent infinite loop. In Launchbury’s semantics, a black-hole is detected by removing ℓfrom the heap before evaluating its contents. Since Sestoft’s revision of the semantics, black-holes can equivalently be detected using the set of locations marked as being under evaluation. In this thesis we need to keep ℓin the heap since the mappings defined for the invariants of our soundness proof in Chapter 5 must apply to all heap locations (regardless of being under evaluation). Thus, we use set Lto detect blackholes (in addition to the benefits that motivated its introduction). The APP⇓rule deals with function applications and, assuming the term is well-typed, evaluation is done in two steps: first, its expression eis evaluated in the original heap, producing a lambda abstraction and an intermediate heap. Then, substituting the lambda variable by the argument of the application, the body of the function is evaluated in the intermediate heap to a final whnf, producing a final heap as well. The LET⇓rule starts by creating a fresh location. Then, the let-bound variable is renamed to this fresh location in all sub-expressions. The location is then allocated to the heap, mapping to the respective augmented expression, and the body of the let is evaluated in this larger heap, with the results being carried over. Finally, rule CASE⇓first evaluates the case discriminant, adding to Sthe bound variables of the case alternatives in order to avoid such variables from being used as locations. Assuming this evaluates to a constructor application in an intermediate heap, then, depending on the constructor that results from the evaluation, the selected alternative is evaluated in the intermediate heap, substituting the formal constructor arguments by the concrete ones. The results of evaluating the alternative are then carried over as the results of evaluating the whole case expression. Note that the set Swas introduced by Encina and Pe˜ na [EP02] to keep freshness locally checkable, a property that motivated Sestoft’s revision [Ses97] to Launchbury’s semantics [Lau93].
22 FCUP 999. 4. Cost Model To illustrate the purpose of set S, consider the following artificial example (in lack of a meaningful short one): case (let s=Succ s in s)of Succ x -> λy. x Note that sis defined as a cyclic successor of itself and that the expected result of evaluating the whole expression is a function that discards its single argument and returns the cyclic successor. However, when evaluating let s=Succ s in s, had the lambda-bound variable ynot been added to set S, we could have chosen yas a fresh location and, although not violating the freshness condition, we would have ended up with the identity function instead as the result, since (with naive substitution) the term λy. x[y/x]is equivalent to λy. y. The set Savoids such variable captures. We now present a lemma that states that the contents of heap locations that are under evaluation are preserved during intermediate evaluations. Lemma 4.3 (Invariant Locations Under Evaluation).If H,S,L⊢be⇓w, H′then for all ℓ∈L we have ℓ∈Hiff ℓ∈H′and if ℓ∈Hthen H′(ℓ) = H(ℓ). Proof. By inspection of the operational semantics (Figure 4.2) we observe that VAR⇓is the only rule that modifies an existing location ℓand that this rule does not apply when ℓ∈L. 4.3 Cost-instrumented Operational Semantics In order to measure the total number of heap allocations of a given program, we have defined a cost model by instrumenting the rules of Figure 4.2 with a non-negative counter as shown in Figure 4.4. In the new rules, judgements of the form H,S,Lmbe⇓w, H′should be read as “in the heap H, expression beevaluates to whnf w, producing the new heap H′, and mnew heap cells have been allocated”. For simplicity, but without loss of generality, we choose a uniform cost-model where evaluation costs one (heap) unit for each fresh heap location (regardless of its content) that is needed during evaluation — essentially counting the number of new locations in the
FCUP 23 4.3. Cost-instrumented Operational Semantics 999. wis in whnf H,S,L0w⇓w, H(WHNF⇓C) ℓ6∈ L H,S,L∪ {ℓ}mH(ℓ)⇓w, H′ H,S,Lmℓ⇓w, H′[ℓ7→ w](VAR⇓C) H,S,Lme⇓λx. e′,H′H′,S,Lm′e′[ℓ/x]⇓w, H′′ H,S,Lm+m′e ℓ ⇓w, H′′ (APP⇓C) ℓis fresh H[ℓ7→ be[ℓ/x]],S,Lme[ℓ/x]⇓w, H′ H,S,L1 + mlet x=bein e⇓w, H′(LET⇓C) H,S∪Sn i=1 ({−→ xi} ∪ BV(ei)) ,Lme⇓ck~ ℓ, H′ H′,S,Lm′ek[~ ℓ/−→ xk]⇓w, H′′ H,S,Lm+m′case eof {ci−→ xi-> ei}n i=1 ⇓w, H′′ (CASE⇓C) Figure 4.4: Cost-instrumented lazy operational semantics heap (i.e. the number of newly allocated locations). We could have chosen other metrics [JLH+09], modelling the usage of other countable resources such as execution time or stack space, but we believe this simplicity has allowed us to focus on the principles needed to develop a resource analysis for call-by-need. Cost-metric refinements are left to further work. The only change introduced in Figure 4.4 with respect to Figure 4.2 is the introduction of the non-negative value above the turnstile. This value corresponds to the cost of evaluation in terms of quantity of heap cells required. We will now describe how the rules in Figure 4.4 affect this total heap allocation counter. As we have seen, rule WHNF⇓leaves the heap unchanged. Thus, no heap cells are allocated in rule WHNF⇓C, corresponding to a cost of zero. In rules APP⇓Cand CASE⇓Cthe cost of evaluation is the sum of the costs of each of the two evaluation steps. Rule VAR⇓Cstates that the cost of evaluating a location ℓis the cost of evaluating the corresponding heap expression H(ℓ). Note that although the resulting heap is updated, ℓ was already in the domain of H′(by Lemma 4.3) and thus no new heap cell was added at that point which justifies the preservation of cost m. Rule LET⇓Cis the only rule that effectively allocates heap cells, costing one heap cell for the
30 FCUP 999. 5. Amortised Analysis .(A| ∅)(SHAREEMPTY) .(X|X,...,X)(SHAREVAR) Bi=µX.c1: (p′ i1,~ Bi1)|···|cm: (p′ im,~ Bim) .~ Aj~ B1j, . . . , ~ Bnj pj≥Pn i=1 p′ ij (1 ≤i≤n, 1≤j≤m) .µX.c1: (p1,~ A1)|···|cm: (pm,~ Am)|B1, . . . , Bn(SHAREDAT) .(Ai|A).(B|Bi)qi≥q(1 ≤i≤n) .A−→ qBA1−→ q1B1, . . . , An−→ qnBn(SHAREFUN) .(Aj|B1j, . . . , Bnj )m=~ A=~ Bi(1 ≤i≤n, 1≤j≤m) .~ A~ B1, . . . , ~ Bn(SHAREVEC) .(A|A1,...,An)qi≥q(1 ≤i≤n) .(Tq(A)|Tq1(A1),...,Tqn (An)) (SHARETHUNK) Figure 5.2: Sharing relation .(Γ | ∅)(SHAREEMPTYCTX) .(A|B1,...,Bn).(Γ |∆) .(x:A, Γ|x:B1,...,x:Bn,∆) (SHARECTX) Figure 5.3: Sharing relation extended to contexts do not. The last three sharing examples fail since in the first of these a typing for yappears only at the right-hand side of the sharing relation; in the second, the potential on the lefthand side is not linearly distributed with respect to the right-hand side (56≤ 3 + 3); and the last example fails since sharing is contravariant in the left argument of functions and thus, while the cost of the outermost thunk type on the right-hand side can exceed the corresponding cost on the left-hand side, the cost of the inner thunk type cannot. 5.2.1 Subtyping Relation Sharing also allows the relaxation of annotations to subsume subtyping. The special case of sharing one type to a single other corresponds to a subtyping relation; we define the shorthand notation A <:Bto mean .(A|B). Inequalities over type annotations in rules SHAREDAT, SHAREFUN and SHARETHUNK allow potential annotations to decrease and cost annotations to increase. Informally, A <:Bimplies not only that Aand Bhave identical
FCUP 31 5.2. Sharing Relation 999. underlying types, but also that Bhas lower or equal potential and greater or equal cost than that of A. As usual in structural subtyping, this relation is contravariant in the left argument of functions (SHAREFUN). 5.2.2 Idempotent Types We now define the notion that some types can be freely shared. Namely, if they observe the following definition: Definition 5.1 (Idempotent Types and Idempotent Contexts).We say type A(respectively context Γ) is idempotent iff .(A|A, A)(respectively .(Γ |Γ,Γ)) holds. This special case occurs when sharing a type or context to itself: because of non-negativity, .(A|A, A)(respectively .(Γ |Γ,Γ)) requires the potential annotations in A(respectively Γ) to be zero for all data types outside of function types. Note though that function types are unaffected by this special case of sharing. However, since function types do not carry potential per se (the potential required to execute the body of a function must come from its arguments), all types subject to such constraint carry no potential. For example, types T1(µX.{Unit:(0,())}) T1(T1(µX.{Unit:(1,())})−→ 1B) T1(µX.{Cons:(0,(T1(µX.{Unit:(0,())}),T1(X))) | Nil:(0,())}) are idempotent, whereas types T1(µX.{Unit:(1,())}) T1(µX.{Cons:(1,(T1(µX.{Unit:(0,())}),T1(X))) | Nil:(0,())}) T1(µX.{Cons:(0,(T1(µX.{Unit:(0,())}),T1(X))) | Nil:(1,())}) are not. We use this property to impose a constraint that types or contexts carry no potential. A variant of this is .(A|A, A′), which implies that A′is a subtype of Athat holds no potential.
32 FCUP 999. 5. Amortised Analysis 5.3 Typing Judgements Our analysis for lazy evaluation is presented in Figures 5.4 and 5.5 as a proof system that derives judgements of the form Γqbe:A, where Γis a typing context, beis an augmented expression, Ais an annotated type and q(above the turnstile) is a non-negative rational number approximating the cost of evaluating be. For simplicity, we will omit turnstile annotations whenever they are not explicitly mentioned. In the LET rule, the cost q′of evaluating beis deferred by moving it to the thunk type of xin the type judgement of e. If xdoes not occur in ethen its cost can be discarded, in accordance with lazy evaluation. Also, type A′is restricted to being idempotent in order to prevent the potential of xfrom being reused in the derivation of be, keeping potential from being obtained for free in the recursive definition. Finally, the overall cost of the let expression is 1for the newly allocated heap cell (according to the cost model) plus the cost qof evaluating the body eand, if beis a constructor, its potential p′is also added to the overall cost. Note that the thunk cost of xin the type judgement of beis q′, instead of always zero as in a previous presentation [SVF+12]. This change allowed us to fix a minor problem in the soundness proof of the main theorem. VAR moves the cost from the thunk type to the turnstile, ensuring that any cost in the thunk type is paid for at this point of access in a type derivation. In the ABS rule, the cost of eventually applying the λ-abstraction is q, but the cost of evaluating the λ-abstraction itself is zero, since it is already a whnf. In order to avoid duplicating potential where a λ-abstraction is applied more than once, ABS ensures that Γ is idempotent, by forcing it to share with itself. While on the one hand this means functions can be reused arbitrarily without risking unsound duplication of potential, on the other hand functions must obtain all their required potential, other than a constant amount, from their input argument xalone and not from other variables in dom(Γ). APP ensures that the argument and function types match and includes the cost of the function in the final result. The CONS rule simply ensures consistency between the arguments and the result type. Since constructors cannot appear in source forms, the rule is used only when we need to assign types either to heap expressions or to evaluation results. Note that while rule LET
FCUP 33 5.3. Typing Judgements 999. Γ, x:Tq′(A′)q′be:A∆, x:Tq′(A)qe:C x6∈ dom(Γ,∆) .(A|A, A′)q′= 0 if beis a whnf p=p′,if be≡c ~y and A=µX.{· · · |c: (p′,~ B)|· · · } 0,otherwise Γ,∆1 + q+plet x=bein e:C(LET) x:Tq(A)qx:A(VAR) Γ, x:Aqe:C x 6∈ dom(Γ) .(Γ |Γ,Γ) Γ0λx.e :A−→ qC(ABS) Γqe:A−→ q′ C Γ, y:Aq+q′e y :C(APP) B=µX.{· · · |c: (p, ~ A)|· · · } y1:A1[B/X],...,yk:Ak[B/X]0c ~y :B(CONS) Γqe:B B =µX.{c1: (p1,−→ A1)|···|cn: (pn,−→ An)} (Sn i=1{−→ xi})∩dom(∆) = ∅ i= 1, . . . , n (|−→ Ai|=|−→ xi|=ki ∆, xi1:Ai1[B/X],...,xiki:Aiki[B/X]q′+piei:C Γ,∆q+q′case eof {ci−→ xi-> ei}n i=1 :C(CASE) Figure 5.4: Syntax directed type rules must ensure that sufficient potential (p′) is available for the constructor, the CONS rule does not — the former corresponds to allocating a constructor, the latter to merely referencing one. The CASE rule deals with pattern-matching over an expression of a (possibly recursive) data type. The rule requires that all branches of the alternatives admit an identical result type and that part of the estimated cost of each alternative branch is the same; fulfilling such a condition may require the relaxation of type and/or cost information using the structural rules described below. The matching branch uses extra resources corresponding to the potential annotation on the matched constructor, previously set aside at the introduction of the constructor (LET). The structural rules of Figure 5.5 allow the analysis to be relaxed in various ways. Rule WEAK allows the introduction of an extra hypothesis in the typing context and the side condition ensures type Amust be structurally equivalent to any of Γ↾x, if Γ↾xis not empty, preventing ill-formed contexts, such as {x:Bool, x:List}. RELAX allows argument costs to be relaxed. SUPERTYPE and SUBTYPE allow supertyping in a hypothesis and subtyping
34 FCUP 999. 5. Amortised Analysis Γqe:C.(A′|(Γ, x:A)↾x) Γ, x:Aqe:C(WEAK) Γq′e:A q ≥q′ Γqe:A(RELAX) Γ, x:Bqe:C A <:B Γ, x:Aqe:C(SUPERTYPE) Γqe:B B <:C Γqe:C(SUBTYPE) Γ, x:A1, x:A2qe:C.(A|A1, A2) Γ, x:Aqe:C(SHARE) Γ, x:Tq′ 0(A)qe:C Γ, x:Tq′ 0+q′(A)q+q′e:C(PREPAY) Figure 5.5: Structural type rules in the conclusion, respectively. SHARE allows the use of sharing to split potential in a hypothesis. Finally, PREPAY allows (part or all of) the cost of a thunk to be paid for, so reducing the cost of further uses. It is important to note that a decrease of cost annotations for thunks (possibly down to zero) can only be achieved through the PREPAY structural rule and not through the sharing rules of Figure 5.2. Without PREPAY the system would model call-by-name, since each access of a variable would pay for the entire cost. Also, if we would force the use of PREPAY for the entire cost after each LET, we would be modelling call-by-value: pay in full once at introduction (LET) and pay zero at every access (VAR). It is the ability to selectively choose when to use PREPAY that enables the system to model call-by-need. Thus, “prepaying” is key to correctly modelling the reduced costs of lazy evaluation by allowing costs to be accounted only once for a thunk, if at all. 5.4 Example: Analysing Call-By-Need We now present type derivations for the examples from Section 4.4 in order to illustrate how the type rules of Figures 5.4 and 5.5 reflect the costs of our operational semantics.
FCUP 35 5.4. Example: Analysing Call-By-Need 999. 5.4.1 Non-Strict Evaluation Recall example (4.1) which demonstrates that unneeded redexes are not reduced (i.e. that the semantics is non-strict): let z=zin (λx. λy.y)z Evaluation of this term in our operational semantics succeeds, requires one heap cell (for allocating the thunk named by z) and the result is the identity function λy.y: H,S,L1let z=zin (λx. λy.y)z⇓λy.y,H′ An analysis for this term is given in Figure 5.6 as an annotated type derivation.∗ The final judgement is: ∅1let z=zin (λx.λy.y)z:Tq(B)−→ qB The annotation in the turnstile of this judgement gives a cost estimate of one heap cell, matching the exact cost of the operational semantics. The type annotation qrepresents the cost of the thunk bound to the concrete argument of the identity function λy.y. The value of qcan be arbitrary. So can type B. Note that type A′is similarly arbitrary, subject only to the side condition .(A′|A′, A′), forbidding circular data for having potential. 5.4.2 Lazy Evaluation The second example (4.2) illustrates the sharing of normal forms, i.e. lazy evaluation: let f=let z=zin (λx. λy.y)z in let i=λx.xin let v=f i in f v Evaluating f v forces the thunk named by f; following evaluation, the location associated with fis updated with a whnf. Subsequent evaluations of fre-use this result. Evaluation of ∗For the complete derivation see Figure B.1 in Appendix B.
36 FCUP 999. 5. Amortised Analysis VAR z:Tq′′A′q′′ z:A′ ... z:Tq′′A′0(λx.λy.y)z:Tq(B)−→ qBLET ∅1let z=zin (λx.λy.y)z:Tq(B)−→ qB where .(A′|A′, A′) Figure 5.6: Type derivation for a non-strict evaluation example the overall expression therefore costs 4 heap cells (as seen in Figure 4.5, Chapter 4): ∅,∅,∅4(4.2) ⇓λx.x,[ℓ07→ λy.y, ℓ17→ λx.x, ℓ27→ λx.x, ℓ37→ ℓ3] The type derivation in Figure 5.7 shows the analysis for this example.† The final type judgement replicates the exact operational cost of 4 heap cells: ∅4(4.2) :B, where B=Tq′(C)−→ q′ C Note that we employ the structural type rule SHARE to allow the function fto be used twice. The duplication is justified since the type of fis idempotent (i.e. it shares to itself). The crucial point in this type derivation that allows us to match the exact operational cost is the use of the structural rule PREPAY (below SHARE) to pay, precisely once, the cost of the thunk bound to f. Also note that although the type derivation constrains B=Tq′(C)−→ q′ Cto be idempotent, i.e. .(B|B, B ), it leaves type Cunconstrained. 5.5 Soundness This section establishes the soundness of our analysis for lazy evaluation with respect to the cost model of Section 4.3. We begin by stating some auxiliary proof lemmas and preliminary definitions, notably formalising the notion of potential. We then define the principal invariants of our system, namely, type consistency and type compatibility relations between a heap configuration of †For the complete derivation see Figure B.2 in Appendix B.
FCUP 37 5.5. Soundness 999. (Figure 5.6,where q= 0) WEAK f:T1(T0 (B)−→ 0B)1let z=zin (λx.λy.y)z:T0 (B)−→ 0B ... i:T0(B)0λx.x:B ... f:T0(T0 (B)−→ 0B), f:T0(T0 (B)−→ 0B),i:T0(B)1let v=f i in f v :BSHARE f:T0(T0 (B)−→ 0B),i:T0(B)1let v=f i in f v :BPREPAY f:T1(T0 (B)−→ 0B),i:T0(B)2let v=f i in f v :BLET f:T1(T0 (B)−→ 0B)3let i=λx.xin ...:BLET ∅4let f= (let z=zin (λx.λy.y)z)in let i=λx.xin let v=f i in f v :B where B = Tq′(C)−→ q′ C Figure 5.7: Type derivation for a lazy-evaluation example the operational semantics and global types, contexts and balance. We conclude with the soundness result proper (Theorem 5.13). 5.5.1 Auxiliary Lemmas The first auxiliary lemma allows us to replace variables in type derivations. Note that because of the lazy evaluation semantics (and unlike the usual substitution lemma for the λ-calculus), we substitute only with variables but not with arbitrary expressions. Also, since our typing contexts are multisets, we need to ensure the simultaneous substitution of all typings of the variable in the context. Lemma 5.2 (Substitution).If Γ, x:A1,...,x:An qbe:Cand x6∈ dom(Γ) and y /∈dom(Γ) ∪ FV(be)then also Γ, y:A1,...,y:An qbe[y/x] : C. Proof. By induction on the height of derivation of Γ, x:A1,...,x:An qbe:C, simply replacing any occurrences of xfor y. The next two lemmas establish inversion properties for constructors and λ-abstractions. Lemma 5.3 (CONS Inversion).If Γ0c ~y :Bthen B=µX.{· · · | c: (p, ~ A)| · · · } and .(Γ |y1:A1[B/X], . . . , yk:Ak[B/X]).
38 FCUP 999. 5. Amortised Analysis Lemma 5.4 (ABS Inversion).If Γ0λx.e :A−→ qCthen there exists Γ′such that .(Γ |Γ′), .(Γ′|Γ′,Γ′),x /∈dom(Γ′)and Γ′, x:Aqe:C. Proof Sketch (for both lemmas). A typing with conclusion Γ0c ~y :Bmust result from axiom CONS followed by (possibly zero) uses of structural rules. Similarly, a typing Γ0λx.e : A−→ qCmust result from an application of the rule ABS followed by (possibly zero) uses of structural rules. The proof follows by induction on the structural rules, considering each rule separately. For rules RELAX and PREPAY induction is trivial since both type judgements have zero on the turnstile. For the remaining structural rules the proof follows by transitivity of the sharing relation. See Section 5.5.6.2 and 5.5.6.3, respectively, for the detailed proofs. Note that, for a typing judgement with any number greater than zero on the turnstile, inversion in our type system would not hold in general. The reason is that two (mutually exclusive) rules might apply. For example x:T1(A)1e:Cmight have premise x:T1(A)0e:Cthrough rule RELAX, or it might have premise x:T0(A)0e:Cthrought rule PREPAY. This is not a problem since the proofs we present in our system do not require inversion lemmas with a number other than zero on the turnstile of the typing judgements. The final auxiliary lemma allows splitting contexts used for typing expressions in whnf according to a split of the result type. Lemma 5.5 (Context Splitting).If Γ0w:A, where wis an expression in whnf and .(A|A1, A2); then there exist Γ1,Γ2such that .(Γ |Γ1,Γ2),Γ10w:A1and Γ20w:A2. Proof Sketch. The proof follows from an application of Lemma 5.3 (if wis a constructor) or Lemma 5.4 (if wis an abstraction) together with the definition of sharing. See Section 5.5.6.4 for the detailed proof. 5.5.2 Global Types, Contexts and Balance We now define some auxiliary mappings that will be necessary for formulating the soundness of our type system. The mapping Mfrom locations to types, written {ℓ17→ A1,...,ℓn7→ An}, records the global type of a location, which accounts for all potential in all references to that location.
FCUP 39 5.5. Soundness 999. We extend subtyping to global types in the natural way, namely M<:M′if and only if dom(M)⊆dom(M′)and for all ℓ∈dom(M)we have M(ℓ)<:M′(ℓ). This relation will be used to assert that the potential assigned to global types is always non-increasing during execution. The mapping Cfrom locations to typing contexts, written {ℓ17→ Γ1,...,ℓn7→ Γn}, associates each location with its global context that justifies its global type. We also extend the projection operation from (local) contexts to global contexts in the natural way: C↾ℓ={ℓ17→ Γ1,...,ℓn7→ Γn}↾ℓ def = (Γ1,...,Γn)↾ℓ Furthermore, we introduce an auxiliary balance (or lazy potential) mapping Bfrom locations to non-negative rational numbers. The balance mapping will be used to keep track of the partial costs of thunks that have been paid in advance by applications of the PREPAY rule. Note that these auxiliary mappings are needed only in the soundness proof of the analysis for bookkeeping purposes, but are not part of the operational semantics — in particular, they do not incur run-time costs. 5.5.3 Potential We now define the potential of an augmented expression with respect to a heap and an annotated type. Definition 5.6 (Potential).The potential assigned to an augmented expression beof type A under heap H, written φH(be:A), is defined in (5.1) within Figure 5.8. The potential of data constructors is obtained by summing the type annotation with the (possibly recursive) potential contributed by each of the arguments. Note how the potential of data constructors is unwrapped from thunk types. The potential of expressions other than data constructors is always zero. Equation (5.2) extends the definition to typing contexts in the natural way. Equation (5.3) defines potential for global contexts, but considers only thunks that are not under evaluation.
46 FCUP 999. 5. Amortised Analysis 5.5.6.2 Inversion Lemma for Constructors Lemma 5.3 (CONS Inversion).If Γ0c ~y :Bthen B=µX.{· · · | c: (p, ~ A)| · · · } and .(Γ |y1:A1[B/X],...,yk:Ak[B/X]). Proof. A typing with conclusion Γ0c ~y :Bmust result from axiom CONS followed by (possibly zero) uses of structural rules. The proof follows by induction on the structural rules, considering each rule separately. For rules RELAX and PREPAY induction is trivial since both type judgements have zero on the turnstile. For the remaining structural rules the proof follows by transitivity of the sharing relation. We now consider each of the remaining structural rules. Case WEAK:We have Γ, xn+1:Cn+1 0c ~y :B. Applying induction to the premise of rule WEAK Γ0c ~y :Bwe obtain B=µX.{· · · |c: (p, ~ A)|· · · } as required for the conclusion, and .(Γ |y1:A1[B/X],...,yk:Ak[B/X]) Let Γ = {x1:C1,...,xn:Cn}. By the definition of sharing (Figure 5.3) we know that .(x1:C1,...,xn:Cn|y1:A1[B/X],...,yk:Ak[B/X]) iff there is a partition ∆1,...,∆nof {y1:A1[B/X],...,yk:Ak[B/X]}such that .(xi:Ci|∆i) holds and dom(∆i)⊆ {xi}, for (1 ≤i≤n). Let ∆n+1 =∅. Since .(xn+1:Cn+1 |∆n+1 )holds (by SHAREEMPTYCTX) and dom(∆n+1)⊆ {xn+1}, again by definition of sharing we have .(Γ, xn+1:Cn+1 |y1:A1[B/X],...,yk:Ak[B/X]) as required.
FCUP 47 5.5. Soundness 999. Case SUPERTYPE:We have Γ, xn+1:C′ n+1 0c ~y :B. The premises of rule SUPERTYPE are Γ, xn+1:Cn+1 0c ~y :Band .C′ n+1 |Cn+1 . Applying induction to Γ, xn+1:Cn+1 0c ~y : Bwe obtain B=µX.{· · · |c: (p, ~ A)|· · · } as required for the conclusion, and .(Γ, xn+1:Cn+1 |y1:A1[B/X],...,yk:Ak[B/X]) Let Γ = {x1:C1,...,xn:Cn}. By the definition of sharing (Figure 5.3) we know that .(x1:C1,...,xn:Cn, xn+1:Cn+1 |y1:A1[B/X],...,yk:Ak[B/X]) iff there is a partition ∆1,...,∆n,∆n+1 of {y1:A1[B/X],...,yk:Ak[B/X]}such that .(xi:Ci|∆i)holds and dom(∆i)⊆ {xi}, for (1 ≤i≤n+ 1). From .C′ n+1 |Cn+1 and .(xn+1:Cn+1 |∆n+1 )by the transitivity of sharing we have .xn+1:C′ n+1 |∆n+1 Thus by definition of sharing we have .Γ, xn+1:C′ n+1 |y1:A1[B/X],...,yk:Ak[B/X] as required. Case SUBTYPE:We have Γ0c ~y :C. The premises of rule SUBTYPE are Γ0c ~y :B and .(B|C). Applying induction to Γ0c ~y :Bwe obtain B=µX.{· · · |c: (p, ~ A)|· · · } and .(Γ |y1:A1[B/X],...,yk:Ak[B/X]) From .(B|C)we know C=µX.{· · · |c: (p′,~ A′)|· · · }
48 FCUP 999. 5. Amortised Analysis where p≤p′and .~ A~ A′. Also, .(yi:Ai[B/X]|yi:A′ i[C/X]) for (1 ≤i≤k). By the transitivity of sharing we obtain .(Γ |y1:A′ 1[C/X],...,yk:A′ k[C/X]) as required. Case SHARE:We have Γ, x:C′0c ~y :B. Applying induction to the premise of rule SHARE Γ, x:C′ 1, x:C′ 20c ~y :Bwe obtain B=µX.{· · · |c: (p, ~ A)|· · · } as required for the conclusion, and .(Γ, x:C′ 1, x:C′ 2|y1:A1[B/X],...,yk:Ak[B/X]) Let Γ = {x1:C1,...,xn:Cn}. By the definition of sharing (Figure 5.3) we know that .(x1:C1,...,xn:Cn, x:C′ 1, x:C′ 2|y1:A1[B/X],...,yk:Ak[B/X]) iff there is a partition ∆1,...,∆n,∆′ 1,∆′ 2of {y1:A1[B/X],...,yk:Ak[B/X]}such that .(xi:Ci|∆i)holds and dom(∆i)⊆ {xi}, for (1 ≤i≤n), and .(x:C′ 1|∆′ 1),.(x:C′ 2|∆′ 2) hold and dom(∆′ 1∪∆′ 2)⊆ {x}. From .(x:C′ 1|∆′ 1)and .(x:C′ 2|∆′ 2)we have .(x:C′ 1, x:C′ 2|∆′ 1,∆′ 2). From .(C′|C′ 1, C′ 2) (also premise of rule SHARE) and the transitivity of sharing we have .(x:C′|∆′ 1,∆′ 2). By definition of sharing we have .(Γ, x:C′|y1:A1[B/X],...,yk:Ak[B/X]) as required. This concludes the proof of the CONS Inversion.
FCUP 49 5.5. Soundness 999. 5.5.6.3 Inversion Lemma for λ-abstractions Lemma 5.4 (ABS Inversion).If Γ0λx.e :A−→ qCthen there exists Γ′such that .(Γ |Γ′), .(Γ′|Γ′,Γ′),x /∈dom(Γ′)and Γ′, x:Aqe:C. Proof. A typing Γ0λx.e :A−→ qCmust result from an application of the rule ABS followed by (possibly zero) uses of structural rules. The proof follows by induction on the structural rules, considering each rule separately. For rules RELAX and PREPAY induction is trivial since both type judgements have zero on the turnstile. For the remaining structural rules the proof follows by transitivity of the sharing relation. We now consider each of the remaining structural rules. Case WEAK:We have Γ, yn+1:Bn+1 0λx.e :A−→ qCand, as a premise of rule WEAK, Γ0λx.e :A−→ qC Applying induction to Γ0λx.e :A−→ qCwe obtain Γ′such that .(Γ |Γ′),.(Γ′|Γ′,Γ′), x /∈dom(Γ′)and Γ′, x:Aqe:C. Let Γ = {y1:B1,...,yn:Bn}. By the definition of sharing (Figure 5.3) we know that .(y1:B1,...,yn:Bn|Γ′) iff there is a partition ∆1,...,∆nof Γ′such that .(yi:Bi|∆i)holds and dom(∆i)⊆ {yi}, for (1 ≤i≤n). Let ∆n+1 =∅. From SHAREEMPTYCTX we have .(yn+1:Bn+1 |∆n+1 ). By the definition of sharing we have .(Γ, yn+1:Bn+1 |Γ′) as required. Case SUPERTYPE:We have Γ, yn+1:B′ n+1 0λx.e :A−→ qCand, as a premise of rule SUPERTYPE, Γ, yn+1:Bn+1 0λx.e :A−→ qC
50 FCUP 999. 5. Amortised Analysis where .B′ n+1 |Bn+1 . Applying induction to Γ, yn+1:Bn+1 0λx.e :A−→ qCwe obtain Γ′ such that .(Γ, yn+1:Bn+1 |Γ′),.(Γ′|Γ′,Γ′),x /∈dom(Γ′)and Γ′, x:Aqe:C. Let Γ = {y1:B1,...,yn:Bn}. By the definition of sharing (Figure 5.3) we know that .(y1:B1,...,yn:Bn, yn+1:Bn+1 |Γ′) iff there is a partition ∆1,...,∆n,∆n+1 of Γ′such that .(yi:Bi|∆i)holds and dom(∆i)⊆ {yi}, for (1 ≤i≤n+ 1). From .B′ n+1 |Bn+1 and .(yn+1:Bn+1 |∆n+1 )by the transitivity of sharing we have .yn+1:B′ n+1 |∆n+1 Thus, by the definition of sharing we obtain .Γ, yn+1:B′ n+1 |Γ′ as required. Case SUBTYPE:We have Γ0λx.e :A′−→ q′ C′and, as a premise of rule SUBTYPE, Γ0λx.e :A−→ qC where .A−→ qCA′−→ q′ C′. Applying induction to Γ0λx.e :A−→ qCwe obtain Γ′such that .(Γ |Γ′),.(Γ′|Γ′,Γ′),x /∈dom(Γ′)and Γ′, x:Aqe:C. From .A−→ qCA′−→ q′ C′we know q≤q′,.(A′|A)and .(C|C′). From Γ′, x:Aqe:Capplying rules SUPERTYPE (with .(A′|A)), RELAX (with q≤q′) and SUBTYPE (with .(C|C′)) we obtain Γ′, x:A′q′e:C′ as required.
FCUP 51 5.5. Soundness 999. Case SHARE:We have Γ, y:B′0λx.e :A−→ qCand, as a premise of rule SHARE, Γ, y:B′ 1, y:B′ 20λx.e :A−→ qC where .(B′|B′ 1, B′ 2). Applying induction to Γ, y:B′ 1, y:B′ 20λx.e :A−→ qCwe obtain Γ′ such that .(Γ, y:B′ 1, y:B′ 2|Γ′),.(Γ′|Γ′,Γ′),x /∈dom(Γ′)and Γ′, x:Aqe:C. Let Γ = {y1:B1,...,yn:Bn}. By the definition of sharing (Figure 5.3) we know that .(y1:B1,...,yn:Bn, y:B′ 1, y:B′ 2|Γ′) iff there is a partition ∆1,...,∆n,∆′ 1,∆′ 2of Γ′such that .(yi:Bi|∆i)holds and dom(∆i)⊆ {yi}, for (1 ≤i≤n), and .(y:B′ 1|∆′ 1)and .(y:B′ 2|∆′ 2)hold, and dom(∆′ 1∪∆′ 2)⊆ {y}. From .(y:B′ 1|∆′ 1)and .(y:B′ 2|∆′ 2)we have .(y:B′ 1, y:B′ 2|∆′ 1,∆′ 2). From .(B′|B′ 1, B′ 2)and the transitivity of sharing we have .(y:B′|∆′ 1,∆′ 2). By definition of sharing we have .(Γ, y:B′|Γ′) as required. This concludes the proof of the ABS Inversion. We now present the proof of Lemma 5.5 (Context Splitting), followed by the proof of Lemma 5.7 (Potential Splitting). 5.5.6.4 Context Splitting Lemma Lemma 5.5 (Context Splitting).If Γ0w:A, where wis an expression in whnf and .(A|A1, A2); then there exist Γ1,Γ2such that .(Γ |Γ1,Γ2),Γ10w:A1and Γ20w: A2. Proof. Expression wis either a constructor application or a λ-abstraction. The proof follows by considering the two cases separately. Z/A A/B B/Z
52 FCUP 999. 5. Amortised Analysis Case w=c ~y:We have Γ0c ~y :Aand .(A|A1, A2). By applying Lemma 5.3 we obtain A=µX.{· · · |c: (p, ~ B)|· · · } and .(Γ |y1:B1[A/X],...,yk:Bk[A/X]). From .(A|A1, A2) we also obtain A1=µX.{· · · |c: (p′,~ B′)|· · · } A2=µX.{· · · |c: (p′′,~ B′′)|· · · } Applying rule CONS we obtain y1:B′ 1[A1/X],...,yk:B′ k[A1/X]0c ~y :A1 y1:B′′ 1[A2/X],...,yk:B′′ k[A2/X]0c ~y :A2 as required, by considering Γ1=y1:B′ 1[A1/X],...,yk:B′ k[A1/X] Γ2=y1:B′′ 1[A2/X],...,yk:B′′ k[A2/X] We are left to prove .(Γ |Γ1,Γ2). Note that by definition of sharing and .(A|A1, A2) .(yi:Bi[A/X]|yi:B′ i[A1/X], yi:B′′ i[A2/X]) for (1 ≤i≤k). Thus, we have .(y1:B1[A/X],...,yk:Bk[A/X]|Γ1,Γ2). By transitivity of sharing we obtain .(Γ |Γ1,Γ2)as required. Case w=λx.e:We have Γ0λx.e :A−→ qCand .A−→ qCA1−→ q1C1, A2−→ q2C2. By applying Lemma 5.4 we obtain Γ′such that .(Γ |Γ′),.(Γ′|Γ′,Γ′),x /∈dom(Γ′)and Γ′, x:Aqe:C. From .A−→ qCA1−→ q1C1, A2−→ q2C2we also obtain .(A1|A),q≤q1,.(C|C1),.(A2|A), q≤q2and .(C|C2). Let Γ1= Γ2= Γ′. From Γ1, x:Aqe:Capplying rules SUPERTYPE (with .(A1|A)), RELAX (with q≤q1), SUBTYPE (with .(C|C1)) and ABS (with .(Γ1|Γ1,Γ1)and x /∈dom(Γ1)) we obtain Γ10λx.e :A1−→ q1C1as required. Also from Γ2, x:Aqe:Capplying rules SUPERTYPE (with .(A2|A)), RELAX (with q≤q2), SUBTYPE (with .(C|C2)) and ABS (with .(Γ2|Γ2,Γ2)and x /∈dom(Γ2)) we obtain Γ20λx.e :A2−→ q2C2as required. We are left to prove .(Γ |Γ1,Γ2). This is equivalent to .(Γ |Γ′,Γ′)and follows from .(Γ |Γ′)
FCUP 53 5.5. Soundness 999. and .(Γ′|Γ′,Γ′)by the transitivity of sharing. We thus conclude the proof of Context Splitting. 5.5.6.5 Potential Splitting Lemma Lemma 5.7 (Potential Splitting).If .(A|A1,...,An)then for all besuch that the potentials are defined, we have φH(be:A)≥PiφH(be:Ai). Proof. First note that the results follow immediately if beis not in whnf or is a λ-abstraction (because potentials are zero in those cases). The potential is also zero if beis a constructor that is part of a cycle (since otherwise it would be undefined). The remaining case is for a constructor with no cycles, i.e. a directed acyclic graph (DAG). The proof is then by induction on the length of the longest path. We have .(A|A1,...,An)and be≡c ~y. Also φH(c ~y:A)is defined. If A=Tq(B)then Ai=Tqi(Bi)for (1 ≤i≤n)and we would proceed to proving φH(c ~y:B)≥PiφH(c ~y:Bi). Otherwise, A=µX.{· · · |c:(p, ~ B)|· · · } and Ai=µX.{· · · |c:(pi,~ B′ i)|· · · } for (1 ≤i≤n). We have to prove φH(c ~y:A)≥PiφH(c ~y:Ai)or in this case the equivalent inequality p+X j φH(H(ℓj):Bj[A/X]) ≥X i (pi+X j φHH(ℓj):B′ ij[Ai/X]) By induction on the shorter paths H(ℓj), we know X j φH(H(ℓj):Bj[A/X]) ≥X iX j φHH(ℓj):B′ ij[Ai/X] From the non-negativity of potential annotations, all that remains to prove is p≥X i pi and that follows from .(A|A1,...,An)by the definition of sharing. This concludes the proof of Potential Splitting.
54 FCUP 999. 5. Amortised Analysis 5.5.6.6 Idempotent Cycles Definition 5.16 (Reachability).The one-step reachability relation ℓ❀Hℓ′between two locations ℓ, ℓ′in a heap Hholds if and only if H(ℓ) = c~ ℓ′′ and ℓ′∈~ ℓ′′. The many-step reachability relation ❀+ His defined as the transitive closure of the one-step reachability relation. Note that reachability only traverses constructors, but not unevaluated locations nor λ-abstractions. This mimics the definition of potential (Definition 5.6). The following lemma shows that, in a consistent configuration, locations within cycles can be assigned global types with zero potential. Because of the way the invariants were defined, any cycles having positive potential must keep this potential within the cycle in order to justify the typing of each subsequent location. Therefore, since this potential cannot affect the types of locations outside the cycle, we can always set the potential within a cycle to zero. Lemma 5.17 (Idempotent Cycles).Let (H,L)be a heap configuration consistent with global types, contexts and balance M,C,B, that is, such that C,B⊢MEM (H,L) : Mand .(M|Γ,C). Then there exist C′,M′such that M<:M′with C′,B⊢MEM (H,L) : M′and .(M′|Γ,C′)such that for all ℓwith ℓ❀+ Hℓwe have .(M′(ℓ)|M′(ℓ),M′(ℓ)) as well. Proof. Consider a cycle consisting of the locations ℓ0,...,ℓn+1 with ℓi❀Hℓi+1 and ℓn+1 = ℓ0. By Definition 5.16 (Reachability) each H(ℓi)must be a constructor of the form ci(...,ℓi+1,...). The type consistency of locations (Definition 5.10) for each ℓimust hold by case LOC1, because constructors are whnfs. Since thunk annotations are irrelevant for LOC1, we omit them in the following for readability. Let M(ℓi) = T(Ai), hence C(ℓi)0ci(...,ℓi+1,...) : Aiby LOC1. By our assumption that recursive types are non-interleaving, the type for the position of ℓi+1 within the constructor ci must be the µ-bound type variable, i.e. Ai=µX.{ · · · |ci: (pi,...T(X)...)|· · · }. Applying Lemma 5.3 (CONS Inversion) we obtain .(C(ℓi)|ℓi+1:T(Ai),...)(5.17)
FCUP 55 5.5. Soundness 999. From (5.17) by the definition of context sharing and subtyping we conclude that there exists A′ isuch that T(A′ i)∈C↾ℓi+1 and A′ i<:Ai. By the definition of global compatibility (Definition 5.12), we have .M(ℓi+1)Γ↾ℓi+1 ,C↾ℓi+1 ; again by definition of subtyping this implies Ai+1 <:A′ i; combining with A′ i<:Aiestablished earlier, we obtain Ai+1 <:A′ i<:Aifor 0≤i≤n(5.18) Because <:is a partial order (Lemma 5.14) and An+1 =A0by definition, it follows from (5.18) that the Ai, A′ imust all be equal. Let Abe this common type of the cycle locations, i.e. M(ℓi) = T(A)for all 0≤i≤n. The compatibility hypothesis for location ℓinow instantiates as follows: .T(A)Γ↾ℓi,T(A),...(5.19) Because each location occurs at least once in the cycle with exactly the global type T(A) we know that any other references in Γor Cmust occur with an idempotent subtype of A, i.e. A′such that A <:A′and .(A′|A′, A′). We can thus set the global type for all locations in the cycle to this self-sharing type A′without disrupting type consistency. 5.5.6.7 Proof of the Soundness Theorem The proof of Theorem 5.13 follows by induction on the lengths of the derivations of (5.6) and (5.5) ordered lexicographically, with the derivation of the evaluation taking priority over the typing derivation. This is required since an induction on the length of the typing derivation alone would fail for the case of unevaluated locations, which prolongs the length of the typing derivation by a typing judgement for the thunk, granted through the type consistency hypothesis. On the other hand, the length of the derivation for the term evaluation never increases, but may remain unchanged where the last step of the typing derivation was obtained by a structural rule. In these cases, the length of the typing derivation does decrease, allowing an induction over the lexicographically ordered lengths of both derivations. We proceed by case analysis of the typing rule used in premise (5.5). Case VAR:We have ℓ:Tq(A)qℓ:Afrom the typing hypothesis (5.5). From the compatibility hypothesis (5.8) we then obtain .M(ℓ)Tq(A),Θ↾ℓ,C↾ℓwhich implies M(ℓ) = Tq′(b A) and .b AA, ¯ Afor some types b A, ¯ Aand annotation q′with q≥q′.
62 FCUP 999. 5. Amortised Analysis and H,S,L⊢e ℓ ⇓w, H′′, respectively. By inversion of rules APP and APP⇓we obtain Γqe:A−→ q′ C(5.41) H,S,L⊢e⇓λx.e′,H′(5.42) H′,S,L⊢e′[ℓ/x]⇓w, H′′ (5.43) By premise (5.9) we assume m≥t+q+q′+φH(Γ, ℓ:A) + φH(Θ) + ΦL H(C) + ΦL H(B) = (t+q′) + q+φH(Γ) + φH(ℓ:A, Θ) + ΦL H(C) + ΦL H(B)(5.44) Inequation (5.44) shows that the bound for msatisfies the requirements for applying induction for expression eusing judgements (5.41) and (5.42); we obtain m′,Γ′,C′,B′,M′and m′′ 1 such that: Γ′0λx.e′:A−→ q′ C(5.45) H,S,Lm′′ 1e⇓λx.e′,H′(5.46) M<:M′(5.47) C′,B′⊢MEM (H′,L) : M′(5.48) .(M′|(Γ′, ℓ:A, Θ,C′)(5.49) m′≥t+q′+φH′λx.e′:A−→ q′ C+φH′(ℓ:A, Θ) + ΦL H′C′+ ΦL H′B′(5.50) m−m′≥m′′ 1(5.51) By Lemma 5.4 (ABS inversion) applied to judgement (5.45) we can assume without loss of generality that .(Γ′|Γ′,Γ′)and Γ′, x:Aq′e′:C; applying Lemma 5.2 (Substitution) we obtain Γ′, ℓ:Aq′e′[ℓ/x] : C(5.52) In order to apply the induction hypothesis to e′[ℓ/x]it remains to show that the bound (5.50) for m′satisfies the premise (5.9). By .(Γ′|Γ′,Γ′)established earlier and Lemma 5.7 (Potential Splitting) we know φH′(Γ′) = 0 and therefore φH′(Γ′, ℓ:A) = φH′(ℓ:A).
FCUP 63 5.5. Soundness 999. By Def. 5.6 (Potential) we know φH′λx.e′:A−→ q′ C= 0; substituting in (5.50) gives us: m′≥t+q′+φH′λx.e′:A−→ q′ C+φH′(ℓ:A, Θ) + ΦL H′C′+ ΦL H′B′ =t+q′+φH′(ℓ:A, Θ) + ΦL H′C′+ ΦL H′B′ =t+q′+φH′Γ′, ℓ:A+φH′(Θ) + ΦL H′C′+ ΦL H′B′ Hence we are able to apply induction on e′[ℓ/x]and obtain: Γ′′ 0w:C(5.53) H′,S,Lm′′ 2e′[ℓ/x]⇓w, H′′ (5.54) M′<:M′′ (5.55) C′′,B′′ ⊢MEM (H′′,L) : M′′ (5.56) .(M′′ |(Γ′′,Θ),C′′ )(5.57) m′′ ≥t+φH′′ (w:C) + φH′′ (Θ) + ΦL H′′ C′′+ ΦL H′′ B′′(5.58) m′−m′′ ≥m′′ 2(5.59) From (5.47) and (5.55) and the transitivity of subtyping we conclude M<:M′′. From (5.46) and (5.54) and rule APP⇓Cwe obtain H,S,Lm′′ 1+m′′ 2e ℓ ⇓w, H′′. From (5.51) and (5.59) we establish proof obligation (5.16), i.e. m−m′′ =m+(−m′+m′)−m′′ = (m−m′)+ (m′− m′′)≥m′′ 1+m′′ 2. Equations (5.53), (5.56), (5.57) and (5.58) establish the remaining proof obligations. This concludes the proof of the APP case. Case CONS:This case cannot occur because the theorem applies only to initial expressions (not augmented expressions). Case CASE:The typing and evaluation premises are Γ,∆q+q′case eof {ci−→ xi-> ei}n i=1 :C(5.60) H,S,L⊢case eof {ci−→ xi-> ei}n i=1 ⇓w, H′′ (5.61)
64 FCUP 999. 5. Amortised Analysis From (5.61) by inversion of rule CASE⇓we obtain: H,S∪ n [ i=1 ({−→ xi} ∪ BV(ei)) ,L⊢e⇓ck~ ℓ, H′(5.62) H′,S,L⊢ek[~ ℓ/−→ xk]⇓w, H′′ (5.63) From (5.60) by inversion of the typing rule CASE we obtain: Γqe:B(5.64) B=µX.{c1: (p1,−→ A1)|···|cn: (pn,−→ An)}(5.65) ( n [ i=1 {−→ xi})∩dom(∆) = ∅(5.66) |−→ Ak|=|−→ xk|=j(5.67) ∆, xk1:Ak1[B/X],...,xkj:Akj[B/X]q′+pkek:C(5.68) From (5.68), (5.66) and (5.67) together with Lemma 5.2 (substitution) we obtain ∆, ℓ1:Ak1[B/X],...,ℓj:Akj[B/X]q′+pkek[~ ℓ/−→ xk] : C(5.69) Let mbe such that m≥t+q+q′+φH(Γ,∆) + φH(Θ) + ΦL H(C) + ΦL H(B) = (t+q′) + q+φH(Γ) + φH(∆,Θ) + ΦL H(C) + ΦL H(B)(5.70) We are now able to apply the induction hypothesis for expression eusing (5.64) and (5.62) and obtain: Γ′0ck~ ℓ:B(5.71) H,S∪ n [ i=1 ({−→ xi} ∪ BV(ei)) ,Lm′′ 1e⇓ck~ ℓ, H′(5.72) M<:M′(5.73) C′,B′⊢MEM (H′,L) : M′(5.74) .(M′|(Γ′,∆,Θ),C′)(5.75) m′≥(t+q′) + φH′(ck~ ℓ:B) + φH′(∆,Θ) + ΦL H′C′+ ΦL H′B′(5.76) m−m′≥m′′ 1(5.77)
FCUP 65 5.5. Soundness 999. From (5.71), by Lemma 5.3 (inversion), we have .(Γ′|l1:Ak1[B/X],...,lj:Akj[B/X]) (5.78) From (5.75) and (5.78), global compatibility can be relaxed to .(M′|(l1:Ak1[B/X],...,lj:Akj[B/X],∆,Θ),C′)(5.79) We now apply induction again, this time for expression ek[~ ℓ/−→ xk]using (5.69), (5.63), (5.74) and (5.79). It remains to show that the bound (5.76) satisfies premise (5.9). By Def. 5.6 (potential) and (5.65) we know φH′(ck~ ℓ:B) = pk+Pj i=1 φH′(ℓi:Aki[B/X]); substituting in (5.76) yields: m′≥t+q′+pk+Pj i=1 φH′(ℓi:Aki[B/X]) + φH′(∆,Θ) + ΦL H′(C′) + ΦL H′(B′) =t+q′+pk+φH′∆, ℓ1:Ak1[B/X],...,ℓj:Akj[B/X]+φH′(Θ) + ΦL H′C′+ ΦL H′B′ Hence we can apply induction and obtain: Γ′′ 0w:C(5.80) H′,S,Lm′′ 2ek[~ ℓ/−→ xk]⇓w, H′′ (5.81) M′<:M′′ (5.82) C′′,B′′ ⊢MEM (H′′,L) : M′′ (5.83) .(M′′ |(Γ′′,Θ),C′′ )(5.84) m′′ ≥t+φH′′ (w:C) + φH′′ (Θ) + ΦL H′′ C′′+ ΦL H′′ B′′(5.85) m′−m′′ ≥m′′ 2(5.86) From (5.73) and (5.82) and the transitivity of subtyping we conclude M<:M′′. From (5.72) and (5.81) and rule CASE⇓Cwe obtain H,S,Lm′′ 1+m′′ 2case eof {ci−→ xi-> ei}n i=1 ⇓w, H′′ From (5.77) and (5.86) we establish proof obligation (5.16), i.e. m−m′′ =m+(−m′+m′)− m′′ = (m−m′)+(m′−m′′)≥m′′ 1+m′′ 2. Equations (5.80), (5.83), (5.84) and (5.85) establish the remaining proof obligations. This concludes the proof of the CASE case.
66 FCUP 999. 5. Amortised Analysis Case WEAK:The typing premise (5.5) reads Γ, x:Aqe:C. By inversion of rule WEAK we obtain Γqe:C. In order to apply the induction hypothesis for this judgement, we note that premise (5.7) (type consistency) holds unchanged; and because .(M|Γ, x:A, Θ,C) implies .(M|Γ,Θ,C)so does (5.8) (global compatibility). The bound (5.9) for the induction also holds because φH(Γ, x:A)≥φH(Γ). We can therefore apply induction to ewith the typing Γqe:Cand obtain all required results for this case. Case RELAX:By the second premise of RELAX follows q−q′≥0and thus we can choose t′=t+q−q′. We apply the induction hypothesis to Γq′e:Afor this t′. Since RELAX is a structural rule, all statements apart from (5.5) and (5.9) remain unchanged. The induction hypothesis thus yields all required conclusions verbatim, except for (5.15). Instead, the induction yields m′≥t′+φH′(w:A) + φH′(Θ) + ΦL H′(C′) + ΦL H′(B′). Unfolding our choice for t′yields m′≥(t+q−q′) + φH′(w:A) + φH′(Θ) + ΦL H′(C′) + ΦL H′(B′). By the second premise of RELAX follows q−q′≥0and thus m′≥t+φH′(w:A) + φH′(Θ) + ΦL H′(C′) + ΦL H′(B′)as required to conclude this case. Case PREPAY:The typing premise is Γ, ℓ:Tq′ 0+q′(A)q+q′e:C By inversion of the rule PREPAY we obtain Γ, ℓ:Tq′ 0(A)qe:C(5.87) Let B′=B[ℓ7→ q′+B(ℓ)], i.e. B′is equal to Bexcept for location ℓwhere it increases by q′. Assuming mas in premise (5.9), we show that it satisfies the requirements for applying induction to (5.87) with the modified B′: m≥t+q+q′+φH(Γ, ℓ:Tq′ 0+q′(A)) + φH(Θ) + ΦL H(C) + ΦL H(B) ≥t+q+φH(Γ, ℓ:Tq′ 0(A)) + φH(Θ) + ΦL H(C) + ΦL HB′ The last inequality holds because φH(ℓ:Tq′ 0+q′(A)) = φH(ℓ:Tq′ 0(A)) by Def. 5.6 (potential) and q′+ ΦL H(B)≥ΦL H(B′); note that the latter is an equality when H(ℓ)is not a whnf. We need to reestablish both global compatibility and type consistency in order to apply
FCUP 67 5.5. Soundness 999. the induction hypothesis. Let Tr(A′) = M(ℓ). By the definition of sharing and global compatibility (5.8) we have .Tr(A′)Tq′ 0+q′(A)and hence q′ 0+q′≥r. Define k= max(r−q′,0), and M′=M[ℓ7→ Tk (A′)]. To establish consistency for M′, note that only the global type of location ℓchanges. Assume that (LOC2) applies, i.e. H(ℓ)is not in whnf and ℓ /∈L, since otherwise the claim is trivial. From the consistency premise (5.7) we have C(ℓ)r+B(ℓ)H(ℓ) : A′(5.88) By the definition of kwe have k+q′= max(r−q′,0)+q′≥r. Hence we can apply rule RELAX to (5.88) and obtain C(ℓ)k+q′+B(ℓ)H(ℓ) : A′ By definition of B′this is equivalent to the required C(ℓ)k+B′(ℓ)H(ℓ) : A′. To establish compatibility for M′we need to show .Tk (A′)Γ↾ℓ,Tq′ 0(A),C↾ℓ From the compatibility premise (5.8) we know .Tr(A′)Γ↾ℓ,Tq′ 0+q′(A),C↾ℓ(5.89) First we show that .Tk (A′)Tq′ 0(A); by definition of sharing, we need to show q′ 0≥k. By definition of k, we have q′ 0≥k⇐⇒ q′ 0≥max(r−q′,0) ⇐⇒ q′ 0≥r−q′∧q′ 0≥0⇐⇒ q′ 0+q′≥r∧q′ 0≥0; the latter holds by non-negativity assumption, while the former holds by the compatibility premise above. For other types Ts (A′′)in either Γ↾ℓor C↾ℓ, observe that Tk (A′)<:Tr(A′)by construction and Tr(A′)<:Ts (A′′)by the original compatibility (5.89). By transitivity we obtain the desired result. Since the other premises remain unchanged, we can therefore apply induction and obtain precisely the results required for the conclusion of this case.
68 FCUP 999. 5. Amortised Analysis Case SHARE:The typing hypothesis is Γ, ℓ:Aqe:C. By inversion of rule SHARE we obtain Γ, ℓ:A1, ℓ:A2qe:Cand .(A|A1, A2). Assuming mas in premise (5.9), we obtain: m≥t+φH(Γ, ℓ:A) + φH(Θ) + ΦL H(C) + ΦL H(B) ≥t+φH(Γ, ℓ:A1, ℓ:A2) + φH(Θ) + ΦL H(C) + ΦL H(B) The last inequality holds by Lemma 5.7 (Potential Splitting) φH(H(ℓ):A)≥φH(H(ℓ):A1) + φH(H(ℓ):A2). We can therefore apply the induction hypothesis to ewith typing premise Γ, ℓ:A1, ℓ:A2qe:Cand obtain as result the required conclusions for the case SHARE. This concludes the proof of this case. Case SUPERTYPE:The type rule gives us Γ, x:Aqe:Cand A <:B. We show that we can apply induction for the premise Γ, x:Bqe:C. Type consistency holds unchanged for the induction; by A <:Band the compatibility premise (5.8) .(M|Γ, x:A, Θ,C), we have .(M|Γ, x:B, Θ,C). The bound (5.9) also holds because φH(x:A)≥φH(x:B)by A <:Band Lemma 5.9. Applying the induction gives us the required conclusions for the case SUPERTYPE. Case SUBTYPE:The type rule gives us Γqe:C; by inversion we obtain Γqe:Band B <:C. Because the context is unchanged, we can apply induction hypothesis directly and obtain: Γ′0w:B(5.90) H,S,Lm′′ e⇓w, H′(5.91) M<:M′(5.92) C′,B′⊢MEM (H′,L) : M′(5.93) .(M′|(Γ′,Θ),C′)(5.94) m′≥t+φH′(w:B) + φH′(Θ) + ΦL H′C′+ ΦL H′B′(5.95) m−m′≥m′′ (5.96) Applying SUBTYPE to (5.90) gives us Γ′0w:Cas required for (5.10). Lemma 5.9 with B <:Cgives us φH′(w:B)≥φH′(w:C); substituting in (5.95) establishes the bound (5.15). Results (5.91), (5.92), (5.93), (5.94) and (5.96) directly establish the remaining proof obli-
FCUP 69 5.6. A System for Eager Evaluation 999. gations for this case. 5.6 A System for Eager Evaluation This section emphasises the key points of the analysis for lazy evaluation developed in this thesis by contrast to the minimal changes needed to derive an analysis for eager evaluation. The complete definitions and figures of the eager system can be seen in Appendix A. First of all, the analysis needs a cost model to be validated against. For that purpose we derive a cost model for eager evaluation from Figure 4.4 by replacing rule LET⇓Cwith the following: ℓis fresh Hℓ7→ be[ℓ/x],S,L∪ {ℓ}m′be[ℓ/x]⇓w′,H′ H′[ℓ7→ w′],S,Lme[ℓ/x]⇓w, H′′ H,S,L1 + m′+mlet x=bein e⇓w, H′′ (EAGERLET⇓C) The new rule EAGERLET⇓Cforces evaluation of bebefore evaluating the body of the let expression. Note that the cost m′of this forced evaluation is immediately added to the overall cost of the let expression while, in a lazy setting, an expression in a new location would only possibly incur a cost if its evaluation was needed indeed. Correspondingly, in rule VAR⇓Cthe cost mis zero since all locations introduced by EAGERLET⇓Cmap to whnfs in the heap if their evaluation terminates. Although it is tempting to simplify the eager semantics (for example, in EAGERLET⇓we could avoid adding to Hthe mapping for ℓwhen evaluating be[ℓ/x]or we could alter rule VAR⇓to remove the update since H′=H′[ℓ7→ w]) we must refrain from doing so, remembering that the purpose of presenting an eager system in this thesis is to be able to contrast it with the lazy system. The fewer the changes, the simpler the contrast. With respect to the type system, from Figures 5.4 and 5.5 we derive a type system suitable for eager evaluation by removing the now unneeded rule PREPAY and by replacing rules LET and VAR with
70 FCUP 999. 5. Amortised Analysis Γ, x:A′q′be:A∆, x:Aqe:C x6∈ dom(Γ,∆) .(A|A, A′)q′= 0 if beis a whnf p= p′,if be≡c ~y and A=µX.{· · · |c: (p′,~ B)|···} 0,otherwise Γ,∆1 + q′+q+plet x=bein e:C (EAGERLET) and x:A0x:A (EAGERVAR) respectively. Since we removed all explicit references to thunk types from the type system, we can also derive for the eager system both a new syntax of allowed types (by removing the thunk types from Figure 5.1) and a new sharing relation (by removing rule SHARETHUNK from Figure 5.2). In order to validate the analysis for eager evaluation against its respective cost model, we alter the invariants needed for the proof of the soundness theorem. We start by removing the now unneeded balance B(lazy potential). Moreover, since we no longer have references to thunk types and there is no need to account for expressions that are simultaneously not in whnf and not under evaluation (set L), we can simplify the definition of potential (Figure 5.8) with respect to thunk types (also removing the auxiliary definitions of potential for global contexts Cand balance B) and furthermore remove case LOC2 from the definition of type consistency of locations (Definition 5.10). The soundness theorem (Theorem 5.13) is restated according to the changes introduced for the eager system in this section: Theorem 5.18 (Soundness of the Eager System).If the following statements hold Γqe:A(5.97) H,S,L⊢e⇓w, H′(5.98) C⊢MEM (H,L) : M(5.99) .(M|(Γ,Θ),C)(5.100)
FCUP 71 5.7. Summary 999. then for all t∈Q+ 0and m∈Nwith m≥t+q+φH(Γ) + φH(Θ) (5.101) there exist Γ′,C′,M′and m′, m′′ ∈Nsuch that the following statements also hold Γ′0w:A(5.102) H,S,Lm′′ e⇓w, H′(5.103) M<:M′(5.104) C′⊢MEM (H′,L) : M′(5.105) .(M′|(Γ′,Θ),C′)(5.106) m′≥t+φH′(w:A) + φH′(Θ) (5.107) m−m′≥m′′ (5.108) Except for EAGERLET, the proof of the eager system is omitted since all cases are similar to (or simpler than) the ones presented in the soundness proof of the lazy system (in Section 5.5.6.7). The proof of the eager system can be seen in the Appendix A.2. Note that, apart from the expected changes to the operational semantics (EAGERLET⇓) and its corresponding type rules (EAGERLET and EAGERVAR), the fundamental difference between the lazy and the eager systems presented in this chapter is rule PREPAY, that allows the lazy system to prepay or otherwise defer the costs of thunks. Without rule PREPAY, the eager system does not need thunk types nor lazy potential (global balance B) and consequently there is no need to handle those in the definitions of sharing, potential and type consistency. 5.7 Summary In this chapter we have presented a type-based amortised analysis of total heap allocations for lazily evaluated programs and proved that its statically determined bounds are not exceeded during run-time. We have also emphasised the key elements needed in the development of this analysis for lazy evaluation by contrasting the lazy system with a specifically tailored eager system.
78 FCUP 999. 6. Experimental Results q0has been prepaid, the cost of applying map1 to gand xs is zero, which is also the cost of ys. Since the output of map1 has type L0(pc, pn,T0(B)) and ys has cost zero, the type for the input list of map2 is T0 L0(pc, pn,T0(B)), the cost of applying map2 to fand ys is zero and the type of the output of map2 is L0(0,0,T0(C)), the same type as the output of progA. Note from the type of map that the extra amounts pcand pnare 3+qf+0+0 and 1+0, respectively. Now we can see where the costs for the second and third parts come from, since 3+qg+qt+pc= 3+qg+qt+(3+qf) = 6+qg+qf+qtand 1+pn= 1+1 = 2. Since the cost of map is an exact match to its operational cost and no expression in progA is unaccounted for, we conclude that the cost formula of progA shown above is accurate. We use a similar argument to demonstrate that the type given for progB also corresponds to its expected cost. The cost formula is now 1+q0+n(4+qg+qf+qt)+1 which we also divide in three parts: 1+q0,n(4+qg+qf+qt)and 1. The first part corresponds again to a fixed cost of 1+q0, but this time the 1corresponds to allocating a heap cell for binding hto the λ-abstraction (λx.let y=g x in f y), while the q0is still prepayment for evaluating xs to whnf. Before looking at the second and third parts, it is useful to reason about the cost of applying function h. We know function hallocates a heap cell for the binding of yto the application of gto argument x, and returns fapplied to y. So, we know hcosts qh= 1+qg+qfto apply. Now going back to the second and third parts of the cost formula of progB, since q0has been prepaid, the specific type for map in progB is T0 T0(T0(A)−→ qhC)−→ 0T0(Lqt(3+qh+qt,1,T0(A))) −→ 0L0(0,0,T0(C)) and it is clear now that the costs for the second and third parts of the cost formula of progB come from the potential assigned to the input list of map, in particular the Cons nodes: 3+qh+qt= 3+(1+qg+qf)+qt= 4+qg+qf+qt. Again, since the cost of map is an exact match to its operational cost and no expression in progB is unaccounted for, we conclude that the cost formula of progB shown above is accurate, indeed showing that our analysis is able to measure deforestation benefits.
FCUP 79 6.3. Infinite Data Structures: cycle 999. 6.3 Infinite Data Structures: cycle This section serves to demonstrate that our static analysis can obtain accurate bounds when applied to definitions of infinite data structures. Consider the following program let append′=λys.λxs.case xs of Nil -> ys, Cons x xs′-> let ws′=append′ys xs′in let ws =Cons x ws′in ws in let cycle =λzs.let zs′=append′zs′zs in zs′in cycle where cycle is a function that, given a finite non-empty list as its argument, generates an infinite list by constructing a copy of the input list and connecting its end back with the beginning, effectively creating a circular list. The function cycle uses the auxiliary append′, which is defined as the classical append, except for having its argument order reversed. This change is necessary since our system only allows potential in the innermost argument of a function (rule ABS of our type system forces context Γto be idempotent) and thus, if we want the cost of applying append to be paid from the potential in the recursive argument, we must swap the order of arguments (as in this example) or use an uncurried version of the function (as we will see in the next section). In our type system we can derive the following type for cycle: T0 Tq0(Lin)−−−→ 1+q0L′ out where Lin =Lqt(2+qt,0, A) L′ out =L0(0,0, A′),with .(L′ out |L′ out,L′ out )and .(A|A, A′) Note that, since the outermost argument ys of append′cannot have potential, the output list of append′cannot have potential as well, since for the case alternative of the Nil branch, the returning expression is ys. However, given that cycle outputs a circular list and our system does not allow circular data structures with (positive) potential§, the restriction on append′does not negatively affect the type of cycle, since we would not expect its output §Note in Figure 5.4 the use of an idempotent type A′in the recursive typing of rule LET.
80 FCUP 999. 6. Experimental Results list L′ out to have potential anyway. We now show that the bounds given by our analysis are tight. According to the type of cycle, we have the following cost formula 1+q0+n(2+qt) where nis the length of zs with n≥1(otherwise, cycle applied to the empty list would fail to terminate). We divide the cost formula into two parts: a fixed part 1+q0and a part that depends on the length of the input list n(2+qt). In the first part, the 1corresponds to the heap allocation for the let-binding of zs′, while the q0corresponds to a prepayment of the cost of evaluating zs to whnf. The second part corresponds to, for each Cons node of xs in append′, the cost of allocating two heap cells for the let-bindings of ws′and ws plus a prepayment for the evaluation of xs′to whnf. Note that ys acts as a reference to a copy of zs and can be seen as a thunk with zero cost, provided the cost of constructing a copy of the Cons nodes of zs has been prepaid for, as in this case. Since we have covered the cost of all the expressions in the program, we conclude that the cost formula shown above is tight, as long as q0and qtare actual costs and not just upper bounds. 6.4 Nested Data Structures: concat In this section we show the applicability of our analysis to nested data structures, using a function concat. The classical list concatenation function is defined as taking a list of lists as its argument and creating a single list by appending each of the inner lists to the previous one. Here, we define the following alternative version to the classical list concatenation, using an auxiliary function appendp: let appendp =λp.case pof Pair xs ys -> case xs of Nil -> ys, Cons x xs′-> let p′=Pair xs′ys in let zs′=appendp p′in let zs =Cons x zs′in zs in
FCUP 81 6.4. Nested Data Structures: concat 999. let concat =λxss.case xss of Nil -> let nil =Nil in nil, Cons xs xss′-> let ys =concat xss′in let p=Pair xs ys in appendp p in concat We choose to define concat with appendp and not with the append′seen in the previous section. While this allows us to show another alternative version of append successfully handled by our analysis and avoids imposing unnecessary constraints on the output list (since the output list can now have potential, unlike the output of append′), appendp does have a higher cost due to the construction of a pair for each call of this uncurried version and this is reflected on the following type for concat concat :T0 Tqo0(Louter)−−→ qo0Lfinal where Louter =Lqot (2+qol +qi0,1+p′ n,Tqi0(Linner)) Linner =Lqit (3+qit +p′ c,0, A) Lfinal =L0(p′ c, p′ n, A) qol =max(qo0, qot) whose derivation uses the following type for appendp T0 P(T0(Linner),T0(L′ final)) −→ 0L′ final where P(A, B) = T0(µX.{Pair : (0,(A, B)) }) L′ final =L0(p′ c,0, A) where qo0and qot are the usual costs of a list (as defined in the introduction of the current chapter), in this case for the outer list of concat, and qi0and qit are the usual costs applied to the inner lists, but taking the maximum of such costs for each of the inner lists of concat, i.e. qi0is an upper bound on the maximum of the costs of evaluating to whnf each of the inner lists (xs) and qit is an upper bound on the maximum of the costs of evaluating to whnf each of the tails of the Cons nodes of the inner lists (xs′). Assuming, for simplicity, that we are not interested in the potential of the output list (p′ c= 0),
82 FCUP 999. 6. Experimental Results the cost formula extracted from the type of appendp is l(3+qit) where lis the length of the first list of the input. We start by explaining how the cost formula relates to the definition of appendp. First note that the type assigned by our analysis assumes that the first list of the input pair costs zero to evaluate to a whnf (or assumes that this cost has been prepaid). Now, looking at the program definition, the cost of the case expression for the pair is equal to the cost of the case expression for the list xs, since p, from its type, costs nothing to evaluate to whnf. We can also see in the type that xs and ys cost zero to evaluate to whnf, and thus, the cost of the case expression for the list is equal to the cost of the Cons case alternative, which in turn, for each Cons node of xs, corresponds to a cost of 3for the three heap cells storing the thunks referenced by p′,zs′and zs, plus the cost of prepaying qit for xs′since appendp expects a pair of lists that cost zero to evaluate to whnf (or have those costs prepaid, as in this case). Note that applying appendp to p′ has no extra cost and that not only zs is in whnf, but also evaluating each of its Cons nodes also has no extra cost, according to the type L′ final of the application appendp p′. We have thus related each expression in the definition of appendp to the cost formula expressed by its type. We now do the same with respect to concat. According to its type, and ignoring, for simplicity, p′ cand p′ n, we have the following cost formula qo0+1+n(2+qol +qi0)+m(3+qit) where nis the length of outer list passed as input to concat and mis the sum of the lengths of the inner lists (m=l1,...,ln). Connecting the cost formula to the definition of concat, we can see that, once applied to a list of lists xss,concat evaluates the case discriminant (costing qo0). When concat reaches the end of the outer list, it costs 1for the heap cell allocated by the let-binding for nil. Meanwhile, we have to consider the cost of each Cons node of the outer list, and it useful to consider its part on the cost formula n(2+qol +qi0)+m(3+qit)as n X i=1 (2+qol +qi0+li(3+qit)) So, for each inner list of the input to concat, it costs 2heap cells to create the two letbindings for ys and p. We also have to pay qol, as the worst case between the cost qot of
FCUP 83 6.5. Known Limitation with Co-Recursive Definitions: fibs 999. evaluating xss′to whnf and the cost qo0that the type of concat expects for its input list. Furthermore, we prepay the cost qi0of xs, since the type of appendp expects a list with no cost, and pay the cost li(3+qit)of applying appendp to p. Thus, we have related each expression in the definition of concat to the cost formula expressed by its type. Note that mis the sum of the lengths of the inner lists, taking each length separately into account, and thus it does not introduce a source of relaxation on the cost, unlike, for example, if we had considered m as n×max(l1,...,ln). The cost formula for concat is an exact match to its operational cost, provided qo0,qot,qi0,qit and qol are exact values and not just upper bounds, and therefore the quality of the bounds is the best we could hope for¶. 6.5 Known Limitation with Co-Recursive Definitions: fibs Non-strict functional languages allow the use of an idiom that consists of concisely defining an infinite list where, other than a finite number of initial elements, each element depends on previous ones. The classical definition of the Fibonacci series is an example of such idiom and is written in Haskell as fibs = 0 : 1 : zipWith (+) fibs (tail fibs) Unfortunately, although fibs has a linear cost with respect to the number of elements needed from this infinite list, our analysis cannot capture that fact and cannot find a solution for this example. In fact, we have found that our analysis cannot handle such examples and we discuss the difficulties in the remainder of this section. In order to isolate the problem, we highlight the difficulties with what we believe to be one of the simplest examples of this idiom, concisely written in Haskell as bools =True :map not bools ¶Note that, by definition, qot,qit and qol are likely to be a source of relaxation of the cost. However, this loss of precision is expected of any static analysis, since it results from the need to create a single abstraction to represent an infinity of concrete data.
84 FCUP 999. 6. Experimental Results and translated into our Fun language as let true =True in let false =False in let not =λb.case bof True -> false,False -> true in let map =λf.λxs.case xs of Nil -> let nil =Nil in nil, Cons x xs′-> let y=f x in let ys′=map f xs′in let ys =Cons y ys′in ys in let bools =let bls′=map not bools in let bls =Cons true bls′in bls in bools The bools example defines an infinite list of alternating booleans (arbitrarily starting with True) where each element, other than the first, is defined as the negation of the preceeding element. We start by observing that bools yields a constant cost for each successive element (and thus has a linear cost with respect to its length). Evaluating bools to a whnf, in order to access its first element, costs 2, corresponding to the allocation of two heap cells that hold the thunk map not bools and the whnf Cons true bls′. Each subsequent element costs 3 heap allocations, corresponding to the three lets in the Cons branch of function map. Given this reasoning, we would like to obtain a typing such as bools :T2 L3(0,0,T0(Bool)), where Bool def =µX.{True : (0,()) | False : (0,()) }. Recall the type of map, for input lists without potential, as shown in Section 6.1: T0 T0(A′−→ qfB)−→ 0Tql(L′ in)−−−−−−−−−−−−−−→ 3+qf+ql+max(p′ c, p′ n−2) Lout where L′ in =Lql(0,0, A′),with .(A′|A′, A′) Lout =L3+qf+ql +p′ c(p′ c, p′ n,T0(B)) Applying to this concrete example: A′=T0(Bool),qf= 0 (since applying not to a boolean has zero cost), B=Bool and, for simplicity, assuming we are not interested in having
FCUP 85 6.5. Known Limitation with Co-Recursive Definitions: fibs 999. potential in the output list, p′ c= 0 and p′ n= 0. We thus have T0 T0(T0(Bool)−→ 0Bool)−→ 0Tql(L′ in)−−−→ 3+qlLout where L′ in =Lql(0,0,T0(Bool)) Lout =L3+ql(0,0,T0(Bool)) Since in bools the output list of map is passed back again as the input list, the types Lout and L′ in must match, but then our analysis fails to produce a type for bools due to the impossibility of finding a finite solution to ql= 3+ql(the costs in L′ in and Lout). However, the real problem with this co-recursive definition is that, because of lazy evaluation, the cost of the recursive call of map (3 + ql) is shared with the cost of obtaining each element of the output list (also 3+ ql). Unfortunately, the rules of our type system (including PREPAY) are not enough to track the circular sharing dependencies which would allow lowering the costs of thunk types. Therefore, we conclude that our analysis cannot handle such examples of co-recursive functions. It is important to note that bools can be rewritten in a way for which our analysis obtains accurate results. For example, in the translation to our Fun language of the following Haskell code bools =iter not True where iter f x =x:iter f (f x) bools has type T3+pc L3+pc(pc, pn,T0(Bool)) where any potential in the Cons nodes pcmust be paid for from the costs of evaluating bools, and subsequent tails, to its whnf, while the potential in the Nil node pnhas no restriction since bools never creates such node. We could do better and rewrite bools as a circular definition having constant overall cost, such as let true =True in let false =False in let bools =let bls′=Cons false bools in let bls =Cons true bls′in bls in bools
86 FCUP 999. 6. Experimental Results (in Haskell it could be written as bools =True :False :bools), which has type T2 L0(0,0,T0(Bool)) and thus, although here we could not have potential in bools if we wanted tok, this version has better cost. While we believe the remaining examples with linear cost of this idiom can also be rewritten in a way our analysis can handle, such reformulations might not feel natural for some examples. We would like to avoid forcing programmers out of this style when using our analysis and we will pursue a solution to this problem as further work. 6.6 Summary In this chapter we have shown how our analysis provides accurate cost bounds for functions such as map,cycle and concat, thus covering examples of higher-order functions and the use of infinite and nested data structures. We have also seen how our analysis can hint into which alternative program definition has better operational cost. Remember though, that all static analyses are doomed to fail for some programs and we did show some examples that in particular our analysis finds problematic. Some limitations such as that of append have simple workarounds by swapping the order of arguments or using an uncurried version, but each has its drawbacks: restricted output potential or increased cost of uncurrying the input. Other limitations are left as further work, such as the one found on the co-recursive definitions of the previous section and the one that restricts our analysis to programs with linear costs with respect to the number of constructors in data structures. kCircular data structures in our system cannot have potential other than zero. This is similar to the restriction found in the output of function cycle in Section 6.3.
7. Conclusion In this chapter we summarise the work described in this thesis and note the limitations of our approach together with a discussion of further work. 7.1 Assessment of Achievements Analyses for lazily evaluated programs were restricted to first-order programs or were not automatic or depended on context information currently impractical to obtain or made the relation between costs and inputs more opaque by not expressing data-dependencies in the bounds. This thesis has introduced the first automatic static analysis for accurately determining bounds on the execution costs of lazy functional programs. The analysis uses an amortised analysis technique that is capable of directly analysing higher-order lazy programs, without requiring defunctionalisation or other non-cost-preserving program transformations. Our analysis deals with user-defined (potentially infinite) data structures and data-dependencies are expressed in the produced bounds. We have presented a soundness proof, validating the analysis against an operational semantics derived from Launchbury’s natural semantics of graph reduction, and analysed in detail some non-trivial examples of lazy evaluation using the rules of our system, while providing a URL to a web-prototype implementation of the analysis where more examples can be found and users can try their own. From our novel analysis for lazy evaluation we have derived with minimal changes an analysis for eager evaluation, clearly highlighting the key element of our result: a type rule (PREPAY) that allows costs to be deferred. 87
94 FCUP 999. BIBLIOGRAPHY [BFGY08] V´ ıctor Braberman, Federico Fern´ andez, Diego Garbervetsky, and Sergio Yovine. Parametric Prediction of Heap Memory Requirements. In Proceedings of the International Symposium on Memory Management (ISMM’08), pages 141–150, Tucson, Arizona, USA, June 2008. ACM. 2.4 [BH89] Bror Bjerner and S¨ oren Holmstr¨ om. A compositional approach to time analysis of first order lazy functional programs. In Proceedings of the ACM SIGPLAN Conference on Functional Programming Languages and Computer Architecture (FPCA’89), London, UK, September 1989. 2.2 [BHA86] Geoffrey L. Burn, Chris Hankin, and Samson Abramsky. Strictness analysis for higher-order functions. Science of Computer Programming, 7:249–278, 1986. 2.1 [BR00] Adam Bakewell and Colin Runciman. A Model for Comparing the Space Usage of Lazy Evaluators. In Proceedings of the 2nd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP’00), pages 151–162, Montreal, Quebec, Canada, September 2000. 2.1 [BR01] Adam Bakewell and Colin Runciman. A Space Semantics for Core Haskell. In Graham Hutton, editor, ACM SIGPLAN Haskell Workshop 2000, volume 41 of Electronic Notes in Theoretical Computer Science. Elsevier, 2001. 2.1 [Cam08] Brian Campbell. Type-based amortized stack memory prediction. PhD thesis, Laboratory for Foundations of Computer Science, School of Informatics, University of Edinburgh, UK, 2008. 2.3, 7.2, 7.3 [Cam09] Brian Campbell. Amortised Memory Analysis Using the Depth of Data Structures. In Giuseppe Castagna, editor, Proceedings of the European Symposium on Programming (ESOP’09), York, UK, March, 2009, volume 5502 of Lecture Notes in Computer Science, pages 190–204. Springer, 2009. 2.3, 3.2 [CNPQ08] Wei-Ngan Chin, Huu Hai Nguyen, Corneliu Popeea, and Shengchao Qin. Analysing Memory Resource Bounds for Low-Level Programs. In Proceedings of the International Symposium on Memory Management (ISMM’08), pages 151–160, Tucson, Arizona, USA, June 2008. ACM. 2.4 [CW00] Karl Crary and Stephanie Weirich. Resource Bound Certification. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming
FCUP 95 BIBLIOGRAPHY 999. Languages (POPL’00), pages 184–198, Boston, Massachusetts, USA, January 2000. 2.3 [Dan08] Nils Anders Danielsson. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In Proceedings of the ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL’08), pages 133–144, San Francisco, California, USA, January 2008. 2.2 [DM82] Lu´ ıs Damas and Robin Milner. Principal type-schemes for functional programs. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL’82), pages 207–212, Albuquerque, New Mexico, USA, January 1982. 1, 3.2.1 [DMMZ12] Olivier Danvy, Kevin Millikin, Johan Munk, and Ian Zerny. On Inter-deriving Small-step and Big-step Semantics: A Case Study for Storeless Call-by-need Evaluation. Theoretical Computer Science, 435(0):21–42, 2012. 7.3 [Enn03] Robert Ennals. Adaptive Evaluation of Non-Strict Programs. PhD thesis, King’s College, University of Cambridge, December 2003. 2.1 [EP02] Alberto de la Encina and Ricardo Pe˜ na. Proving the Correctness of the STG Machine. In Thomas Arts and Markus Mohnen, editors, Selected papers of the International Workshop on Implementation of Functional Languages (IFL’01), Stockholm, Sweden, September, 2001, volume 2312 of Lecture Notes in Computer Science, pages 88–104. Springer, 2002. 2.1, 4, 4.2, †, 4.2, 4.2 [EP03a] Alberto de la Encina and Ricardo Pe˜ na. Formally Deriving an STG Machine. In Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP’03), pages 102–112, Uppsala, Sweden, August 2003. ACM. 2.1, 4 [EP03b] Robert Ennals and Simon Peyton Jones. Optimistic Evaluation: an adaptive evaluation strategy for non-strict programs. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP’03), pages 287–298, Uppsala, Sweden, August 2003. 2.1 [EP09] Alberto de la Encina and Ricardo Pe˜ na. From Natural Semantics to C: a Formal Derivation of two STG Machines. Journal of Functional Programming, 19(1):47– 94, 2009. 2.1, 4.1
96 FCUP 999. BIBLIOGRAPHY [Fax00] Karl-Filip Fax´ en. Cheap eagerness: Speculative evaluation in a lazy functional language. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP’00), pages 150–161, Montreal, Canada, September 2000. 2.1 [GS99] J¨ orgen Gustavsson and David Sands. A Foundation for Space-Safe Transformations of Call-by-Need Programs. In Andrew D. Gordon and Andrew M. Pitts, editors, Third International Workshop on Higher Order Operational Techniques in Semantics, volume 26 of Electronic Notes in Theoretical Computer Science. Elsevier, 1999. 2.1 [HAH11] Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. Multivariate Amortized Resource Analysis. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’11), pages 357–370, Austin, Texas, USA, January 2011. 1, 2.3, 3.2, 3.2.1, 5.1, 7.2, 7.3 [HBH+07] Christoph A. Herrmann, Armelle Bonenfant, Kevin Hammond, Steffen Jost, Hans-Wolfgang Loidl, and Robert Pointon. Automatic amortised worst-case execution time analysis. In Proceedings of the 7th International Workshop on Worst-Case Execution Time (WCET) Analysis, pages 13–18, Pisa, Italy, July 2007. 2.3 [HH10] Jan Hoffmann and Martin Hofmann. Amortized Resource Analysis with Polynomial Potential. In Giuseppe Castagna, editor, Proceedings of the European Symposium on Programming (ESOP’10), Paphos, Cyprus, March, 2010, volume 6012 of Lecture Notes in Computer Science, pages 287–306. Springer, 2010. 2.3, 3.2, 3.2.1 [HJ03] Martin Hofmann and Steffen Jost. Static Prediction of Heap Space Usage for First-Order Functional Programs. In Proceedings of the ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL’03), pages 185–197, New Orleans, Louisiana, USA, January 2003. 1, 2.3, 3.2, 7.2, 7.3 [HJ06] Martin Hofmann and Steffen Jost. Type-Based Amortised Heap-Space Analysis. In Peter Sestoft, editor, Proceedings of the European Symposium on Programming (ESOP’06), Vienna, Austria, March, 2006, volume 3924 of Lecture Notes in Computer Science, pages 22–37. Springer, 2006. 2.3, 7.3
FCUP 97 BIBLIOGRAPHY 999. [Hof11] Jan Hoffmann. Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis. PhD thesis, LMU Munich, Germany, 2011. 7.2 [Hop08] Catherine Hope. A Functional Semantics for Space and Time. PhD thesis, University of Nottingham, UK, 2008. 2.2 [HR09] Martin Hofmann and Dulma Rodriguez. Efficient Type-Checking for Amortised Heap-Space Analysis. In Proceedings of the CSL: Annual Conference of the European Association for Computer Science Logic, Coimbra, Portugal, September, 2009, volume 5771 of Lecture Notes in Computer Science, pages 317–331. Springer, 2009. 2.3 [Hug89] John Hughes. Why Functional Programming Matters. The Computer Journal, 32(2):98–107, 1989. 1 [JLH+09] Steffen Jost, Hans-Wolfgang Loidl, Kevin Hammond, Norman Scaife, and Martin Hofmann. “Carbon Credits” for Resource-Bounded Computations Using Amortised Analysis. In Ana Cavalcanti and Dennis R. Dams, editors, FM 2009: Formal Methods, Eindhoven, The Netherlands, November, 2009, volume 5850 of Lecture Notes in Computer Science, pages 354–369. Springer, 2009. 1, 2.3, 3.2, 4.3, 7.1, 7.2, 7.3 [JLHH10] Steffen Jost, Hans-Wolfgang Loidl, Kevin Hammond, and Martin Hofmann. Static Determination of Quantitative Resource Usage for Higher-Order Programs. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’10), pages 223–236, Madrid, Spain, January 2010. 1, 2.3, 3.2, 5.1, 5.5.5, 6.2, 7.1, 7.2, 7.2, 7.3 [Jon92] Simon Peyton Jones. Implementing Lazy Functional Languages on Stock Hardware: The Spineless Tagless G-Machine. Journal of Functional Programming, 2(2):127–202, 1992. 4 [Jos89] Mark B. Josephs. The semantics of lazy functional languages. Theoretical Computer Science, 68(1):105–111, 1989. 2.1 [Jos10] Steffen Jost. Automated Amortised Analysis. PhD thesis, Faculty of Mathematics, Computer Science and Statistics, LMU Munich, Germany, 2010. 2.3, 5.5.5, 7.1, 7.2, 7.2, 7.3
98 FCUP 999. BIBLIOGRAPHY [KCL+10] Gabriele Keller, Manuel M.T. Chakravarty, Roman Leshchinskiy, Simon Peyton Jones, and Ben Lippmeier. Regular, shape-polymorphic, parallel arrays in haskell. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP’10), pages 261–272, Baltimore, Maryland, USA, September 2010. 7.3 [Lau93] John Launchbury. A Natural Semantics for Lazy Evaluation. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’93), pages 144–154, Charleston, South Carolina, USA, January 1993. 1, 1.1, 2.1, 4, 4.1, 4.2, 4.2 [LJ09] Hans-Wolfgang Loidl and Steffen Jost. Improvements to a Resource Analysis for Hume. In Proceedings of the 1st International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA), Eindhoven, The Netherlands, November 2009. Springer. 3.2.1 [Mat98] Ralph Matthes. Extensions of System F by Iteration and Primitive Recursion on Monotone Induction Types. PhD thesis, LMU Munich, Germany, 1998. 5.1, 7.2 [Mil78] Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, 1978. 1, 3.2.1 [MML+10] Simon Marlow, Patrick Maier, Hans-Wolfgang Loidl, Mustafa K. Aswad, and Phil Trinder. Seq no more: Better strategies for parallel haskell. In Proceedings of the third ACM SIGPLAN Haskell Symposium, pages 91–102, Baltimore, Maryland, USA, 2010. ACM. 7.3 [MN92] Alan Mycroft and Arthur Norman. Optimising compilation — lazy functional languages. In Proceedings of the 19th Software Seminar (SOFSEM),ˇ Zdiar, Czechoslovakia, 1992. 2.1 [MNPJ11] Simon Marlow, Ryan Newton, and Simon Peyton Jones. A monad for deterministic parallelism. In Proceedings of the fourth ACM SIGPLAN Haskell Symposium, pages 71–82, Tokyo, Japan, 2011. ACM. 7.3 [Mou98] Jon Mountjoy. The Spineless Tagless G-machine, naturally. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP’98), pages 163–173, Baltimore, Maryland, USA, September 1998. 2.1
FCUP 99 BIBLIOGRAPHY 999. [MOW98] John Maraist, Martin Odersky, and Philip Wadler. The Call-by-Need Lambda Calculus. Journal of Functional Programming, 8:275–317, May 1998. 2.1 [MS99] Andrew Moran and David Sands. Improvement in a Lazy Context: An Operational Theory for Call-by-Need. In Proceedings of the ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL’99), pages 43–56, San Antonio, Texas, USA, January 1999. 2.1 [MT91] Robin Milner and Mads Tofte. Co-induction in relational semantics. Theoretical Computer Science, 87(1):209–220, 1991. 5.5.5 [Myc80] Alan Mycroft. The theory and practice of transforming call-by-need into call-byvalue. In Proceedings of the International Symposium on Programming, Paris, France, April, 1980, volume 83 of Lecture Notes in Computer Science, pages 269–281. Springer, 1980. 2.1 [Myc81] Alan Mycroft. Abstract interpretation and optimising transformations for applicative programs. PhD thesis, Department of Computer Science, University of Edinburgh, UK, 1981. 2.1 [Oka98] Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998. 2.3, 3.2 [PAB+99] Simon Peyton Jones (editor), Lennart Augustsson, Brian Boutel, F. Warren Burton, Joseph H. Fasel, Andrew D. Gordon, Kevin Hammond, John Hughes, Paul Hudak, Thomas Johnsson, Mark P. Jones, John C. Peterson, Alastair Reid, and Philip Wadler. Report on the Non-Strict Functional Language, Haskell (Haskell98). Technical report, Yale University, 1999. 1 [PB10] Maciej Pirog and Dariusz Biernacki. A Systematic Derivation of the STG Machine Verified in Coq. In Proceedings of the third ACM SIGPLAN Haskell Symposium, pages 25–36, Baltimore, Maryland, USA, 2010. ACM. 2.1, 4 [Rey72] John C. Reynolds. Definitional Interpreters for Higher-Order Programming Languages. In Proceedings of the ACM National Conference, pages 717–740. ACM, August 1972. 2.2 [San90a] David Sands. Calculi for Time Analysis of Functional Programs. PhD thesis, Imperial College, University of London, September 1990. 2.2
100 FCUP 999. BIBLIOGRAPHY [San90b] David Sands. Complexity Analysis for a Lazy Higher-Order Language. In Neil Jones, editor, Proceedings of the European Symposium on Programming (ESOP’90), Copenhagen, Denmark, May, 1990, volume 432 of Lecture Notes in Computer Science, pages 361–376. Springer, 1990. 2.2 [San98] David Sands. Computing with contexts: A simple approach. In Andrew D. Gordon, Andrew M. Pitts, and Carolyn L. Talcott, editors, Second Workshop on Higher-Order Operational Techniques in Semantics, volume 10 of Electronic Notes in Theoretical Computer Science. Elsevier, 1998. 2.2 [Ses97] Peter Sestoft. Deriving a Lazy Abstract Machine. Journal of Functional Programming, 7(3):231–264, 1997. 2.1, 4, 4.1, 4.2, ∗, 4.2 [SHFV07] Hugo R. Sim˜ oes, Kevin Hammond, M´ ario Florido, and Pedro Vasconcelos. Using Intersection Types for Cost-Analysis of Higher-Order Polymorphic Functional Programs. In Thorsten Altenkirch and Conor McBride, editors, Revised Selected Papers of the International Workshop on Types for Proofs and Programs (TYPES’06), Nottingham, UK, April, 2006, volume 4502 of Lecture Notes in Computer Science, pages 221–236. Springer, 2007. 1, 1.1 [SVF+12] Hugo Sim˜ oes, Pedro Vasconcelos, M´ ario Florido, Steffen Jost, and Kevin Hammond. Automatic Amortised Analysis of Dynamic Memory Allocation for Lazy Functional Programs. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP’12), pages 165–176, Copenhagen, Denmark, September 2012. 1.1, 2.3, 5.3, 7.3 [Svv07] Olha Shkaravska, Ron van Kesteren, and Marko van Eekelen. Polynomial Size Analysis of First-Order Functions. In Proceedings of the 8th International Conference on Typed Lambda Calculi and Applications (TLCA’07), Paris, France, June, 2007, volume 4583 of Lecture Notes in Computer Science, pages 351–365. Springer, 2007. 2.3 [Tar85] Robert E. Tarjan. Amortized computational complexity. SIAM Journal on Algebraic and Discrete Methods, 6(2):306–318, April 1985. 2.3, 3.1, ∗, 3.2 [THLPJ98] Phil W. Trinder, Kevin Hammond, Hans-Wolfgang Loidl, and Simon Peyton Jones. Algorithm + strategy = parallelism. Journal of Functional Programming, 8(1):23–60, 1998. 7.3
FCUP 101 BIBLIOGRAPHY 999. [Vas08] Pedro Baltazar Vasconcelos. Space cost analysis using sized types. PhD thesis, School of Computer Science, University of St Andrews, November 2008. 1 [VH05] Pedro B. Vasconcelos and Kevin Hammond. Inferring Cost Equations for Recursive, Polymorphic and Higher-Order Functional Programs. In Phil Trinder, Greg J. Michaelson, and Ricardo Pe˜ na, editors, Revised Papers of the International Workshop on Implementation of Functional Languages (IFL’03), Edinburgh, UK, September, 2003, volume 3145 of Lecture Notes in Computer Science, pages 88–101. Springer, 2005. 1 [Wad88] Philip Wadler. Strictness Analysis aids Time Analysis. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL’88), pages 119–132, San Diego, California, USA, January 1988. 2.2 [Wad92] Philip Wadler. The Essence of Functional Programming. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’92), pages 1–14, Albuquerque, New Mexico, USA, January 1992. 2.2 [WH87] Philip Wadler and John Hughes. Projections for Strictness Analysis. In Proceedings of the ACM SIGPLAN Conference on Functional Programming Languages and Computer Architecture (FPCA’87), Portland, Oregon, USA, September 1987. 2.1, 2.2
102 FCUP 999. BIBLIOGRAPHY
A. A System for Eager Evaluation A.1 Definitions and Figures wis in whnf H,S,Lw⇓w, H(WHNF⇓) ℓ6∈ L H,S,L∪ {ℓ}H(ℓ)⇓w, H′ H,S,Lℓ⇓w, H′[ℓ7→ w](VAR⇓) H,S,Le⇓λx. e′,H′H′,S,Le′[ℓ/x]⇓w, H′′ H,S,Le ℓ ⇓w, H′′ (APP⇓) ℓis fresh Hℓ7→ be[ℓ/x],S,L∪ {ℓ}be[ℓ/x]⇓w′,H′ H′[ℓ7→ w′],S,Le[ℓ/x]⇓w, H′′ H,S,Llet x=bein e⇓w, H′′ (EAGERLET⇓C) H,S∪Sn i=1 ({−→ xi} ∪ BV(ei)) ,Le⇓ck~ ℓ, H′ H′,S,Lek[~ ℓ/−→ xk]⇓w, H′′ H,S,Lcase eof {ci−→ xi-> ei}n i=1 ⇓w, H′′ (CASE⇓) Figure A.1: Eager operational semantics 103
110 FCUP 999. A. A System for Eager Evaluation If be[ℓ/x]is in whnf :Evaluation (A.5) terminates immediately by WHNF⇓and we have w′=be[ℓ/x]and H1=H′=H2. We use rule WEAK⇓Cto obtain H1,S,L10be[ℓ/x]⇓w′,H′(A.21) We intend to apply the induction hypothesis over the term e[ℓ/x], so we must establish the required premises first. Let C2=C[ℓ7→ Γ, ℓ:A′]and M2=M[ℓ7→ A]. Type consistency (5.99) is extended to C2⊢MEM (H2,L) : M2by case (LOC1) of Definition A.2, using (A.3) and the fact that q′= 0 from premise of rule EAGERLET (5.97). Compatibility .(M2|(∆, ℓ:A, Θ),C2)follows from (5.100), ℓbeing suitably fresh, .(A|A, A′) from premise of rule EAGERLET (5.97), and Definition 5.12 (Global Compatibility). Since expression be[ℓ/x]is in whnf, it can either be a constructor application or a λ-abstraction. We now consider each case separately. If be[ℓ/x]is in whnf and be[ℓ/x]≡c ~y:From premise m≥t+ 1 + q′+q+p+φH(Γ,∆) + φH(Θ) (5.101) we want to derive m2≥(t+ 1 + q′) + q+φH2(∆, ℓ:A) + φH2(Θ) and for that purpose we have to show t+ 1 + q′+q+p+φH(Γ,∆) + φH(Θ) ≥(t+ 1 + q′) + q+ φH2(∆, ℓ:A) + φH2(Θ), or equivalently p+φH(Γ,∆) + φH(Θ) ≥φH2(∆, ℓ:A) + φH2(Θ). First note that φH(Γ,∆,Θ) = φH2(Γ,∆,Θ) since ℓis suitably fresh, and thus we just have to show p+φH2(Γ) ≥φH2(ℓ:A). Since type A′is idempotent by premise of EAGERLET (5.97), we have φH2(ℓ:A′) = 0 and thus p+φH2(Γ) = p+φH2(Γ, ℓ:A′). From Lemma 5.3 (CONS Inversion) applied to (A.3) we obtain .(Γ, ℓ:A′|y1:A1[B/X],...,yk:Ak[B/X]). By Lemma 5.7 generalised to contexts, we then have φH2(Γ, ℓ:A′)≥φH2(y1:A1[B/X],...,yk:Ak[B/X]) and thus p+φH2(Γ, ℓ:A′)≥p+φH2(y1:A1[B/X],...,yk:Ak[B/X]). Finally, by the definition of potential (Figure A.7) we have φH2(ℓ:A) = p+φH2(y1:A1[B/X],...,yk:Ak[B/X]) and thus obtain what was needed to prove p+φH2(Γ) ≥φH2(ℓ:A). We have all the premises required to apply the induction hypothesis over e[ℓ/x], obtaining m′ 2,Γ′ 2,C′ 2,M′ 2and m′′ 2such that: Γ′ 20w:C(A.22) H2,S,Lm′′ 2e[ℓ/x]⇓w, H′′ (A.23)
FCUP 111 A.2. Proof of the Soundness Theorem for the Eager System 999. M2<:M′ 2(A.24) C′ 2⊢MEM (H′′,L) : M′ 2(A.25) .(M′ 2|(Γ′ 2,Θ),C′ 2)(A.26) m′ 2≥(t+ 1 + q′) + φH′′ (w:C) + φH′′ (Θ) (A.27) m2−m′ 2≥m′′ 2(A.28) Let Γ′= Γ′ 2,M′=M′ 2and C′=C′ 2. Equations (A.22) (A.25) (A.26) directly establish the proof obligations (5.102) (5.105) (5.106) respectively. Conclusion (5.104) follows by (A.24) and the transitivity of subtyping. By applying rule EAGERLET⇓Cwith premises (A.21), (A.23) and lbeing fresh, we establish proof obligation (5.103), yielding H,S,L1 + m′′ 2let x=bein e⇓w, H′′ If we choose m′=t+φH′′ (w:C) + φH′′ (Θ) all we need to complete the proof of case EAGERLET is to show that m−m′≥1 + (m2−m′ 2)(≥1 + m′′ 2=m′′). m−m′≥1 + (m2−m′ 2) ⇐⇒ m−t−φH′′ (w:C)−φH′′ (Θ) ≥1 + m2−t−1−q′−φH′′ (w:C)−φH′′ (Θ) ⇐⇒ { q′= 0 by premise of EAGERLET (5.97), since be[ℓ/x]is in whnf } m≥m2 ⇐⇒ t+ 1 + q′+q+p+φH(Γ,∆) + φH(Θ) ≥t+ 1 + q′+q+φH2(∆, ℓ:A) + φH2(Θ) Note though that we already showed this last inequality is true, when we established the induction premise (5.101). This concludes the proof of case EAGERLET when be[ℓ/x]is in whnf and be[ℓ/x]≡c ~y. If be[ℓ/x]is in whnf and be[ℓ/x]≡λy.e′:From premise m≥t+ 1 + q′+q+p+φH(Γ,∆) + φH(Θ) (5.101) we want to derive m2≥(t+ 1 + q′+p) + q+φH2(∆, ℓ:A) + φH2(Θ) and for that purpose we have to show t+ 1 + q′+q+p+φH(Γ,∆) + φH(Θ) ≥(t+ 1 + q′+p) + q+φH2(∆, ℓ:A) + φH2(Θ), or equivalently φH(Γ,∆) + φH(Θ) ≥φH2(∆, ℓ:A) + φH2(Θ). Note
112 FCUP 999. A. A System for Eager Evaluation that φH(Γ,∆,Θ) = φH2(Γ,∆,Θ) since ℓis suitably fresh, and thus we just have to show φH2(Γ) ≥φH2(ℓ:A). This inequality holds, since by the definition of potential (Figure A.7) we have φH2(ℓ:A) = 0, given that H2(ℓ)is a λ-abstraction. We have all the premises required to apply the induction hypothesis over e[ℓ/x], obtaining m′ 2,Γ′ 2,C′ 2,M′ 2and m′′ 2such that: Γ′ 20w:C(A.29) H2,S,Lm′′ 2e[ℓ/x]⇓w, H′′ (A.30) M2<:M′ 2(A.31) C′ 2⊢MEM (H′′,L) : M′ 2(A.32) .(M′ 2|(Γ′ 2,Θ),C′ 2)(A.33) m′ 2≥(t+ 1 + q′+p) + φH′′ (w:C) + φH′′ (Θ) (A.34) m2−m′ 2≥m′′ 2(A.35) Let Γ′= Γ′ 2,M′=M′ 2and C′=C′ 2. Equations (A.29) (A.32) (A.33) directly establish the proof obligations (5.102) (5.105) (5.106) respectively. Conclusion (5.104) follows by (A.31) and the transitivity of subtyping. By applying rule EAGERLET⇓Cwith premises (A.21), (A.30) and lbeing fresh, we establish proof obligation (5.103), yielding H,S,L1 + m′′ 2let x=bein e⇓w, H′′ If we choose m′=t+φH′′ (w:C) + φH′′ (Θ) all we need to complete the proof of case EAGERLET is to show that m−m′≥1 + (m2−m′ 2)(≥1 + m′′ 2=m′′). m−m′≥1 + (m2−m′ 2) ⇐⇒ m−t−φH′′ (w:C)−φH′′ (Θ) ≥1 + m2−t−1−q′−φH′′ (w:C)−φH′′ (Θ) ⇐⇒ { q′= 0 by premise of EAGERLET (5.97), since be[ℓ/x]is in whnf } m≥m2 ⇐⇒ t+ 1 + q′+q+p+φH(Γ,∆) + φH(Θ) ≥t+ 1 + q′+p+q+φH2(∆, ℓ:A) + φH2(Θ)
FCUP 113 A.2. Proof of the Soundness Theorem for the Eager System 999. Note though that we already showed this last inequality is true, when we established the induction premise (5.101). This last sub-case concludes the proof of case EAGERLET and since the remaining cases are similar to (or simpler than) the ones presented in the soundness proof of the lazy system (in Section 5.5.6.7) this also concludes the proof of the soundness theorem for the eager system.
114 FCUP 999. A. A System for Eager Evaluation
B. Complete Derivations B.1 Simple Example: Analysing Call-By-Need VAR z:Tq′′A′q′′ z:A′ VAR y:Tq(B)qy:BABS ∅0λy.y:Tq(B)−→ qBWEAK x:Tq′′A′0λy.y:Tq(B)−→ qBABS ∅0λx.λy.y:Tq′′A′−→ 0Tq(B)−→ qBAPP z:Tq′′A′0(λx.λy.y)z:Tq(B)−→ qBLET ∅1let z=zin (λx.λy.y)z:Tq(B)−→ qB where .(A′|A′, A′) Figure B.1: Type derivation for a non-strict evaluation example 115
116 FCUP 999. B. Complete Derivations (Figure B.1,where q=0)WEAK f:T1(T0 (B)−→ 0B)1let z=zin (λx.λy.y)z:T0 (B)−→ 0B VAR x:Tq′(C)q′ x:CABS ∅0λx.x:BWEAK i:T0(B)0λx.x:B VAR f:T0(T0 (B)−→ 0B)0f:T0 (B)−→ 0BAPP f:T0(T0 (B)−→ 0B),i:T0(B)0f i :BWEAK f:T0(T0 (B)−→ 0B),i:T0(B),v:T0(B)0f i :B VAR f:T0(T0 (B)−→ 0B)0f:T0 (B)−→ 0BAPP f:T0(T0 (B)−→ 0B),v:T0(B)0f v :BLET f:T0(T0 (B)−→ 0B), f:T0(T0 (B)−→ 0B),i:T0(B)1let v=f i in f v :BSHARE f:T0(T0 (B)−→ 0B),i:T0(B)1let v=f i in f v :BPREPAY f:T1(T0 (B)−→ 0B),i:T0(B)2let v=f i in f v :BLET f:T1(T0 (B)−→ 0B)3let i=λx.xin ...:BLET ∅4let f= (let z=zin (λx.λy.y)z)in let i=λx.xin let v=f i in f v :B where B = Tq′(C)−→ q′ C Figure B.2: Type derivation for a lazy-evaluation example
FCUP 117 B.2. Higher-Order Functions: map 999. B.2 Higher-Order Functions: map (Figure B.4) ABS map:T0 T0(A−→ qfB)−→ 0Tq0(Lin)−→ q0Lout,f:T0(A−→ qfB) 0λxs.case xs of Nil -> let nil =Nil in nil, Cons x xs′-> let y=f x in let ys′=map f xs′in let ys =Cons y ys′in ys :Tq0(Lin)−→ q0Lout ABS map:T0 T0(A−→ qfB)−→ 0Tq0(Lin)−→ q0Lout 0λf.λxs.case xs of Nil -> let nil =Nil in nil, Cons x xs′-> let y=f x in let ys′=map f xs′in let ys =Cons y ys′in ys :T0(A−→ qfB)−→ 0Tq0(Lin)−→ q0Lout map:T0 T0(A−→ qfB)−→ 0Tq0(Lin)−→ q0Lout 0map :T0(A−→ qfB)−→ 0Tq0(Lin)−→ q0Lout LET ∅1let map =λf.λxs.case xs of Nil -> let nil =Nil in nil, Cons x xs′-> let y=f x in let ys′=map f xs′in let ys =Cons y ys′in ys in map :T0(A−→ qfB)−→ 0Tq0(Lin)−→ q0Lout where Lin =Lqt(3+qf+ql+p′ c,1+p′ n, A) Lout =L0(p′ c, p′ n,T0(B)) L′ in =Lqt(0,0, A′),with .(A|A, A′) L′ out =L0(0,0,T0(B′)),with .(B|B, B′) ql=max(q0, qt) Figure B.3: Type derivation for map applied to a list with potential
118 FCUP 999. B. Complete Derivations VAR xs:Tq0(Lin)q0xs :Lin CONS ∅0Nil :Lout WEAK nil:T0(L′ out)0Nil :Lout VAR nil:T0(Lout)0nil :Lout LET ∅1+p′ nlet nil =Nil in nil :Lout WEAK map:T0 T0(A−→ qfB)−→ 0Tq0(Lin)−→ q0Lout 1+p′ nlet nil =Nil in nil :Lout WEAK map:T0 T0(A−→ qfB)−→ 0Tq0(Lin)−→ q0Lout,f:T0(A−→ qfB) 1+p′ nlet nil =Nil in nil :Lout VAR f:T0(A−→ qfB)0f:A−→ qfBAPP f:T0(A−→ qfB),x:Aqff x :BWEAK f:T0(A−→ qfB),x:A, y:Tqf(B′)qff x :B (Figure B.5) LET map:T0 T0(A−→ qfB)−→ 0Tq0(Lin)−→ q0Lout, f:T0(A−→ qfB),f:T0(A−→ qfB),x:A, xs′:Tqt(Lin) 3+qf+ql+p′ clet y=f x in let ys′=map f xs′in let ys =Cons y ys′in ys :Lout SHARE map:T0 T0(A−→ qfB)−→ 0Tq0(Lin)−→ q0Lout, f:T0(A−→ qfB),x:A, xs′:Tqt(Lin) 3+qf+ql+p′ clet y=f x in let ys′=map f xs′in let ys =Cons y ys′in ys :Lout CASE map:T0 T0(A−→ qfB)−→ 0Tq0(Lin)−→ q0Lout,f:T0(A−→ qfB),xs:Tq0(Lin) q0case xs of Nil -> let nil =Nil in nil, Cons x xs′-> let y=f x in let ys′=map f xs′in let ys =Cons y ys′in ys :Lout Figure B.4: Auxiliary type derivation for map applied to a list with potential
FCUP 119 B.2. Higher-Order Functions: map 999. VAR map:T0 T0(A−→ qfB)−→ 0Tq0(Lin)−→ q0Lout 0map :T0(A−→ qfB)−→ 0Tq0(Lin)−→ q0Lout APP map:T0 T0(A−→ qfB)−→ 0Tq0(Lin)−→ q0Lout,f:T0(A−→ qfB) 0map f :Tq0(Lin)−→ q0Lout SUBTYPE map:T0 T0(A−→ qfB)−→ 0Tq0(Lin)−→ q0Lout,f:T0(A−→ qfB) 0map f :Tmin(q0,qt)(Lin)−→ q0Lout APP map:T0 T0(A−→ qfB)−→ 0Tq0(Lin)−→ q0Lout,f:T0(A−→ qfB), xs′:Tmin(q0,qt)(Lin)q0map f xs′:Lout WEAK map:T0 T0(A−→ qfB)−→ 0Tq0(Lin)−→ q0Lout,f:T0(A−→ qfB), xs′:Tmin(q0,qt)(Lin),ys′:Tq0(L′ out)q0map f xs′:Lout CONS y:T0(B),ys′:T0(Lout)0Cons y ys′:Lout WEAK y:T0(B),ys′:T0(Lout),ys:T0(L′ out)0Cons y ys′:Lout VAR ys:T0(Lout)0ys :Lout LET y:T0(B),ys′:T0(Lout)1+p′ clet ys =Cons y ys′in ys :Lout PREPAY y:T0(B),ys′:Tq0(Lout)1+q0+p′ clet ys =Cons y ys′in ys :Lout LET map:T0 T0(A−→ qfB)−→ 0Tq0(Lin)−→ q0Lout,f:T0(A−→ qfB), xs′:Tmin(q0,qt)(Lin),y:T0(B) 2+q0+p′ clet ys′=map f xs′in let ys =Cons y ys′in ys :Lout PREPAY* map:T0 T0(A−→ qfB)−→ 0Tq0(Lin)−→ q0Lout,f:T0(A−→ qfB), xs′:Tqt(Lin),y:T0(B) 2+ql+p′ clet ys′=map f xs′in let ys =Cons y ys′in ys :Lout PREPAY map:T0 T0(A−→ qfB)−→ 0Tq0(Lin)−→ q0Lout,f:T0(A−→ qfB), xs′:Tqt(Lin),y:Tqf(B) 2+qf+ql+p′ clet ys′=map f xs′in let ys =Cons y ys′in ys :Lout ∗Note that rule PREPAY justifies the typing xs′:Tqt(Lin)from xs′:Tmin(q0,qt)(Lin) by prepaying the amount max(qt−q0,0). Figure B.5: Auxiliary type derivation for map applied to a list with potential (cont.)