This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

Equality of functional values
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: -- (:) From: Jacques Carette Subject: Re: [Caml-list] Re: Equality of functional values
```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

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
>
>

```