[Haskell-beginners] Pattern matching over functions

[Alec Story]

On Wed, Dec 7, 2011 at 12:10 PM, Giacomo Tesio <giacomo at 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.


-- 
Alec Story
Cornell University
Biological Sciences, Computer Science 2012
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/beginners/attachments/20111207/2b953b5e/attachment.htm>