Linear and affine types in SimplicityHL

SimplicityHL development
1

In SimplicityHL, all objects are currently passed to functions “by value” and by copying the value. (Under the hood, we use the pair “parallel composition” combinator which does exactly this, copies a value into the input of two expressions.)

However, for smart contracts it’s very important that API authors be able to design session types and for this we need the ability for functions/expressions to “consume” variables. For example, in the prototypical “raw hashing” code

let ctx1: Ctx8 = jet::sha_256_ctx_8_init();
let ctx2: Ctx8 = jet::sha_256_ctx_8_add_2(ctx1, 0x5120);
let ctx3: Ctx8 = jet::sha_256_ctx_8_add_32(ctx2, tweaked_key);
let hash: u256 = jet::sha_256_ctx_8_finalize(ctx3);

We have three ctx* variables, all of which are live. If you replace the final ctx3 with ctx2 say, you will skip hashing tweaked_key and it will be pretty hard for a reviewer to notice this. (Like in Rust, you can name all of these ctx, with each one shadowing the previous ones, which will help in this particular case, but this isn’t particularly general and can be a footgun.)

It would be better if the sha256 jets (or some HL wrapper around them) were to consume their sha256 context objects, and if the user actually intends to “fork” the context they should have to write some sort of explicit copy keyword.

In Rust, this behavior is mediated by the Copy trait and the borrowing system, which lets you avoid copying by passing “shared” or “unique” references. Functions and expressions declare (via their type signature) whether they expect a value, a shared reference, or a unique reference. Then the passed type gets to choose, via Copy, whether “a value” means that the function “moves” (invalidates the original binding) the object or not. The result is pretty natural-feeling, mainly because Rust has references, and the “borrowing rules” are designed to match sensible rules to prevent pointer invalidation.

Rust lacks “linear types”, meaning types that are not Copy (can only be used once) and also must be consumed (must be used once). This prevents lots of natural constructions and leads to weird hacks like the #[must_use] lint, but is hard to fit into the language since it has infinite loops and memory leaks and stuff.

HL does not have references, nor do we want to introduce a borrow checker (anytime soon). We do not have infinite loops or memory leaks. So I think we can introduce linear and affine types without too much trouble. The questions become:

  • Should types or function signatures (or somehow both) be responsible for deciding whether a passed value is passed “by move” or “by copy”?
  • For linear types which must be consumed, how do users implement the “final” consumption? (In Rust it’s been proposed to use destructuring syntax, so if you have a linear type struct MyType { inner: u32 } then you can only get rid of it by writing let MyType { inner: _ } = mytype. This has the nice benefit that it reuses the privacy system to determine who is allowed to destructure the type. Specifically, anyone who can name all fields can destructure. (Though Rust has special .. syntax that lets you destructure without naming fields, which interacts poorly with these proposals.)
  • What escape hatches should exist?

I would propose:

  • Types by default are linear. To make them affine (users are not required to consume them) you need to annotate it with some sort of “autodrop” annotation
  • Types can be annotated to enable explicit copying (similar to Rust Clone) or implicit copying (similar to Rust Copy).
  • Linear types are consumed by destructuring.
  • Functions can “opt in” to consuming their arguments, so if you pass them an object that would otherwise be Copy it will get consumed anyway.

Then the SHA256 context, for example, would be “linear” and also support explicit copies. So you can fork the context all you want, but every context eventually would need to go into a finalize call to get destructured. (And I guess we should also add a drop method which just consumes the context without doing any hashing.)

I don’t have any strong opinions about what these annotations would look like.

2

I think this is a very valuable feature, but it’s also in some tension with our claim to be Rustlike and our claim to be nearly already writable by Rust developers. This might be an argument against having these mechanisms be the default rather than something to opt into, at least if we want to keep saying that we look and feel like Rust here.

is an example that is decently idiomatic as Rust-like SimplicityHL, but that technically wouldn’t work if every variable were a linear type by default. Line 29 would cause a compiler error about oracle_height’s multiplicity (and line 37, not shown in this preview, also has the same problem when it goes to check the oracle signature). I actually predict that almost anything using an oracle statement would run into this problem because you have one consumption of the oracle statement to check its validity, and one consumption of the oracle statement to actually use its value as part of the contract logic.

There are also scattered examples that I found in some of my own demo programs, like a taxicab number checker that manually cubes integers, or many uses of the state management MVP where you first load() a state value to check that the current UTXO really committed to that value, and then separately confirm that individual witness values can successfully regenerate it/correspond to it (thereby using the state value itself at least twice).

3

In Rust if the Height type was not explicitly marked Copy, you would get a compiler error because of multiplicity.