On Wed, Dec 7, 2011 at 12:10 PM, Giacomo Tesio <giacomo@tesio.it> wrote:

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?

But what if we embedded an undecidable problem in the function? For example, \x -> if haltingProblem then x (5*x) else x (4*x). There's no way to decide whether that function is the same or not.

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

That would be nice, but it's awkward to include functionality that relies on partial execution of code that may or may not terminate. I'm not sure how useful alpha substitution like you ask for would be; I don't think it would fix the problem you raised at first.