[Proposal] [Leo RFC] Arbitrary Integer range types

[acoglio]

💥 Proposal - Leo RFC

Summary

Instead of just allowing integer values corresponding to "powers of 2" (unsigned and signed), allow types for arbitrary integer ranges.

Motivation

The type u<n> is the range 0 .. 2^<n> and the type i<n> is the range –2^<n–1> .. 2^<n–1> (where the lower bound is inclusive and the upper bound is exclusive). These power-of-2 ranges are a natural choice for bit-based computations (which is true not only for traditional computations, but also for R1CS computations when the integers are manipulated as bits), but they do not necessarily match ranges of values that may arise naturally in an application.

For instance, a variable may always take values in the range 0 .. 10. Even with the fine-grained integer types proposed in #627, its type would have to include values outside that range.

Allowing users to use arbitrary integer range types that fit the application logic improves the clarity and assurance of the program. Types like u8, i32, and u23 could be viewed as abbreviations of the obvious power of 2 ranges.

Design

This does not seems to require dramatically different machinery from what is or should be already implemented. The existing power-of-2 integer types are already treated as ranges (e.g. to ensure, statically or dynamically, that the result of an operation is representable in the type). This proposal just broadens the kinds of ranges to be handled.

The syntax could be something like int[a..b], which should not be ambiguous with array ranges because this one occurs in a type context, and in addition we would presumably make int a keyword. It might be even good for this to be reminiscent of an array range, if we consider int to be the "bidirectionally infinite array" of all integers, of which we are picking a finite range. This is just an idea; a different syntax can be used.

There would be no notational distinction between signed and unsigned: it is just a range of integers (int). But the usual unsigned/signed notation would apply to abbreviations like u8, i32, and u23 mentioned above.

Since there seems to be consensus that integer operations should not silently wraparound by default, there is no complication deriving from having to define what 'wraparound' means for ranges that do not consist of whole numbers of bits. Whatever the range is, it is a static or dynamic error if the result does not fit, and the user has to use a suitably larger range for the result.

This proposal is independent from #627, but if this proposal about arbitrary integer ranges is adopted, it would make sense to adopt that one too.

This proposal is independent from #628, but if this proposal about arbitrary integer ranges is adopted, then the inference of upper bounds discussed in that proposal could be relaxed from power-of-2 ranges (i.e. numbers of bits) to more flexible ranges.

Bitwise operations may in principle apply to values of non-power-of-2 ranges, but there is no natural "closure" of arbitrary ranges with respect to bitwise operations. Thus, we may want to limit bitwise operations to power-of-2 ranges.

Drawbacks

This makes the language and compiler more complicated, particularly in regard to bitwise operation.

Effect on Ecosystem

None?

Alternatives

Stick to the existing 10 ranges (5 unsigned + 5 signed), or to power-of-2 ranges as proposed in #627.