ndmitchell:
Hi
Actually, you can go slightly better:
words s = case dropWhile isSpace s of [] -> [] (s:ss) -> (s:w) : drop1 sss where (w, sss) = break isSpace ss
drop1 [] = [] drop1 (x:xs) = words xs
Although a good optimising compiler may make this last leap all on its own.
To really convince yourself and everyone else you could compare it against the spec, for both total and partial values.
I'm pretty convinced that I applied reasoning rules at each stage. If you have a proof, testing is irrelevant :-)
I've already modified the Yhc base library with this optimisation, and done some basic testing, and nothing broke.
I'd second Duncan here -- strictness properties are *really* hard, so changes to existing (H98) functions must come with both QuickCheck and strictness checking properties, before I'd be comfortable accepting them. The missing support for partial values in QuickCheck is quite a hole that needs fixing. -- Don