[swift-evolution] protocol-oriented integers (take 2)

[Xiaodi Wu]

On Mon, Jan 16, 2017 at 2:04 PM, Dave Abrahams <dabrahams at 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 <scanon at apple.com>
> wrote:
> >
> >> On Jan 16, 2017, at 3:25 AM, Xiaodi Wu via swift-evolution <
> >> swift-evolution at 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.swift.org/pipermail/swift-evolution/attachments/20170116/0213e341/attachment.html>