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