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