Get the latest tech news
What would it take to add refinement types to Rust?
A few years ago, on a whim, I wrote YAIOUOM. YAOIOUM was a static analyzer for Rust that checked that the code was using units of measures correctly, e.g. a distance in meters is not a distance in centimeters, dividing meters by seconds gave you a value in m / s (aka m * s^-1). YAIOUOM was an example of a refinement type system, i.e. a type system that does its work after another type system has already done its work. It was purely static, users could add new units in about one line of code, and it was actually surprisingly easy to write. It also couldn’t be written within the Rust type system, in part because I wanted legible error messages, and in part because Rust doesn’t offer a very good way to specify that (m / s) * s is actually the same type as m. Sadly, it also worked only on a specific version of Rust Nightly, and the code broke down with every new version of Rust. It’s a shame, because I believe that there’s lots we could do with refinement types. Simple things such as units of measure, as above, but also, I suspect, we could achieve much better error messages for complex type-level programming, such as what Diesel is doing. It got me to wonder how we could extend Rust in such a way that refinement types could be easily added to the language.
Simple things such as units of measure, as above, but also, I suspect, we could achieve much better error messages for complex type-level programming, such as what Diesel is doing. Critically, this steps 2 takes place after both trait selection and unification, which means that type variables are already either resolved or truly generic. Just as is the case for number literals, I suspect that we could live with that, and reject anything that cannot be proven correct, as long as error messages are clear enough that a developer can add the missing annotations.
Or read this on Hacker News