[Proposal] Type Casting Implementation

[Protryon]

💥 Proposal

Context

See issue #438 .

What It Is

This proposal includes explicit upcasting and downcasting for integer type values with Rust-like syntax.

Syntax

type_cast_expression := primary_expression "as" type_ref
primary_expression := <prior definition of primary expression> | type_cast_expression

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:

1. The target type and source type are both integers.

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:

let k: u32 = 5i32 as u32;
let m: u16 = 5u32 as u16;
let n: u16 = 5i32 as u16;
let n: u16 = -5i32 as u16;
let n: i8 = 255u16 as i8;

Implications

• as is a new reserved keyword

Possible Derivative Proposals

• Array type downcasting ([u16] -> [u8])
• Array type upcasting with length-flooring or zero padding ([u8] -> [u16])
• Field <-> int type casting

[howardwu]

@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

[collinc97]

@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 .

[Protryon]

@collinc97 @howardwu Implicit upcasting has been removed.

[acoglio]

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:

• Any casting that may change the numeric value should be definitely explicit (e.g. downcasting).
• It would be fine to have implicit casting when the numeric value doesn't change (e.g. 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.

[bendyarm]

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;
   ...

[bendyarm]

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.

[acoglio]

@Protryon I have a few questions about the current implementation:

• Are casts supported exclusively between integer types, and no other types?
• Are the following true?
  • -1i8 as u16 == 65535 -- sign-extend then make unsigned
  • -1i8 as u8 == 255 -- same bits
  • 255u8 as i8 == -1 -- same bits
  • 511u16 as u8 == 255 -- discard high bits
  • 511u16 as i8 == -1 -- discard high bits
  • -32768i16 as i8 == 0 -- discard high bits
  • -32768i816 as u8 = 0 -- discard high bits
• Does the compiler's evaluator error when a cast changes the mathematical value (as in all the examples above)?
• Are there no automatic/implicit conversions/promotions from smaller to larger types with the same signedness (which always preserve the mathematical value)? E.g. if x is u16 and y is u8, is x + y illegal, requiring x + (y as u16) instead?

[Protryon]

1. Yes. integer -> integer only.
2. yes, yes, yes, yes, yes, yes, yes
3. not at the moment
4. There are no implicit conversions, similar to rust.