On Wed, 6 Feb 2008, Bulat Ziganshin wrote:
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
If the type checker does not terminate because the checked function does not terminate on the example input, then the function does not pass the type check and as a compromise this would be ok.