Low-level Simplicity has no built-in integer types, and integers are interpretations of trees of bits. As a result, SimplicityHL supports a feature called structural typecasting which allows joining and splitting integer types. You can think of this as something like typographically inserting or deleting a space in the exact middle of a representation of an integer or integers (the exact rules about which typecasts are allowed here are more detailed and refer to the underlying tree representation). In base 10 we could imagine
31415926 ←→ 3141 5926
Just adding or removing the separator lets us interpret the same number as a single larger integer or a pair of smaller integers, without actually doing any calculations at all. In reality these would be in binary, like
1110001110001000 ←→ 11100011 10001000
When we’ve asked AIs to optimize existing programs, they’ve often found ways to use this feature, for example to reduce the number of jet calls when computing a hash. Instead of calling jet::sha_256_ctx_8_add_1 four times with four u8 values, we can structurally represent the values as single u32 value (with no overhead) and call jet::sha_256_ctx_8_add_4 just one time. Some other calls can also benefit from similar refactoring, although hashing is the most common example so far.
Unfortunately, the existing syntax for structural typecasting is cumbersome, and human developers reach for it less often and find large typecast expressions rather hard to read.
For example, @stringhandler found a very hard-to-read refactor that an AI proposed in the SHRINCS verifier project that uses this notation repeatedly.
Even the basic uses of this notation are sometimes a bit confusing to users. For example, a standard definition in many contracts is
fn not(bit: bool) -> bool {
<u1>::into(jet::complement_1(<bool>::into(bit)))
}
which uses this notation twice (once to turn a bool into a u1, and again to turn a u1 back into a bool). This notation isn’t far off from one of Rust’s typecast notations, but appears more cumbersome in some cases, and one tricky thing is that the named type is the source type, not the target type (the target type is implicit and is inferred by the compiler according to what is needed in a specific context). Thus <u1>::into() produces a bool when the compiler expects a bool, but the actual target type is not stated anywhere in the conversion. That makes me fear that this notation is actually optimized for the compiler’s convenience more than for the user’s convenience. (Also, the compiler already knows the source type as well here: it is already clear that bit is a bool and that the output of jet::complement_1() is a u1 due to other declarations.)
It would be nice to have a more streamlined and readable typecasting notation available. I think it would make developers more comfortable routinely using structural typecasts, for example in the repeated hashing jet call setting.
I realize we might want different short-term and long-term remedies to this situation, because of the project to completely refactor or replace SimplicityHL’s underlying type system, which might eventually change what sorts of typecasts the compiler is able to perform automatically.
There may be reasons not to use Rust’s as keyword (it applies to conversions in Rust that are absolutely not structural typecasts in SimplicityHL, and Rust programmers might assume that it works for those too, although they’d probably get a useful error back), but it feels nice to me to envision a syntax more like
fn not(bit: bool) -> bool {
jet::complement_1(bit as u1) as bool
}
Again, I think the compiler already knows everything that it needs to make this work properly!