How do we formally say that a function is non-strict in an argument?

Question

We say that a function is strict in its argument if

f ⊥ = ⊥

but how do we say that a function is non-strict in its argument? Can we say that a function is non-strict if

f ⊥ ≠ ⊥

?

How does that extend to functions of many arguments, where we might or might not evaluate an argument depending on the value of some other argument?

I'm asking this in the context of better documenting the strictness properties of Haskell functions using Haddock documentation.

Answer 1

There's no standard notation for expressing complex strictness properties. It's also no not as simple as just being strict, since for data structures you may need to say exactly how much gets evaluated.

That said, for a simple function like

cond c t e = if c then t else e

you can imagine saying that the strictness is 1 & (2 | 3), meaning that it will evaluate the first argument, and either the second or the third. These are the kind of strictness properties that a simple strictness analyzer will come up with. (And simple ones seem to be the only ones that are worth while.)