Re: [Haskell-cafe] is proof by testing possible?

Could that nice precise formulation simply be Scott continuity, which in turn preserves compactness through composition and under application? Dan Piponi wrote:

On Mon, Oct 12, 2009 at 11:31 AM, Neil Brown 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe