[Haskell-cafe] On the purity of Haskell

[Conal Elliott]

On Fri, Dec 30, 2011 at 9:43 AM, Conal Elliott <conal at conal.net> wrote:

> On Fri, Dec 30, 2011 at 9:43 AM, Gregg Reynolds <dev at mobileink.com> wrote:
>
>> On Dec 30, 2011, at 11:20 AM, Colin Adams wrote:
>> On 30 December 2011 17:17, Gregg Reynolds <dev at mobileink.com> wrote:
>>
>> On Dec 30, 2011, at 11:04 AM, Colin Adams wrote:
>>> On 30 December 2011 16:59, Gregg Reynolds <dev at mobileink.com> wrote:
>>>
>>> On Fri, Dec 30, 2011 at 12:49 AM, Heinrich Apfelmus <
>>>> apfelmus at 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?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20111230/571f1128/attachment.htm>