Signed and Unsigned Integer Subtype Refinements

[Crazyblox]

Rendered

[MagmaBurnsV]

Is a supposed to be annotated as unsigned? Because it doesn't make sense to allow integer in a place that expects unsigned if unsigned <: integer.

[Crazyblox]

Should be resolved, along with an additional example for clarity.

[PhoenixWhitefire]

Not sure about the naming; signed/unsigned is not very descriptive to me. Maybe it could be (un)signedinteger instead. Consider noting the alternative names in the Alternatives section with a reason for why it was not chosen

EDIT: Resolved (maybe I should've made this a Review Comment...)

[Bottersnike]

How is

-- Accepts 'integer' and its subtypes
local function processInteger(val: integer)
    -- Type errors if val was passed as 'signed' integer subtype 
    print(integer.ult(val, 100i)) -- 'integer' refines to 'unsigned'
end

local a: integer = 10i
local b: integer = -10i

processUnsigned(a)    -- Type Error: Expected unsigned, got integer
processInteger(b)     -- Valid ('integer' refines to 'unsigned')

intended to function? Both a and b have been cast to integer, so we lost any knowledge regarding if they were signed or unsigned. Inside processInteger, val is now also just an integer (signed | unsigned) but the key problem we face is there is no way to narrow a bag of 64 bits to "signed" or "unsigned" once we've thrown away that metadata. ult would fail there because it required val to be unsigned but got signed | unsigned, but we have no way for the function to do Type errors if val was passed as 'signed' integer subtype as described, so we'd need to explicitly do integer.ult(val :: unsigned, 100i).

Something we'd also want to consider is how do constant integers infer? If we have ult(5i, 10i), is that a type error? If we have -5i we can guaranteeably type that as signed, and if we have a positive integer outside of signed range, that's unsigned, but integers between 0 and 2^63-1 can be represented with both. Do we concede that we would always have to write ult((5i) :: unsigned, (10i) :: unsigned) or would special-case logic be required for inference of integer constants used as literals in a function call?

---

Reading further down in the RFC actually there's

If a variable is typed as the general integer type, it can be used in either signed or unsigned functions. The type checker treats this as a valid "promotion" to the required refinement.

How would we represent this? integer = signed & unsigned? Purely conceptually, the intersection of signed and unsigned would be any number [0, 2^63-1], but notably not [-2^63, -1] (signed only) nor [2^64, 2^64-1] (unsigned only). Is that inaccuracy something that would be considered just waved away?

I do think waving away that conceptual inaccuracy would resolve the issues suggested above, with a literal would always infer as integer. It still leaves integers in a position where a single use of integer instead of signed or unsigned suddenly loses all signed-ness information, though I think that battle was lost when integers were added in their current state.

It would be interesting to see some discussion of inference in the RFC in general. Inferring a negative constant as always signed, for example, would be very useful.

---

Just one final edit: This is quite a wall of text, but I'm very much in support of adding proper signed and unsigned types!

[Bottersnike]

I think it's important to note that

and refine it internally

isn't possible. There's no way at runtime to ever discern between a signed or unsigned integer, and therefore once the types no longer carry that information they likewise have no reasonable checks that could be used as part of refinemt.

[Crazyblox]

Providing the equivalent of :: signed or :: unsigned within the relevant integer library functions would be sufficient to avoid runtime behaviour, which the RFC is stated multiple times to not involve.

[Bottersnike]

I was meaning more in as much as any code that takes an integer can't safely know to cast it to one or the other. I'm not suggesting types should leak to runtime, but rather that there's no runtime behaviour that could be used to determine if/how an integer should be refined. A quick ::signed or ::unsigned, in the same way you can do

int64_t foo = -1;
uint64_t bar = (uint64_t)foo;

In C is fine, but I'm not sure if it's worth mentioning given that's not something that can be "safely" done, except when intentionally breaking rules (bit maths on negative numbers, etc.). Would :: signed and :: unsigned not work fine here?