On strictness and totality

In this paper we present a revised and extended version of the strictness and totality type assignment system introduced by Solberg, Nielson and Nielson in the Static Analysis Symposium '94. Our main result is that (w.r.t. the possibility of replacing safely a lazy application by a strict one) the strictness and totality information given by this system is equivalent to the information given by two separate systems: one for strictness, and one for totality. This result is interesting from both a theoretical (understanding of the relations between strictness and totality) and a practical (more efficient checking and inference algorithms) point of view. Moreover we prove that both the system for strictness and the system for totality have a sound and complete inclusion relation between types w.r.t. the semantics induced by the term model of a language including a convergence to weak head normal form test at higher types.