Strictness Properties of Lazy Algebraic Datatypes - Benton, Nick (Proceedings of the 3rd International Workshop on Static Analysis (SAS '93), 1993)
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 Benton92 to a language including the type nlist.