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

[Dave Abrahams]

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.

-- 
-Dave