Getters vs. public final fields in records

[Andrew Cave]

Thanks for explaining; I think there are a few issues with your reasoning,
however:


As it turns out, the mathematical construct from Domain Theory known as
> "embedding-projection pairs" (which is a formalization of approximation)
> offer us a useful way to talk about the right thing.  The key invariant
> that records must adhere to (specified in the refined contract of
> `Record::equals`) is that unpacking a record components, and repacking in a
> new record, should yield an "equals" record:
>
>     r.equals(new R(r.c0(), r.c1(), ..., r.cn())
>
> (This is as close as we can say in Java to "construction and
> deconstruction form an embedding-projection pair between the space of
> records and the cartesian product space of their components.")
>

There are actually two conditions in the definition of an
embedding-projection pair (I am using “o” for function composition below);

1) p o e = id
2) e o p <= id

Where <= means, roughly speaking, “less defined than”; it is equality, but
allowing the left-hand side to be partial, i.e. non-terminating on some
inputs

Following your “translation” into Java (and ignoring several technicalities
that make it problematic…), taking the constructor to be e and the
destructors to be p,

1) means:

(new R(a1, …, an)).p1().equals(a1)
… and …
(new R(a1, …, an)).pn().equals(an)

2) means (roughly)

new R(r.p1(), …, r.pn()).equals(r) *OR* new R(r.p1(), … r.pn()) fails to
terminate

2) is close to the condition you claimed, but look at 1) — it *forces* the
accessors to return the inputs to the constructor *according to the
existing equals() defined on the inputs* — so, when equals() on the inputs
is reference equality, the accessor is forced to return the exact same
reference.

So, ok, this just means that the embedding-projection pair is not the right
tool to make your case, that’s ok. (Although I’m not sure where you got the
impression it would — it is a very specific definition, used almost
exclusively in the construction of recursive types in domain theory).

Instead, your condition is simply e o p = id — the accessors form a right
inverse of the constructor, or the constructor is a left inverse of the
accessors, fine.

Note that if your constraint is the only one applied, that permits
definitions of equality that satisfy properties like R(a,b).equals(R(b,a))
— records can be made “unordered” and the accessors can roll a die to
decide which component to return, as well as more complex quotients, like
R(a,b).equals(R(c,d)) exactly when a*d = b*c (the rational numbers). Maybe
that’s intentional? You tell me.


The reason that the situation you describe is inevitable comes from …
>

>
> If your component already chooses the answer for equals that you want --
> such as ArrayList::equals comparing lists by contents, or arrays comparing
> by identity -- then you can do nothing.  Otherwise, you have to override
> the constructor, accessor, and equals in concert to preserve the invariant
> that deconstruction and reconstruction yields something equivalent to the
> original.
>

There are already at least two ways to express this in Java, the first
being to wrap the components in a class that defines the equality you want,
and the second is to use a plain old class instead of a record. What is
missing from Java is the ability to express plain old Cartesian products
where the behaviour of the accessors and equality is *known* and
well-understood by all. So I would hardly call the current situation
“inevitable”.

Consistent with the choice we've made elsewhere (functional interfaces are
> nominal function types, not structural ones; sealed types are nominal union
> types, not structural ones), the rational choice for Java's product types
> is also nominal, not structural.
>

I think there is a confusion here between structural *types* and structural
*equality*? Nominal typing means simply that types are declared equal when
they have the same name, while structural typing means types are declared
equal if they have the same “structure” (“definition”). Records could force
structural equality but remain nominally typed.

Note also that Java has been a hybrid of structurally typed and nominally
typed ever since the introduction of generics — we no longer “name” the
type of “lists of integers” IntList — instead we compare the types
List<SomeComplexTypeExpression> and List<SomeOtherComplexTypeExpression> by
comparing the structure of the types — that SomeComplexTypeExpression is
the same as SomeOtherComplexTypeExpression, allowing type variables inside
SomeComplexTypeExpression to be instantiated along the way.

Pair<T,S> is actually a kind of structural record type!!

So structural typing and nominal typing are not in conflict, they can and
do work in harmony.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.org/pipermail/amber-dev/attachments/20220813/726688b1/attachment.htm>