On 7 Feb 2008, at 12:07 AM, Henning Thielemann wrote:
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.
Tell that to my co-workers...
Same here: If the automatic proof takes too long -
choose a simpler example input (if possible).
3 hours wasn't chosen arbitrarily --- I've had suites of unit tests
take that long, and that's realistically about when I'd check for
divergence. And in a large program I'd hate to recompile only to
discover that it's taking so long because *I* introduced an infinite
loop into the compiler.
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.
jcc
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
