[Haskell-cafe] Signature for non-empty filter
lemming at henning-thielemann.de
Thu Feb 7 03:07:45 EST 2008
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.
More information about the Haskell-Cafe