Re: [Haskell-cafe] Signature for non-empty filter

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