[Haskell-cafe] Signature for non-empty filter

[Henning Thielemann]

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.