[Haskell-cafe] Signature for non-empty filter

[Bulat Ziganshin]

Hello Henning,

Thursday, February 7, 2008, 4:27:30 PM, you wrote:

>> ok, read this as "computer can ensure...", because it was exactly the
>> original question - "can computer check that any given function in
>> turing-complete language is non-trivial?"

> My original question according to
> 
> http://www.haskell.org/pipermail/haskell-cafe/2008-February/039161.html
>   was "Is Haskell's type system including extensions strong enough for
> describing a function, that does not always return a trivial value?"

where Haskell is *turing-complete* *computer* language

this allows to answer to your question that you need to use special,
non-turing language if you want to check arbitrary functions for
non-trivialness. one example of such language:

data Func = ConstTrue | ConstFalse

and dependent-typed languages provides you (afaiu) much richer
facilities to describe functions for which you still may prove
something useful

so, if you term "function" includes the Func type, the answer is
"yes", but if you mean usual haskell functions, the answer is no


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