A new construction of a finite set of strictness properties for any lazy algebraic datatype is presented. The construction is based on the categorical view of the solutions to the recursive domain equations associated with such types as initial algebras. We then show how the initial algebra induction principle can be used to reason about the entailment relation on the chosen collection of properties. We examine the lattice of properties given by our construction for the type nlist of lazy lists of natural numbers and give proof rules which extend the conjunctive strictness logic of [2] to a language including the type nlist.
CITATION STYLE
Benton, P. N. (1993). Strictness properties of lazy algebraic datatypes. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 724 LNCS, pp. 206–217). Springer Verlag. https://doi.org/10.1007/3-540-57264-3_42
Mendeley helps you to discover research relevant for your work.