Department of Computer Science and Technology

Technical reports

Strictness analysis of lazy functional programs

Peter Nicholas Benton

August 1993, 154 pages

This technical report is based on a dissertation submitted December 1992 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Pembroke College.

DOI: 10.48456/tr-309

Abstract

Strictness analysis is a compile-time analysis for lazy functional languages. The information gained by a strictness analyser can be used to improve code generation for both sequential and parallel implementations of such languages.

After reviewing the syntax and semantics of a simply typed lambda calculus with constants, we describe previous work on strictness analysis. We then give a new formulation of higher order strictness analysis, called strictness logic. This is inspired by previous work on static analysis by non-standard type inference, and by work on logic of domains. We investigate some proof theoretic and semantic properties of our logic, and relate it to the conventional approach using abstract interpretation. We also consider extending the logic with disjunction.

We then describe how to extend the simply typed lambda calculus with lazy algebraic datatyped. A new construction of lattices of strictness properties of such datatypes is described. This arises from the characterisation of the solutions to the recursive domain equations associated with these types as initial algebras.

Next we consider first order (ML-style) ploymorphism and show how Wadler’s ‘theorems for free’ parametricity results may be obtained from a simple extension of the semantics of monomorphic language. We then prove a polymorphic invariance result relating the derivable strictness properties of different substitution instances of polymorphic terms.

Full text

PDF (13.3 MB)

BibTeX record

@TechReport{UCAM-CL-TR-309,
  author =	 {Benton, Peter Nicholas},
  title = 	 {{Strictness analysis of lazy functional programs}},
  year = 	 1993,
  month = 	 aug,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-309.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-309},
  number = 	 {UCAM-CL-TR-309}
}