Hi Brent, thanks for your answer. I don't get it, though... Looks like

id (\z -> bar z (2*x + 3*x))

is actually different from

f1 -> \x -> bar x (5*x)

as in the first x can only be a closure, while in the second is an argument. Supposing that it's just a typo and you did mean id (\z -> bar z (2*z + 3*z)) I see how it could be very complex, but still seem to me (theoretically?) decidable. What I'm missing? Nevertheless, while I would see an extreme value in a compiler that is able to understand that "id (\z -> bar z (2*z + 3*z)) == f1" is True, it's not my target. I would find already very useful a compiler that is able to understand id f = f, that (\x -> 3 + x) == (\y = 3 + y) == (+3) even if it isn't able to see that (+3) == (\x -> 2 + 1 + x). This would improve greatly the power of Functors (at least as I understood them :-D) Don't you think? Giacomo On Wed, Dec 7, 2011 at 3:42 PM, Brent Yorgey wrote:

On Wed, Dec 07, 2011 at 11:34:28AM +0100, Giacomo Tesio wrote:

...

Hi Haskellers,

I'm wondering why, given that functions and referential transparency are first class citizens in haskell, it isn't possible to write a mapping function this way:

f1 :: a -> b

f2 :: a -> b

f3 :: c -> a -> b

map :: (a -> b) -> T a -> T b map f1 = anEquivalentOfF1InTCategory map f2 = anEquivalentOfF2InTCategory map f3 $ c = anEquivalentOfF3withCInTCategory map unknown = aGenericMapInTCategory

Is it "just" the implementation complexity of the feature in ghc that prevents this? Or is it "conceptually" wrong?

At a first look, I thought that most of complexity here should be related to function's equality, but than I thought that the function full name should uniquely map from the category of meanings in the programmer mind to the category of implementations available to the compiler's.

It is preciesly *because* of referential transparency that you cannot do this. Suppose that

f1 = \x -> bar x (5*x)

then

map (\x -> bar x (5*x))

is supposed to be equivalent to 'map f1'. You might not think that is too bad -- it is obvious that is the same as f1's definition. But what about

map (id (\z -> bar z (2*x + 3*x)))

? This is also required to be the same as 'map f1'. But now you have to know about distributivity of multiplication over addition in order to tell. This gets arbitrarily complicated (and, in fact, undecidable) very quickly.

-Brent

_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

On Wed, Dec 07, 2011 at 06:10:01PM +0100, Giacomo Tesio wrote:

Hi Brent, thanks for your answer.

I would find already very useful a compiler that is able to understand id f = f, that (\x -> 3 + x) == (\y = 3 + y) == (+3) even if it isn't able to see that (+3) == (\x -> 2 + 1 + x).

But then we would lose referential transparency.

This would improve greatly the power of Functors (at least as I understood them :-D) Don't you think?

Well... I suppose it would make things more expressive (although I think "greatly" is overstating things), but at the terrible cost of losing referential transparency, and probably also parametricity (although I have not thought about it carefully). I, for one, am not willing to give up these beautiful and powerful reasoning tools just for a little gain in expressivity. -Brent

Giacomo

On Wed, Dec 7, 2011 at 3:42 PM, Brent Yorgey wrote:

...

On Wed, Dec 07, 2011 at 11:34:28AM +0100, Giacomo Tesio wrote:

...

Hi Haskellers,

I'm wondering why, given that functions and referential transparency are first class citizens in haskell, it isn't possible to write a mapping function this way:

f1 :: a -> b

f2 :: a -> b

f3 :: c -> a -> b

map :: (a -> b) -> T a -> T b map f1 = anEquivalentOfF1InTCategory map f2 = anEquivalentOfF2InTCategory map f3 $ c = anEquivalentOfF3withCInTCategory map unknown = aGenericMapInTCategory

Is it "just" the implementation complexity of the feature in ghc that prevents this? Or is it "conceptually" wrong?

At a first look, I thought that most of complexity here should be related to function's equality, but than I thought that the function full name should uniquely map from the category of meanings in the programmer mind to the category of implementations available to the compiler's.

It is preciesly *because* of referential transparency that you cannot do this. Suppose that

f1 = \x -> bar x (5*x)

then

map (\x -> bar x (5*x))

is supposed to be equivalent to 'map f1'. You might not think that is too bad -- it is obvious that is the same as f1's definition. But what about

map (id (\z -> bar z (2*x + 3*x)))

? This is also required to be the same as 'map f1'. But now you have to know about distributivity of multiplication over addition in order to tell. This gets arbitrarily complicated (and, in fact, undecidable) very quickly.

-Brent

_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

I agree. I think I got it, without the ability to correctly match equivalent morphisms, morphisms can't be treated as objects. Probably such ability would require a very powerful runtime, but I don't think that it would be just matter of expressivity (and you would not loose referential transparency as (+3) would be matched with (\x -> 5 + x - 2). Giacomo On Thu, Dec 8, 2011 at 1:53 PM, Daniel Fischer < daniel.is.fischer@googlemail.com> wrote:

On Thursday 08 December 2011, 07:14:39, Brent Yorgey wrote:

...

I, for one, am not willing to give up these beautiful and powerful reasoning tools just for a little gain in expressivity.

-Brent

Seconded,

Daniel

_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

On 10-Dec-2011 11:17 AM, Ken KAWAMOTO wrote:

On Thu, Dec 8, 2011 at 3:14 PM, Brent Yorgey wrote:

...

On Wed, Dec 07, 2011 at 06:10:01PM +0100, Giacomo Tesio wrote:

...

I would find already very useful a compiler that is able to understand id f = f, that (\x -> 3 + x) == (\y = 3 + y) == (+3) even if it isn't able to see that (+3) == (\x -> 2 + 1 + x). But then we would lose referential transparency. As I understand, this would be against lazy evaluation since it would request to evaluate expressions in lambda, but I don't see how this relates to referential transparency. Can you elaborate this a little bit?

I second the question. From what I understand referential transparency means that an expression can be replaced by its value with no change to program semantics, or equivalently that a function always produces the same result/behaviour given the same input. How does determining whether two (pure) functions are equivalent break referential transparency? cheers! Graham

Thanks, Ken

_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

Excellent, thanks Daniel and Felipe. We don't even need to invoke infinite or undecidable problems, since it's easy to construct equal functions for which determining equality would be prohibitively expensive. If then you can only check equality for some functions, because you want compilation to finish, say, within the programmer's lifetime, you lose referential transparency. Graham On 11-Dec-2011 1:24 PM, Daniel Fischer wrote:

...

...

On Thu, Dec 8, 2011 at 3:14 PM, Brent Yorgey wrote:

...

On Wed, Dec 07, 2011 at 06:10:01PM +0100, Giacomo Tesio wrote:

...

I would find already very useful a compiler that is able to understand id f = f, that (\x -> 3 + x) == (\y = 3 + y) == (+3) even if it isn't able to see that (+3) == (\x -> 2 + 1 + x). But then we would lose referential transparency. As I understand, this would be against lazy evaluation since it would request to evaluate expressions in lambda, but I don't see how this relates to referential transparency. Can you elaborate this a little bit? I second the question. From what I understand referential transparency means that an expression can be replaced by its value with no change to

On 10-Dec-2011 11:17 AM, Ken KAWAMOTO wrote: program semantics, or equivalently that a function always produces the same result/behaviour given the same input. How does determining whether two (pure) functions are equivalent break referential transparency? I think if it were possible to find out whether two functions are the same for *every* pair of two functions, it wouldn't violate referential

On Sunday 11 December 2011, 19:07:06, Graham Gill wrote: transparency.

But it's not possible, so all you have is that for some pairs of functions equality can be proved, for some pairs it can be disproved and for some pairs, it cannot be decided.

So

foo f g = if canProveEqual f g then "Yay :)" else "Nay :("

wouldn't be referentially transparent,

foo (+3) (\x -> x+3) = "Yay :)" foo (+3) somethingWhichIsTheSameButCan'tBeProvedToBe = "Nay :("

Thanks Daniel and Felipe. To me it seems Daniel's foo doesn't break referential transparency because we can always replace "foo (+3) (\x -> x+3)" with "Yay :)", and "foo (+3) somethingWhichIsTheSameButCan'tBeProvedToBe" with "Nay :(". It just contradicts our expectation that "foo (+3) something....ToBe" should return "Yay :)", which is another story. On Mon, Dec 12, 2011 at 3:24 AM, Daniel Fischer wrote:

But it's not possible, so all you have is that for some pairs of functions equality can be proved, for some pairs it can be disproved and for some pairs, it cannot be decided.

This sounds like quite common function behavior as we can see in f n = if n > 0 then True else if n == 0 then f 0 else False Here, f 1 returns True, f (-1) returns False, and f 0 doesn't terminate. Still f is referentially transparent, isn't it? If so, why can we not say foo is referentially transparent? On the other hand, I agree that Felipe's obviouslyEqual is not referentially transparent as its behavior really depends on how Haskell runtime allocates functions (thunks) in memory. I understand that we cannot construct such a function that always terminates and decides functions' equality (equality defined as, say, "f1 equals f2 iff f1 x == f2 x for any argument x"). But again, does this have something to do with referential transparency? Isn't this just because it's undecidable problem?

On Mon, Dec 12, 2011 at 10:47, Giacomo Tesio wrote:

While I got your point, I'm still wondering about functions as constructor of other functions thus it would be possible to match to the function name like we do for type constructors. I can't have an insight about why this is wrong. Why can't we treat functions as constructors?

This makes (f) and (id f) different, when referential transparency requires that they be the same. Anything capable of spotting that difference *must* be in IO. A concrete reason for this is laziness: *everything* is a function, including literals — and I do not mean by this things like the implicit fromIntegral/fromRational on numeric literals. Everything is a function which is evaluated to WHNF when needed. So now you have an additional issue: if you're pattern-matching something — which is the normal way to force evaluation — you have to know whether we're expecting normal pattern matching, which does evaluation to a data constructor, or your function-pattern matching, which evaluates to some kind of distinguished "function constructor". Additionally, there is the question of where you draw the line. Do you consider a binding to be a "function constructor"? Only a top level binding? Only an imported binding? Only an import from a "system" module? Only a primop? I can see arguments for all of them, and no obvious argument for why one of them is better than the others. Moreover, the deeper you go in this stack, the greater the chance that different compilers, or different versions of the same compiler, produce different results; this is again a violation of referential transparency. -- brandon s allbery allbery.b@gmail.com wandering unix systems administrator (available) (412) 475-9364 vm/sms

On Sun, Dec 11, 2011 at 4:07 PM, Graham Gill wrote:

I second the question. From what I understand referential transparency means that an expression can be replaced by its value with no change to program semantics, or equivalently that a function always produces the same result/behaviour given the same input. How does determining whether two (pure) functions are equivalent break referential transparency?

It doesn't. Whoever it also isn't guaranteed to terminate. What *does* break referential transparency is a function equality that works sometimes, but not other. Cheers, -- Felipe.