On Thu, 7 Feb 2008, Neil Mitchell wrote:
Hi
I think what you want to say now is not just
(filter f l) is type correct when there is some argument on which f returns true
but
(filter f l) is type correct when there is some *element of l* on which f returns true
or in Haskell:
filterNonEmpty f x = assert (not $ null res) res where res = filter f x
If you give that definition to the Catch tool (http://www-users.cs.york.ac.uk/~ndm/catch/) it will try and prove each call is safe. For certain examples, Catch will do the job very well - for example if your filter is something structural like isJust or null.
Indeed, if Catch or ESC or similar tools can handle such specifications it would be great. However I suspect that the translation you gave is different from what I wanted. I consider a function buggy, if it implements 'const' considerably more complicated than just saying 'const'. :-) That is, I only want to reject a function if it _always_ returns the empty list. Your 'filterNonEmpty' is rejected whenever _some_ arguments yield the empty list.