[Haskell-cafe] On the purity of Haskell

[Conal Elliott]

On Fri, Dec 30, 2011 at 10:24 AM, Gregg Reynolds <dev at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20111230/2836a876/attachment.htm>