[Haskell-cafe] Signature for non-empty filter

[Henning Thielemann]

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.