Finding the spirit of L-World
brian.goetz at oracle.com
Thu Feb 21 17:59:02 UTC 2019
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
> - 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
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.)
More information about the valhalla-spec-observers