[Haskell-cafe] is proof by testing possible?

[Dan Piponi]

On Mon, Oct 12, 2009 at 11:31 AM, Neil Brown <nccb2 at kent.ac.uk> wrote:
> swap = undefined
>
> Terminates and does not swap its arguments :-)  What do free theorems say
> about this, exactly -- do they just implicitly exclude this possibility?

I'm terrible at reasoning about functions with bottoms (ie. undefined
or non-termination).

But I suspect that a property like this holds: if the type signature
of a function f is polymorphic in a, and it doesn't produce bottom for
one particular value x of type a, for some particular type a, f can
never produce bottom for any choice of x in any choice of type a.
(Which is not to say it might not fail, but that the failure will be
an issue with x, not f.)

The intuition behind this is that if a function is polymorphic in a
then it never examines the a. So even if a is bottom, the function can
never know it. But it could fail because f additionally accepts as
argument a polymorphic function that itself accepts a's, and that
fails. But then it wouldn't be f's fault, it'd be the fault of the
function you passed in.

This is very poor of me. There's probably a nice precise formulation
of what I've just said :-)
--
Dan