[Haskell-cafe] Signature for non-empty filter

[Neil Mitchell]

Hi

> 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.

Yes, but someone redefined your problem as the above one, which I can
solve :-) For your original problem, Catch is entirely unsuitable.
ESC/Haskell would be my preferred method of solving this within
Haskell, but I'm not sure if it has existentials or not. I could
imagine writing something like:

filter :: {f: exists x. f x == True} -> {True} -> {True}
filter :: (a -> Bool) -> [a] -> [a]

Thanks

Neil