On Mon, Jan 16, 2017 at 2:04 PM, Dave Abrahams <dabrah...@apple.com> wrote:
> > on Mon Jan 16 2017, Xiaodi Wu <xiaodi.wu-AT-gmail.com> wrote: > > > On Mon, Jan 16, 2017 at 12:02 PM, Stephen Canon <sca...@apple.com> > wrote: > > > >> On Jan 16, 2017, at 3:25 AM, Xiaodi Wu via swift-evolution < > >> swift-evolution@swift.org> wrote: > >> > >> > >> Unless I'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. > >> > >> > >> 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, > >> > > > > I think this goes back to the distinct mentioned earlier: imperfection in > > how we model something, or a difference in what we'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. > > > >> or for any non-zero value of an unsigned type. > >> > > > > 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. > > > > 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. > >> > > > > If we don't remove division, type conforming to Arithmetic would also > model > > a subset of a field that need not be closed under the operations. I'm not > > sure it'd be wise to put such a mathematical definition on it with a > "need > > not" 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. > > I feel like I'm mostly watching from the sidelines as the math titans > duke it out, but, FWIW, that sounds pretty good to me. 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: - 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... - 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. - A rough sketch of what I understand the semantics to be of these protocols so far: https://gist.github.com/xwu/a4250536ff8e5d207682079b641e9408 > -- > -Dave >
_______________________________________________ swift-evolution mailing list swift-evolution@swift.org https://lists.swift.org/mailman/listinfo/swift-evolution