On Fri, Dec 30, 2011 at 9:43 AM, Conal Elliott <co...@conal.net> wrote:
> On Fri, Dec 30, 2011 at 9:43 AM, Gregg Reynolds <d...@mobileink.com> wrote: > >> On Dec 30, 2011, at 11:20 AM, Colin Adams wrote: >> On 30 December 2011 17:17, Gregg Reynolds <d...@mobileink.com> wrote: >> >> On Dec 30, 2011, at 11:04 AM, Colin Adams wrote: >>> On 30 December 2011 16:59, Gregg Reynolds <d...@mobileink.com> wrote: >>> >>> On Fri, Dec 30, 2011 at 12:49 AM, Heinrich Apfelmus < >>>> apfel...@quantentunnel.de> wrote: >>>> >>>> The function >>>>> >>>>> f :: Int -> IO Int >>>>> f x = getAnIntFromTheUser >>= \i -> return (i+x) >>>>> >>>>> is pure according to the common definition of "pure" in the context of >>>>> purely functional programming. That's because >>>>> >>>>> f 42 = f (43-1) = etc. >>>>> >>>>> Conclusion: f 42 != f 42 >>>> >>>> (This seems so extraordinarily obvious that maybe Heinrich has >>>> something else in mind.) >>>> >>>> This seems such an obviously incorrect conclusion. >>> >>> f42 is a funtion for returning a program for returning an int, not a >>> function for returning an int. >>> >>> >>> My conclusion holds: f 42 != f 42. Obviously, so I won't burden you >>> with an explanation. ;) >>> >>> -Gregg >>> >> Your conclusion is clearly erroneous. >> >> proof: 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. > > And on what do you base your claim that getAnIntFromUser is not definable? > Or that applying it (what?) to 42 gives a quasi-function? > > Also: f is not a function, so I guess your proof is flawed. > Can you support the claim that f is not a function?
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe