Getters vs. public final fields in records

[Brian Goetz]

> 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

A good intuition for <= here is "approximates" or "has less information 
than."  The bottom value (which is used to describe 
nonterminating/throwing operations) is a uniformly terrible (zero 
information) approximation for everything.  But e-p pairs are not just 
about partiality; they are also about information loss.  (The discrete 
partial ordering, which allows partiality but no other approximation, is 
a common but less interesting case.)  This model was chosen to also 
support _normalization_ such as defensive copies (this is a form of 
throwing away information, namely identity), rounding, truncating (e.g., 
float to int), clamping ("if (x > n) x = n"), replacing invalid 
components with valid ones (e.g., replacing (_, 0) with (0, 1) in a 
Rational class), etc.

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

Except you've got your mappings the wrong way around.  The cartesian 
product space of the components is the "bigger" space; the constructor 
_projects_ from the unrestricted cartesian product space into the 
potentially-more-restricted record space, potentially losing 
information. The deconstructor (or vector of accessors) embeds back from 
the restricted record space to the unrestricted space, and does not lose 
information.  (This is easy to get backwards; I often have to work it 
out from scratch when I get confused, and I have even mistyped "embed" 
for "project" once in this mail already.)

> 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 
> <https://urldefense.com/v3/__http://r.pn__;!!ACWV5N9M2RV99hQ!JQG3adQp8m1iHE_imVAw7SlzgNphGS5ZRKlDzRAUrGs3XsCgwOszFt1dkJblhuW9ishVPHZsTkA_d8xT$>()).equals(r) 
> *OR* new R(r.p1(), … r.pn 
> <https://urldefense.com/v3/__http://r.pn__;!!ACWV5N9M2RV99hQ!JQG3adQp8m1iHE_imVAw7SlzgNphGS5ZRKlDzRAUrGs3XsCgwOszFt1dkJblhuW9ishVPHZsTkA_d8xT$>()) 
> fails to terminate

Since you got your e/p backwards, you've got = / <= backwards too.

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

When you fix it, you get

     (new R(a1 .. an).p1() <= a1

which says you get a potentially normalized version of a1 out, as expected.

(I actually don't think you get as strong a component-by-component 
relation as the (1) and (2) relations you claim from the spec we have, 
but since I would have _liked_ to have gotten that, I'm not arguing with 
them.)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.org/pipermail/amber-dev/attachments/20220813/820ab003/attachment-0001.htm>