[Haskell-cafe] Signature for non-empty filter

[Jonathan Cast]

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