[Haskell-cafe] On the purity of Haskell

[Gregg Reynolds]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20111230/b600ddfa/attachment.htm>