Hello Henning, Thursday, February 7, 2008, 12:29:02 AM, you wrote:
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.
how you can check that some code doesn't terminate? ;) it may be just a bit too slow. we again return to my original point - we can check for *some* representations of trivial functions values, but we can't *ensure* that some computation is non-trivial -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com