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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
