[Haskell-cafe] Signature for non-empty filter

[Bulat Ziganshin]

Hello Henning,

Wednesday, February 6, 2008, 6:09:28 PM, you wrote:

>> it's another question: you can describe trivial values using type
>> system, but can't prohibit them using it - it's impossible because you
>> can't check for arbitrary algorithm whether it will be finally stopped

> I could consider the function buggy, if it does not terminate on the given
> example.

it's impossible to check for *arbitrary* function call whether it will be
terminated. seems that you don't have formal CS education? :)

so one can develop set of functions that are guaranteed to be
terminated or guaranteed to be non-trivial. but it's impossible to
check for arbitrary function whether it's trivial and even whether it
will terminate for particular data

this means that answer to original question - one can ensure that
argument for filter is non-terminating function only if these
functions are written using some special notation which doesn't allow
to write arbitrary turing-complete algorithms

-- 
Best regards,
 Bulat                            mailto:Bulat.Ziganshin at gmail.com