|
Abstract : |
We propose a notion of uniform ideal (certain Scott-closed sets) to characterise strictness properties. This enables us to explain why Hughes ' and Wadler's H projection for lazy list strictness analysis is not in general expressible as an abstract interpretation property of the standard semantics. We give circumstances when it is so expressible. Doing so casts light on Burn's HB projection and his question of its relationship to H. Uniform ideals are a generalisation of the sets of values corresponding to types in (simple) polymorphic type systems. Wadler's doubly-lifted abstract domain constructor for lazy lists can be seen as a special case which only uses certain uniform ideals. The con uence of strictness and type theory furthers Kuo and Mishra's notion of \strictness types". Summary of results We characterise strictness properties as uniform ideals. This enables us to give abstract interpretation properties to show that a function on list(t 1 +t 2) is H-strict (Wadler and Hughes). We show that the property of a function on list(int) of being H-strict cannot be expressed as an abstract interpretation of the standard interpretation under weak conditions including uniform treatment of integer constants and compositionality. 2 Burn's HB-strictness is seen as the best possible analogue to H-strictness subject to these, |
