Finding the spirit of L-World

[Brian Goetz]

More on substitutibility and why this it is desirable...

> #### Equality
>
> Now we need to define equality.  The terminology is messy, as so many
> of the terms we might want to use (object, value, instance) already
> have associations. For now, we'll describe a _substitutability_
> predicate on two instances:
>
>    - Two refs are substitutable if they refer to the same object
>      identity.
>    - Two primitives are substitutable if they are `==` (modulo special
>      pleading for `NaN` -- see `Float::equals` and `Double::equals`).
>    - Two values `a` and `b` are substitutable if they are of the same
>      type, and for each of the fields `f` of that type, `a.f` and `b.f`
>      are substitutable.
>
> We then say that for any two objects, `a == b` iff a and b are
> substitutable.

Currently, our type system has refs and primitives, and the == predicate 
applies on all of them.  And for all the types we have today (with the 
almost-too-small-to-mention anomaly of NaN), == *already is* a 
substitutibility predicate (where substitutibility means, informally: 
"no observable difference between the two arguments."  Two refs are 
substitutible if they refer to the same object identity; two primitives 
are substitutible if they refer to the same value (modulo NaN.)

VM engineers like to refer to `==` on refs as "identity equality", but 
that's really an implementation detail.  What it really means is: are 
the two things the same.  And that's what `==` means for primitives too, 
and that's how the other 99.99% of users think of it too.

The natural interpretation of `==` in a world with values is to extend 
this "are these two things the same" to values too.  The 
substitutibility relation above applies the same "are you the same" 
logic equally to refs, values, and primitives.  No sharp edges (except 
the NaNsense that we are already stuck with.)