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@gmail.com