The only times where I have used intensional equality (which was in a 
dynamically typed system for doing mathematics), it would have 
considered the bottom two lambda-expressions to be _different_, as in 
SML/NJ.

This intensional equality is only used for optimizations.  A function 
can optimize some cases based on intensional equality with some known 
cases, and fall-through to a slower general case otherwise.  Not 
recognizing two terms as equivalent only results in slower computation 
time, not an incorrect result.  You might see it as a sort of 
overloading based on function-level matching.

Maple, Mathematica and MuPAD (internally) use this kind of 
dispatch-on-function feature a lot.  This is related to the issue that 
in all these languages, 'constructors' and 'functions' are one and the 
same.  My experience is that in practice, this works.  Perhaps it would 
not be as useful in languages where constructors and functions are 
different.

Jacques

Stefan Monnier wrote:
> I don't know what the OCaml optimizer may do, but I do know that in SML/NJ
> such an intentional equality would often not give the expected result,
> because it's pretty common for it to use various forms of eta-like
> expansions in the hope of doing uncurrying or argument flattening, so you
> may end up with
>
>    f == f
>
> turned into
>
>    (λx1.λx2.f(x1,x2)) == (λy1.λy2.f(y1,y2))
>
> and the system may not try to recognize that the two lambda-expressions are
> identical (too costly an analysis for no performance benefit), so it will
> compile them to two different pieces of machine language.
>
>
>         Stefan
>
>