Idea: Optics types, combining pattern types and view types

language design
1

Here is a naive idea inspired by the optics (lens and prisms) in bidirectional transformation. Given the view types like lens that provides partial view and update for product types, and pattern types like prisms that provides partial view and update for sum types, the idea is to combine them together: the optics type that provides partial view and update for both product types and sum types.

Here is the syntax sketch.

struct Foo {
    x: i32,
    y: Bar,
}

enum Bar {
    A,
    B(i32),
    C {
        p: i32,
        q: i32,
    }
}

fn foo(
    // lens that views and updates x of Foo
    a: &mut optics_type!(Foo is .{ x, .. }),
    // prisms that views and updates Bar::B(_) of lens y of Foo
    b: &mut optics_type!(Foo is .{ y: Bar::B(_), .. }),
) {
    *a.x += 1;
    // `b.y` is guaranteed to be `Bar::B` so here it is exhaustive.
    let Bar::B(ref mut b) = b.y;
    *b += 1;
}

fn main() {
    let mut foo = Foo { x: 0, y: Bar::B(0) };
    foo(&mut foo, &mut foo);
}

With path-sensitive type checks (like that where we check if a field of a given type is moved), it is even possible to introduce prism types that can change the discriminant of an enum (but only allowed to use in function parameters).

// After calling this function, the discriminant of `c` is guaranteed 
// to be changed from `B` to `C`.
fn bar(c: &mut optics_type!(Bar is B(_) => C { .. })) {
    let Bar::B(b) = c;
    *c = Bar::C { p: b, q: b };
}
2

Do you have any ideas on how this might be implemented. Does it involve unsafe wrapped in a safe interface? Could you give some details?

That being said, it looks like an interesting proposal.

3

as far as i can see, your proposal is "just" view types + pattern types, so it is unclear why a new optics_type! compiler macro should be necessary.

of course neither feature is close to stabilization so it is rather hard to tell what may or may not be possible, but it is true that it is important to make sure that they do work together

4

First, introduce new subtyping rules: (for convenience, write $ty is $pat as optics_types!($ty is $pat), $ty1 <: $ty2 as $ty1 is the subtype of $ty2).

  • for product types: (T1, T2) <: (T1, T2) is (_, ..), i.e. types that view more fields are subtype of types that view less fields.
  • for sum types: Option<T> is Some(_) <: Option<T>, i.e., the types that specify more strict discriminants are subtype of types that specify less strict discriminants.

Patterns in the optics types will be used for pattern exhaustiveness analysis. Subtyping conversion results are recorded during type checking and used for borrow check later.

Then, add new type rules for expressions:

  • the type of an integral literal expression carries that const pattern, e.g. the type of 42i32 is i32 is 42.
  • the type of an enum constructor is the pattern type with that discriminant, e.g. the type of Some(0i32) is Option<i32> is Some(0).

After that, add a new rule of borrow checking: for each mutable-mutable, or mutable-immutable borrow conflict pair reported by the original borrow checker, visit their subtyping conversion results, and check if their patterns overlap, and only report those where their patterns overlap as errors.

Taking the same example:

struct Foo {
    x: i32,
    y: Bar,
}

enum Bar {
    A,
    B(i32),
    C {
        p: i32,
        q: i32,
    }
}

We have:

  • Foo <: Foo is .{ x, .. }
  • Foo is .{ x: 0, .. } <: Foo is .{ x, .. }
  • Foo <: Foo is .{ y: Bar::B(_), .. })
  • Bar is B(_) <: Bar
  • Foo is .{ y: Bar::B(_), .. }) <: Foo is .{ y, .. }

The struct expression Foo { x: 0, y: Bar::B(0) } has type Foo is .{ x: 0, y: Bar::B(0) }. Then foo(&mut foo, &mut foo) does such type transformations:

    foo(&mut foo, &mut foo)
 :  fn(&mut Foo is .{ x: 0, y: Bar::B(0) }, &mut Foo is .{ x: 0, y: Bar::B(0) })
<:  fn(&mut Foo is .{ x: 0, .. }, &mut Foo is .{ y: Bar::B(0) })
<:  fn(&mut Foo is .{ x, .. }, &mut Foo is .{ y: Bar::B(_) })

which finishes type checking.

At borrowck, &mut foo, &mut foo are reported at first by the original borrowck (the NLL checker or Polonius), but they are converted to &mut Foo is .{ x, .. }, &mut Foo is . { y: Bar::B(_) } where their patterns don't overlap, so they will not be reported as borrow errors.

5

Here optics_type! is just a randomly picked name for combined view types and pattern types.