Assumed Audience: Programmers interested in Yao or programming language design. Or Rustaceans and anyone interested in Vale.

Epistemic Status: Fairly confident, but not as confident as I’d like because I do not have much time to implement these ideas.

Introduction

Last time, I laid out how Rust could have had more static analysis. This time, I will talk about how Rust could have had more power.

At the same time, I have been following the exploits of Evan Ovadia and his Vale programming language.

Think they are disconnected? Well, you’re right. Mostly.

But as a fellow programming language creator, I see things differently.

Vale wants to have more static analysis too, and Evan has done a great job.

So Rust is a great step. Vale is a great step. But people still want more.

To make it optimal, and to make Rust more powerful, we have to do something counterintuitive: move some things to runtime.

Traits

Instead of static traits, what if types could implement traits in multiple ways and choose the implementation at runtime?

Sounds stupid, but if a language has this, it has no need for the orphan rule. It also solves the Expression Problem!

Higher RAII

To understand Higher RAII, you need to understand the Typestate Pattern in Rust. Make sure to read that post.

tl;dr: You can use types to indicate state.

Unfortunately, when you are in the penultimate state, how do you ensure that the programmer reaches the end state? Sure, you can have a type to indicate intermediate states, but how do you create a type to indicate the end state?

The answer is: you don’t; you create a type that has to be destroyed in a specific way, and the destruction is how the program transitions to the end state.

Most literature calls these “linear types.”

Okay, there is some confusion about that term, but the key in this post is that they are meant to be types that have to be destroyed in a specific way.

Anyway, “Higher RAII” is Evan’s term for these “linear types,” though he has since adopted the “linear” moniker.

But Rust has some trouble with linear types, and so does Evan with Vale; specifically exceptions are questionable.

My language, Yao, does not have exceptions.

But it does have safe thread cancellation, so how do we handle that? I mean, linear types need to be destroyed, and if there is an existing linear type on the stack when a cancellation happens, how do you destroy it?

The answer: context stacks!

Context stacks are a construct that first appeared in Jai by Jonathan Blow. Essentially, you can create any context stack you want, and then you push values onto that stack in functions or scopes; those values are popped off when the function or scope exits.

Thus, you can use the value on the top of the stack in callees of the function that pushed the item.

For every linear type that you might use, you push a default destructor, something that would do something sane in case of cancellation.

To use Evan’s examples, a default destructor would:

  • Rollback a database transaction.
  • Cancel a future.
  • Remove a cached item from a map.

You get the idea.

And then, if there is no destructor for a specific linear type when a cancellation happens, the program crashes. Crashing is fine; after all, that’s what memory-safe programs do when they are about to violate that safety.

This could even work in the presence of exceptions!

Thus, finally, you get full linear types, even with thread cancellation and exceptions. You even get the power to choose the default at runtime, which means you can choose the ideal default in any situation.

Conclusion

As I said, it’s counterintuitive, but because of Turing-completeness, you cannot avoid moving some things to runtime.

Yes, you may even need to move things that guarantee static properties to runtime! This is what bounds checks are.

But that’s the key: you decide what static properties you want to guarantee, and then you do what you have to, at comptime or runtime, to maintain those guarantees.

And sometimes, moving things to runtime gives more power.

The main job of a programming language designer is to properly separate comptime and runtime, and then put the correct things in each.