Unambiguous View

[jaybosamiya-ms]

At a high level, UnambiguousView states that the View and DeepView coincide exactly. To do this, we first introduce Rust type-level equality (with TypeEq) which allows us to then define UnambigiousView.

I would like to additionally suggest that we (eventually) rename View->ShallowView and UnambiguousView->View; but I think that should be a future migration, since it would break codebases at least somewhat. For now, I have left in a comment related to this possible migration.

Additionally, obviously, naming and so on is up for bike-shedding---I am not particularly thrilled with "unambiguous view" as the name (but I do think it is better than the "both views" name that has been informally used in the past to refer to this idea).

Furthermore, while TypeEq implemented via sealed traits is kinda cute, ideally we wouldn't need to rely on sealed traits. There is some support in Rust to have equalities via associated types, but unfortunately, there appears to be a bad recursion that occurs, and so instead we have the TypeEq approach. The reason I think TypeEq is suboptimal is that the type system itself isn't aware of the equality, and thus we need to have the reflexivity conversion to remind the type system that equality is fine; if we were using a built-in type equality, then we wouldn't need that level of indirection.

EDIT: With @zeldovich noticing that associated type equality works when you try just View::V==DeepView::V (rather than what I was previously attempting, which was introducing UnambiguousView::V and trying to do UnambiguousView::V == View::V == DeepView::V, which leads to a self-recursion that the compiler does not like), we no longer need TypeEq, and can directly do equality.

---

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[jaybosamiya-ms]

The test failures are a little baffling, since they are all(?) about duplicate diagnostic items; this PR does nothing related to diagnostic items, so I am not quite sure what to do to fix this. My current hypothesis is that I might be missing some attribute somewhere, but am not sure what. The failures are reproduced locally too with:

$ vargo test -p rust_verify_test --test basic

[zeldovich]

The TypeEq trick is neat, but it seems like it's not strictly needed: I think you can get the same effect with:

use vstd::prelude::*;

verus! {

pub trait UnambiguousView
where
    Self: View,
    Self: DeepView<V = <Self as View>::V>,
 {
    proof fn all_views_are_eq(&self)
        ensures
            self.view() == self.unambiguous_view(),
            self.unambiguous_view() == self.deep_view(),
    ;

    #[verifier::inline]
    open spec fn unambiguous_view(&self) -> <Self as View>::V {
        self.view()
    }
}

struct S {}

impl View for S {
    type V = int;
    open spec fn view(&self) -> Self::V { 1 }
}

impl DeepView for S {
    type V = int;
    open spec fn deep_view(&self) -> Self::V { 1 }
}

impl UnambiguousView for S {
    proof fn all_views_are_eq(&self) {}
}

}

[jaybosamiya-ms]

Ooh, that is neat! I tried a similar version but was placing another V within UnambiguousView and ensuring equality between all 3 Vs---that causes a bad recursion problem that I alluded to in the main PR description. Doing it your way seems to remove that entire issue.

I'll update this PR when I get a few spare cycles, thanks for providing the demonstration case! I think that might also unblock a subtle issue I was facing with containers here (which is the main reason why I switched this PR to a draft).

[tjhance]

the test failure is due to an obscure test that makes sure that builtin can be embedded as a submodule rather than imported as an external crate. The only way I can make sense of the test failure is that something in your change is prompting Verus to import builtin as an external crate even when it's not supposed to. However, from a quick inspection, I don't see why this is the case. Nothing is jumping out from the macro-expanded code, either. If you could bisect and figure out exactly which code snippet is triggering the issue, it will probably help diagnose.

[tjhance]

Can you write up a bit about the intended use-case for UnambiguousView?

[tjhance]

update: I believe c38aa46 should fix the test failure, though I still don't understand why this particular PR is triggering the bug when it wasn't an issue before.

[jaybosamiya-ms]

Updated to remove the TypeEq trick, and although I am slightly sad that we won't have "John Major equality" showing up, this does clean things up a non-trivial amount (thanks @zeldovich).

Additionally, I think it unblocks support for containers. I want to mull over one specific detail for a little bit before I push UnambiguousView for containers too to this branch, so I will still keep it as a draft, but yeah, I am more confident of things working out for containers too.

---

Thanks @tjhance for looking into the CI failure. I too am surprised this triggered it, but I haven't tried to bisect it. Instead, it appears that things are passing on my latest push, so I guess things are ok again?

---

Use case: I mention this in the description, but I would like UnambiguousView to become the "main" View, with View being renamed to ShallowView. I am not doing that in this PR, but essentially this PR will unblock moving to that world. The idea of unambiguous views was proposed in the first Verus retreat a couple of years ago (although it was called "both views" then), and was generally considered a useful idea, because it made the common case remain nice, while the cases where shallow/deep matter become explicit.

As a particular example, working with (say) v1: Vec<u8>, then v1@ is unambiguous, but for a v2: Vec<Vec<u32>>, then v2@ can be confusing to new users. The mental model that some users might work with is @ gives you the spec version of things, which is kinda true, but only at the first level. Yes, a user would then figure out that they are only getting the first level view, and want a deeper view, but wouldn't it be nice if the verifier is able to help guide them towards this. In particular, we can imagine a diagnostic that says "v2@ is ambiguous, you might prefer to use v2.shallow_view() or v2.deep_view() instead". We could also imagine a new syntax for each of shallow/deep views, but I suspect many of the use cases that we are using x@, we do actually mean the unambiguous one, and there is some benefit to be had by making things explicit.

Anyways, to actually be able to test things out (possibly via a Veritas run) to know if we can switch to this explicit shallow/deep world, it is helpful to know how many situations actually break when we switch @ to mean "unambiguous only".

Again, this PR is not making any of those shifts in syntax/etc, nor is it proposing explicitly to make such shifts (other than by a singular doc comment), it is merely introducing UnambiguousView for possible future use.

Oh, and iirc, @parno had some specific use case(s) for it too.

[amaurremi]

I think establishing a clear connection between View and DeepView is valuable, as the current lack of connection often leads to unexpected errors. However, I'm concerned about introducing a third type (UnambiguousView). My understanding is that UnambiguousView applies when View and DeepView coincide exactly—but in such cases, is a new type strictly necessary? Wouldn't it be simpler to directly express View and DeepView in terms of each other?

Ideally, we could introduce more general type constraints that establish relationships between DeepView and View for particular subsets of types, such as parameterless types or containers.

Specifically,

• for parameterless types, View and DeepView definitions could naturally coincide.
• for types with type parameters that are functors, it seems straightforward to derive DeepView from View by composing view with what would be fmap deep_view in Haskell (i.e., applying view to the container itself and deep_view to its contained values).

I've drafted an example in Haskell demonstrating this approach.

I'm unsure if expressing this approach cleanly in Rust is straightforward, and I recognize it would impose constraints on the types of Views and DeepViews users can define—they would no longer be entirely arbitrary. Nevertheless, I believe these constraints would significantly improve usability in Verus, and the trade-off would be worthwhile. Users who need specialized behavior could still define their own custom View-like type classes.

[tjhance]

To be honest, I'm still not sure I understand what problem this is solving. As I understand it, the biggest complaint about the view system is that DeepView is hard to use; but the introduction of UnambiguousView doesn't address the design of DeepView at all. UnambiguousView will complicate the trait design significantly, and it will make the normal ("shallow") view harder to use.

The premise of UnambiguousView seems predicated on the idea that having both views coincide is "the common case":

[UnambiguousView] was generally considered a useful idea, because it made the common case remain nice, while the cases where shallow/deep matter become explicit.

However, I don't find this case to be particularly common, as shallow and deep views will essentially never coincide when working with generics. The specification of Vec<A>, for example has to be given in terms of "shallow" view, because there might not be any View/DeepView trait implemented for A.

[jaybosamiya-ms]

Thanks @amaurremi for writing up the Haskell version. I suspect that it is not translatable to Rust trait world due to trait resolution semantics (specifically, at least to my current understanding, we can't have specialization in the way that the OVERLAPPABLE/OVERLAPPING are doing things in the Haskell version). If you are able to translate it to Verus (or even into Rust, without yet passing Verus checks), that would be great! The

Fwiw, this PR is not introducing a new Rust/Verus type, or even a new type of view, instead it just is a constraint available for types that already have things coinciding. Users should not need to actually know of, or deal with the unambiguous view (at least in the intended final state, see below). The "for particular subsets of types" in Rust is just represented via traits, which is why we end up introducing a new trait, that's all.

---

@tjhance, to answer your question: this PR is not the final state of this feature, but is introducing the scaffolding necessary to reach the final intended state. I write more about intended final state elsewhere too, but I'll summarize below.

For Vec, we can write interesting things, but I haven't had sufficient time to flesh it out. This is the core reason I have not even marked this PR as ready-for-review. Even before final state (which will be at the end of a series of PRs to help allow for smooth migration for existing codebases), there are some design decisions that need to finish being fleshed out in this first step; thus still a draft :)

Regarding the usage: there are both expert and novice users (of both Verus and Rust), and it would help cater to both users well, especially if we can provide a better on-ramp to expert usage. Travis, you are an expert user who regularly works in parametric land: it is perfectly normal for you to work in the space where shallow/deep do not coincide; I trust you to use the correct view in any use case, making yourself explicit if necessary. However, for novice users, it is surprising and confusing to get Vec<Vec<u8>> become into Seq<Vec<u8>>, since they formed the (incorrect, but plausible) belief that @ is "this value, but in the mathematical world". Indeed, it is not implausible to have such a belief, when most of their usage has focused on situations with up to one level of genericness (i.e., most complex type used is a Vec<u8> which still is unambiguous with shallow and deep coinciding perfectly).

Now obviously, one can say "that is incorrect, and they should learn that @ just means shallow" but I believe we can provide a better on-ramp to that. Specifically, imagine if @ meant "the unambiguous view" and if it didn't apply, then the user is notified (with a nice message) saying something like "v@ is only usable when there is an unambiguous way to consider the view of v; in this case, there are two possibilities: either Seq<Vec<u8>> or Seq<Seq<u8>>; to pick the specific one, use v.shallow_view() or v.deep_view() respectively". As said, this comes with the downside of expert users who regularly have to deal with (generic) shallow views getting the extra boilerplate of .shallow_view() showing up in their code. However, I think this is a place where we can come up with a better sigil (hard, but not impossible, so I am not suggesting this) or an opt-in "@ always means shallow" or "@ always mean deep" that could apply at a module boundary.

The vision here is that for most users, they don't need to worry about the complexities of there existing various kinds of views. If they are reading someone else's code, often the specific view being taken is not particularly important either, so if they saw an @ in one of the "opted in" modules, they are not actually misled. Also, expert library authors and such aren't really inconvenienced either. If they are actually using both views in the same part of the codebase, then likely the specific choice of views matters a lot, in which case, it is better to be explicit with .shallow_view() or .deep_view() is much more helpful.

[tjhance]

@tjhance, to answer your question: this PR is not the final state of this feature, but is introducing the scaffolding necessary to reach the final intended state.

I didn't mean to imply that I thought this PR was the "final state". I was operating under the assumption that the "final state" is what was given in the PR description:

I would like to additionally suggest that we (eventually) rename View->ShallowView and UnambiguousView->View

Which I also took to mean that @ would come to mean UnambiguousView.

Unless I'm misunderstanding something, this would mean an enormous amount of code that uses @ for conciseness would need to replace it with the significantly more unwieldy .shallow_view().

However, for novice users, it is surprising and confusing to get Vec<Vec> become into Seq<Vec>, since they formed the (incorrect, but plausible) belief that @ is "this value, but in the mathematical world". Indeed, it is not implausible to have such a belief, when most of their usage has focused on situations with up to one level of genericness (i.e., most complex type used is a Vec which still is unambiguous with shallow and deep coinciding perfectly).

While I acknowledge there may be an issue for novice users, I simply don't believe this issue is significant enough to justify such a large downgrade in the utility of @.

[jaybosamiya-ms]

I 100% agree that if most code needs to be changed to .shallow_view(), then it is a significant downgrade. Indeed, I too would argue against the change in that case. However, my belief is that most code would be able to proceed as normal (especially, see the "opted in" part I mention in my prior reply). Basically, I think we should actually run an experiment to see how much code is impacted, rather than simply guess. If the amount of code impacted is small, then I think there is some happy balance that we might be able to agree upon in order to have a better experience for novices without significantly impacting expert users either.

So yes, I agree with you that if there is a massive downgrade then the benefit is not worth it. However, I suspect that the final state is not as stark as it might initially appear.

[utaal]

[retreat 2025] there may be open design decisions to resolve here

[parno]

At the retreat, there was some discussion of trying to be more disciplined about (a) implementing both view and deep_view for everything in vstd, and (b) trying to define deep_view in terms of view, along the lines that @amaurremi suggests above.

There was also a desire for a shorthand for deep_view. As shown in the informal vote tally below, changing @ to mean deep_view was popular, but it also had several detractors arguing against it. The next most popular symbol for deep_view was ~.

[utaal]

Fwiw, I wasn't present at this discussion, but I'd also vote against redefining @ as deep_view: this is both because (shallow_)view is often sufficient, and because it would be a massively breaking change.

[jaybosamiya-ms]

Similarly, I wasn't at this discussion, and I too would vote against redefining @ as deep_view.

As one might guess with this PR draft, my viewpoint (heh), is that the unambiguous view is often sufficient for most tasks. I do believe that there is work to be done to actually demonstrate that it won't be too much of a breaking change, before we even seriously consider @ to mean "unambiguous view". However, when we do consider it, based on the sigils folks seem to have voted on in the discussion, I am actually leaning towards the following (eventual) sugar, especially with keeping in mind that we already have syntax in Verus where number of squigglies going up has the meaning of "do more" (== vs =~= vs =~~=).

Suffix	Meaning
@	.unambigous_view()
@~	.shallow_view()
@~~	.deep_view()