<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<br>
<blockquote type="cite" cite="mid:CAJuA9EimeJYuHUQbRq=W3p=w1F1eLN3XnQ9K=7KAV5746aTUfA@mail.gmail.com">
<div>
<div class="gmail_quote">
<div dir="auto">There are actually two conditions in the
definition of an embedding-projection pair (I am using “o”
for function composition below);</div>
<div dir="auto"><br>
</div>
<div dir="auto">1) p o e = id</div>
<div dir="auto">2) e o p <= id </div>
<div dir="auto"><br>
</div>
<div dir="auto">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</div>
</div>
</div>
</blockquote>
<br>
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. <br>
<br>
<blockquote type="cite" cite="mid:CAJuA9EimeJYuHUQbRq=W3p=w1F1eLN3XnQ9K=7KAV5746aTUfA@mail.gmail.com">
<div>
<div class="gmail_quote">
<div dir="auto">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,</div>
</div>
</div>
</blockquote>
<br>
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.) <br>
<br>
<blockquote type="cite" cite="mid:CAJuA9EimeJYuHUQbRq=W3p=w1F1eLN3XnQ9K=7KAV5746aTUfA@mail.gmail.com">
<div>
<div class="gmail_quote">
<div dir="auto">1) means:</div>
<div dir="auto"><br>
</div>
<div dir="auto">(new R(a1, …, an)).p1().equals(a1)</div>
<div dir="auto">… and …</div>
<div dir="auto">(new R(a1, …, an)).pn().equals(an)</div>
<div dir="auto"><br>
</div>
<div dir="auto">2) means (roughly)</div>
<div dir="auto"><br>
</div>
<div dir="auto">new R(r.p1(), …, <a href="https://urldefense.com/v3/__http://r.pn__;!!ACWV5N9M2RV99hQ!JQG3adQp8m1iHE_imVAw7SlzgNphGS5ZRKlDzRAUrGs3XsCgwOszFt1dkJblhuW9ishVPHZsTkA_d8xT$" moz-do-not-send="true">r.pn</a>()).equals(r) *OR* new
R(r.p1(), … <a href="https://urldefense.com/v3/__http://r.pn__;!!ACWV5N9M2RV99hQ!JQG3adQp8m1iHE_imVAw7SlzgNphGS5ZRKlDzRAUrGs3XsCgwOszFt1dkJblhuW9ishVPHZsTkA_d8xT$" moz-do-not-send="true">r.pn</a>()) fails to terminate</div>
</div>
</div>
</blockquote>
<br>
Since you got your e/p backwards, you've got = / <= backwards
too.<br>
<br>
<blockquote type="cite" cite="mid:CAJuA9EimeJYuHUQbRq=W3p=w1F1eLN3XnQ9K=7KAV5746aTUfA@mail.gmail.com">
<div>
<div class="gmail_quote">
<div dir="auto">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.</div>
</div>
</div>
</blockquote>
<br>
When you fix it, you get<br>
<br>
(new R(a1 .. an).p1() <= a1<br>
<br>
which says you get a potentially normalized version of a1 out, as
expected. <br>
<br>
(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.) <br>
<br>
</body>
</html>