Syntactic Musings on View Types
— 2025-04-04

Here's a silly little insight I had the other day: if you squint, both View Types and Pattern Types seem like lightweight forms of Refinement Types 1. Both will enable constraining types, but in slightly different and complementary ways. Let's take a look at this using an example of an RGB struct containing fields for individual Red, Green, and Blue channels stored as usize 2:

1

I like the term "lightweight refinement types" for the category of extensions that include pattern types and view types. To me it's reminiscent of lightweight formal methods: less thorough than the full thing, but with incredible returns for the relative effort expended.

2

Don't question why we're storing these values as usize too much. It's a little silly. For the purpose of this example just pretend there is some reason why we have to do it like this.

#[derive(Debug, Default)]
struct Rgb {
    r: usize,
    g: usize,
    b: usize,
}

Pattern types will give us the ability to directly use things like ranges or enum members in type signatures. In the following example the type usize is refined to statically only be allowed to contain values between 0..255. This is similar to the NonZero* types in the stdlib, but as part of the language and usable with arbitrary patterns:

impl Rgb {
    fn set_red(&mut self, num: usize is ..255) { .. }
    //                                   ^^^^^^^^ range pattern
}

View types are about segmenting the fields contained in self so that multiple (mutable) methods can operate on the same type without resulting in borrow checking issues. In the following example we provide mutable access to individual fields using separate methods. None of these methods take overlapping borrows of the fields in Self. This means we're free to call all of these methods, observe their return types, and we won't get any borrow checker errors. Here's an example using the syntax from Niko's latest post:

impl Rgb {
    fn red_mut(self: &mut { r } Self) -> .. { .. }
    //                    ^^^^^ view
    fn green_mut(self: &mut { g } Self) -> .. { .. }
    //                      ^^^^^ view
    fn blue_mut(self: &mut { b } Self) -> .. { .. }
    //                     ^^^^^ view
}

Here's a fun question: what happens if we combine combine Pattern Types and View Types? Both serve different purposes, and I know I've got cases where I'd like to combine them. So what would that look like? In the abstract, it seems like we would end up with something like the following:

impl Rgb {
    fn foo(self: &mut { r, g } Self is Self { r: ..255, g: ..255, .. }) {}
    //                ^^^^^^^^      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    //                  view                      pattern
}

To me that seems like a lot to read. But also rather... double? Both View Types and Pattern Types refine Self here. I would have expected us to be able to combine both. Now what if View Types and Pattern Types instead shared the same syntactic position. There's a reason View Types have to use is, so let's use that. With that we could rewrite our earlier example like this instead:

impl Rgb {
    fn foo(&mut self is Self { r: ..255, g: ..255, .. }) {}
    //               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    //                          view + pattern
}

This seems a lot more readable to me. Combining both features seems much less like a hassle here, and maybe even… nice? This updated notation would also affect our earlier View Types example. Using the updated notation would now be written the same way, but without using any patterns:

impl Rgb {
    fn red_mut(&mut self is Self { r, .. }) -> .. { .. }
    //                           ^^^^^^^^^ view
    fn green_mut(&mut self is Self { g, .. }) -> .. { .. }
    //                             ^^^^^^^^^ view
    fn blue_mut(&mut self is Self { b, .. }) -> .. { .. }
    //                            ^^^^^^^^^ view
}

I feel like this would rather neatly unify where we talk about refinements in function signatures. Notationally this reframes View Types as Pattern Types with ignored fields. Though we don't necessarily need to adopt this notation: what I care about most is that we think about how both features are intended to come together in the language to create a cohesive experience. Thanks for reading!