<div dir="ltr">On Mon, Jan 16, 2017 at 2:04 PM, Dave Abrahams <span dir="ltr"><<a href="mailto:dabrahams@apple.com" target="_blank">dabrahams@apple.com</a>></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 class="gmail-HOEnZb"><div class="gmail-h5"><br>
on Mon Jan 16 2017, Xiaodi Wu <<a href="http://xiaodi.wu-AT-gmail.com" rel="noreferrer" target="_blank">xiaodi.wu-AT-gmail.com</a>> wrote:<br>
<br>
> On Mon, Jan 16, 2017 at 12:02 PM, Stephen Canon <<a href="mailto:scanon@apple.com">scanon@apple.com</a>> wrote:<br>
><br>
>> On Jan 16, 2017, at 3:25 AM, Xiaodi Wu via swift-evolution <<br>
>> <a href="mailto:swift-evolution@swift.org">swift-evolution@swift.org</a>> wrote:<br>
>><br>
>><br>
>> Unless I'm mistaken, after removing division, models of SignedArithmetic<br>
>> would have the mathematical properties of a ring. For every element a in<br>
>> ring R, there must exist an additive inverse -a in R such that a + (-a) =<br>
>> 0. Models of Arithmetic alone would not necessarily have that property.<br>
>><br>
>><br>
>> Closure under the arithmetic operations is a sticky point for all the<br>
>> finite integer models vs. the actual ring axioms. No finite [non-modulo]<br>
>> integer type is closed, because of overflow. Similarly, additive inverses<br>
>> don’t exist for the most negative value of a signed type,<br>
>><br>
><br>
> I think this goes back to the distinct mentioned earlier: imperfection in<br>
> how we model something, or a difference in what we're modeling? Finite<br>
> memory will dictate that any model that attempts to represent integers will<br>
> face constraints. Signed integer types represent a best-effort attempt at<br>
> exactly representing the greatest possible number of integers within a<br>
> given amount of memory such that the greatest proportion of those have an<br>
> additive inverse that can be also be represented in the same amount of<br>
> memory.<br>
><br>
>> or for any non-zero value of an unsigned type.<br>
>><br>
><br>
> This is not fundamentally attributable to a limitation of how we model<br>
> something. Non-zero values of unsigned type do not have additive inverses<br>
> in the same way that non-one values of unsigned type do not have<br>
> multiplicative inverses.<br>
><br>
> The obvious way around this is to say that types conforming to Arithmetic<br>
>> model a subset of a ring that need not be closed under the operations.<br>
>><br>
><br>
> If we don't remove division, type conforming to Arithmetic would also model<br>
> a subset of a field that need not be closed under the operations. I'm not<br>
> sure it'd be wise to put such a mathematical definition on it with a "need<br>
> not" like that. Better, IMO, to give these protocols semantics based on a<br>
> positive description of the axioms that do hold--with the caveat that the<br>
> result of addition and multiplication will hold to these axioms only<br>
> insofar as the result does not overflow.<br>
<br>
</div></div>I feel like I'm mostly watching from the sidelines as the math titans<br>
duke it out, but, FWIW, that sounds pretty good to me.</blockquote><div><br></div><div>Ha, Steve is the titan. I'm just some guy who's still trying to wrap his head about this stuff. A few more comments though:</div><div><br></div><div>- Why is `signum` required on BinaryInteger? Should it not be required on SignedArithmetic instead? For signed non-integers, a signum function can be defined. It can even be generalized to complex numbers. I'm unsure, OTOH, what one does with a signum function for an unsigned integer...</div><div><br></div><div>- Why is there a static `isSigned` on BinaryInteger? All types refine either `SignedInteger` or `UnsignedInteger`, which would seem to give you the desired answer either statically or dynamically.</div><div><br></div><div>- A rough sketch of what I understand the semantics to be of these protocols so far: <a href="https://gist.github.com/xwu/a4250536ff8e5d207682079b641e9408">https://gist.github.com/xwu/a4250536ff8e5d207682079b641e9408</a></div><div><br></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"><span class="gmail-HOEnZb"><font color="#888888"><br>
--<br>
-Dave<br>
</font></span></blockquote></div><br></div></div>