[Haskell-cafe] is proof by testing possible?

[Dan Weston]

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 <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
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
> 
>