Open Protryon opened 3 years ago
@Protryon I think we should make all implicit upcasting explicit. In implementing a cryptographic primitive in Leo, it could be risky to support implicit upcasting. For the purposes of Leo, language safety matters a lot, and I realize this case would tradeoff ease-of-use for that slightly, but I do believe it's preferred
@Protryon I think we should make all implicit upcasting explicit. In implementing a cryptographic primitive in Leo, it could be risky to support implicit upcasting. For the purposes of Leo, language safety matters a lot, and I realize this case would tradeoff ease-of-use for that slightly, but I do believe it's preferred
I agree with Howard - use explicit syntax when upcasting. As a supporting data point, if we mirror the rust type casting syntax I expect developers familiar with rust to gravitate towards explicit casting for everything .
@collinc97 @howardwu Implicit upcasting has been removed.
The proposal looks good to me, and I agree with the explicitness of casting.
But to elaborate on the latter point a bit, I believe that:
u8
to u16
, or even u8
to i32
).
I'm just talking from a pure user surprise/error perspective; there may be other considerations, alluded to by Howard, that make explicit casting preferable in all cases. If it turns out to be a burden on users, we can re-evaluate.One common operation people will want to do is to multiply two N-bit unsigned integers to get a single 2N-bit unsigned integer. Does this proposal handle that? I could see something like
function something (a: u8, b: u8) -> ...
let c: u16 = (a * b) as u16;
...
When we discussed this proposal in meetings, I remember we also discussed overflow issues.
Is this the right issue for that or do we need a separate issue?
Right now, overflows are errors. But modular arithmetic in the integer types would be a nice feature.
Maybe there could be two forms of the arithmetic operators on integers, strict and modular.
E.g., let z = x mod+ y
would discard an overflow.
@Protryon I have a few questions about the current implementation:
-1i8 as u16 == 65535
-- sign-extend then make unsigned-1i8 as u8 == 255
-- same bits255u8 as i8 == -1
-- same bits511u16 as u8 == 255
-- discard high bits511u16 as i8 == -1
-- discard high bits-32768i16 as i8 == 0
-- discard high bits-32768i816 as u8 = 0
-- discard high bitsx
is u16
and y
is u8
, is x + y
illegal, requiring x + (y as u16)
instead?
💥 Proposal
Context
See issue #438 .
What It Is
This proposal includes explicit upcasting and downcasting for integer type values with Rust-like syntax.
Syntax
Rust-like syntax was chosen over C-like syntax to keep the parser logic as simple as possible, and avoid extra semantic ambiguity at AST level.
Explicit Cast Semantics
A given
type_cast_expression
is valid if:Downcasting will be evaluated with C-like bit truncation. Upcasting will be evaluated with normal unsigned/signed respective extension. Signedness casting will not modify the underlying bits at all, just coerce the type represented at asg/compiler level. (manifested in snarkos as moving bit gadgets between, for example,
Uint8
->Int8
)Upcasting bit extensions will be calculated BEFORE a signedness transformation if both are performed.
Examples:
Implications
as
is a new reserved keywordPossible Derivative Proposals