[Haskell-cafe] Signature for non-empty filter
jonathanccast at fastmail.fm
Thu Feb 7 10:30:29 EST 2008
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.
More information about the Haskell-Cafe