[Haskell-cafe] Signature for non-empty filter

[Neil Mitchell]

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.

Thanks

Neil