[Haskell-cafe] Signature for non-empty filter

Jonathan Cast 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 mailing list