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 <byorgey@seas.upenn.edu> 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