On Fri, Dec 30, 2011 at 10:24 AM, Gregg Reynolds <d...@mobileink.com> wrote:
> > 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 > I'm recommending a shift to more well-defined terms in hopes to move this discussion away from tastes & opinions and from what's obvious (even if untrue or ill-defined). If you look at the signature of 'f', you can see that it's declared to be a function (and a computable one at that). To demonstrate that it's not actually a function, I'd expect you to show that it's one-to-many, which then raises the question of equality, as needed to distinguish one from many. - Conal
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
