<div dir="ltr">On Mon, Jan 16, 2017 at 12:02 PM, Stephen Canon <span dir="ltr">&lt;<a href="mailto:scanon@apple.com" target="_blank">scanon@apple.com</a>&gt;</span> wrote:<br><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><div style="word-wrap:break-word"><span class="gmail-"><blockquote type="cite">On Jan 16, 2017, at 3:25 AM, Xiaodi Wu via swift-evolution &lt;<a href="mailto:swift-evolution@swift.org" target="_blank">swift-evolution@swift.org</a>&gt; wrote:<br></blockquote><div><blockquote type="cite"><div><div style="font-family:helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><br class="gmail-m_7691912612560415340Apple-interchange-newline">Unless I&#39;m mistaken, after removing division, models of SignedArithmetic would have the mathematical properties of a ring. For every element a in ring R, there must exist an additive inverse -a in R such that a + (-a) = 0. Models of Arithmetic alone would not necessarily have that property.</div></div></blockquote></div><br></span><div>Closure under the arithmetic operations is a sticky point for all the finite integer models vs. the actual ring axioms.  No finite [non-modulo] integer type is closed, because of overflow. Similarly, additive inverses don’t exist for the most negative value of a signed type,</div></div></blockquote><div><br></div><div>I think this goes back to the distinct mentioned earlier: imperfection in how we model something, or a difference in what we&#39;re modeling? Finite memory will dictate that any model that attempts to represent integers will face constraints. Signed integer types represent a best-effort attempt at exactly representing the greatest possible number of integers within a given amount of memory such that the greatest proportion of those have an additive inverse that can be also be represented in the same amount of memory.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><div style="word-wrap:break-word"><div>or for any non-zero value of an unsigned type.</div></div></blockquote><div><br></div><div>This is not fundamentally attributable to a limitation of how we model something. Non-zero values of unsigned type do not have additive inverses in the same way that non-one values of unsigned type do not have multiplicative inverses.</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><div style="word-wrap:break-word"><div>The obvious way around this is to say that types conforming to Arithmetic model a subset of a ring that need not be closed under the operations.</div></div></blockquote><div><br></div><div>If we don&#39;t remove division, type conforming to Arithmetic would also model a subset of a field that need not be closed under the operations. I&#39;m not sure it&#39;d be wise to put such a mathematical definition on it with a &quot;need not&quot; like that. Better, IMO, to give these protocols semantics based on a positive description of the axioms that do hold--with the caveat that the result of addition and multiplication will hold to these axioms only insofar as the result does not overflow.</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><div style="word-wrap:break-word"><div>– Steve</div></div></blockquote></div><br></div></div>