[Haskell-cafe] is proof by testing possible?
westondan at imageworks.com
Mon Oct 12 15:59:46 EDT 2009
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 :-)
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe