Neil Brown wrote: > Dan Piponi wrote: >> On Mon, Oct 12, 2009 at 10:42 AM, muad <[email protected]> wrote: >> >>> Is it possible to prove correctness of a functions by testing it? >> consider a function of signature >> >> swap :: (a,b) -> (b,a) >> >> We don't need to test it at all, it can only do one thing, swap its >> arguments. (Assuming it terminates.) >> > swap = undefined > > Terminates and does not swap its arguments :-) What do free theorems > say about this, exactly -- do they just implicitly exclude this > possibility?
Normally, one presumes that "undefined" (id est, calling "error") is equivalent to looping, except that calling "error" is pragmatically speaking better: it is nicer to the caller of your function (they/you get to see a somewhat more descriptive error message instead of 100% CPU without any results). Regards, Jochem -- Jochem Berndsen | [email protected] | joc...@牛在田里.com _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
