On Dec 30, 2011, at 11:43 AM, Conal Elliott wrote:
>> roof: f is a function, and it is taking the same argument each time.
>> Therefore the result is the same each time.
>
> That's called begging the question. f is not a function, so I guess your
> proof is flawed.
>
> It seems pretty clear that we're working with different ideas of what
> constitutes a function. When I use the term, I intend what I take to be the
> standard notion of a function in computation: not just a unique mapping from
> one input to one output, but one where the output is computable from the
> input. Any "function" that depends on a non-computable component is by that
> definition not a true function. For clarity let's call such critters
> quasi-functions, so we can retain the notion of application. Equality cannot
> be defined for quasi-functions, for obvious reasons.
>
> f is a quasi-function because it depends on getAnIntFromUser, which is not
> definable and is obviously not a function. When applied to an argument like
> 42, it yields another quasi-function, and therefore "f 42 = f 42" is false,
> or at least unknown, and the same goes for f 42 != f 42 I suppose.
>
> -Gregg
>
> Please don't redefine "function" to mean "computable function". Besides
> distancing yourself from math, I don't think doing so really helps your case.
No redefinition involved, just a narrowing of scope. I assume that, since we
are talking about computation, it is reasonable to limit the discussion to the
class of computable functions - which, by the way, are about as deeply embedded
in orthodox mathematics as you can get, by way of recursion theory. What would
be the point of talking about non-computable functions for the semantics of a
programming language?
> And on what do you base your claim that getAnIntFromUser is not definable?
Sorry, not definable might a little strong. "Not definable in the way we can
define computable functions" work better? In any case I think you probably see
what I'm getting at.
> Or that applying it (what?) to 42 gives a quasi-function?
I can't think of a way to improve on what I've already written at the moment -
it too would depend on IO - so if my meaning is not clear, so be it.
Wait, here's another way of looking at it. Think of IO actions as random
variables. So instead of getAnIntFromUser, use X as an integer random variable
yielding something like:
f :: Int -> IO Int
f x = X >>= \i -> return (i+x)
I would not call this f a function because I don't think it answers to the
commonly accepted definition of a function. Ditto for the result of applying
it to 42. Others obviously might consider it a function. De gustibus non set
disputandem.
-Gregg
-Gregg
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
