On Wed, 6 Feb 2008, Jonathan Cast wrote:
On 6 Feb 2008, at 1:54 PM, Matthew Pocock wrote:
On Wednesday 06 February 2008, Henning Thielemann wrote:
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.
Can't fault this logic. The problem is that you may have to wait quite a long time to discover this non-termination.
I would second this --- letting the compiler go only to discover that it's been running for the last 3 hours because it's diverging seems like a wasted 3 hours.
There is the same problem with unit testing: Tests that eat too much time have to be rewritten. Same here: If the automatic proof takes too long - choose a simpler example input (if possible). But Dan's point definitely applies here - there is no need to automatically prove every instance, if there is a possibility to do a proof manually.