Projections for polymorphic first-order strictness analysis
- 1 June 1992
- journal article
- research article
- Published by Cambridge University Press (CUP) in Mathematical Structures in Computer Science
- Vol. 2 (3) , 301-326
- https://doi.org/10.1017/s0960129500001493
Abstract
We apply the categorical properties of polymorphic functions to compile-time analysis, specifically projection-based strictness analysis. First we interpret parameterised types as functors in a suitable category, and show that they preserve monics and epics. Then we define “strong” and “weak” polymorphism, the latter admitting certain projections that are not polymorphic in the usual sense. We prove that, under the right conditions, a weakly polymorphic function is characterised by a single instance. It follows that the strictness analysis of one simple instance of a polymorphic function yields results that apply to all. We show how this theory may be applied. In comparison with earlier polymorphic strictness analysis methods, ours can apply polymorphic information to a particular instance very simply. The categorical approach simplifies our proofs, enabling them to be carried out at a higher level, and making them independent of the precise form of the programming language to be analysed. The major limitation of our results is that they apply only to first-order functions.Keywords
This publication has 8 references indexed in Scilit:
- Inverse image analysis generalises strictness analysisInformation and Computation, 1991
- Strictness analysis aids time analysisPublished by Association for Computing Machinery (ACM) ,1988
- Compiling strictness into streamsPublished by Association for Computing Machinery (ACM) ,1987
- Higher-order strictness analysis in untyped lambda calculusPublished by Association for Computing Machinery (ACM) ,1986
- The Category-Theoretic Solution of Recursive Domain EquationsSIAM Journal on Computing, 1982
- The theory and practice of transforming call-by-need into call-by-valuePublished by Springer Nature ,1980
- Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpointsPublished by Association for Computing Machinery (ACM) ,1977
- Towards a theory of type structureLecture Notes in Computer Science, 1974