The Case for Transitive Type Equality

[jsiek]

Review of the Current Design

In the current design for Carbon, type equality is not always transitive. In particular, in the context of a generic with type parameters A, B, and C, with only the constraints that A == B and B == C, the type checker thinks that A != C and will signal an error if the body of the generic includes a subexpression that tries to convert from A to C. The planned workaround for such situations is to add an observe declaration to the body of the generic such as the following:

observe A == B == C;

The primary reason for the lack of transitivity in the current design is to allow for recursive interfaces while at the same time ensuring that type checking is decidable and efficient. The following is an example of a recursive interface from the Carbon design documents. The Container interface has a GetSlice method whose return type is the associated type SliceType that is also a Container.

interface Container {
  let ElementType:! Type;

  let SliceType:! Container
	  where .ElementType == ElementType and
			.SliceType == .Self;

  fn GetSlice[addr me: Self*]
	  (start: IteratorType, end: IteratorType) -> SliceType;
}

Is Transitivity Important?

One of the questions is how often does the need for transitivity come up in the context of generic functions and classes. If it comes up a lot, then the lack of transitivity will be more problematic. On the other hand, if it does not come up very often, then the lack is less problematic. There are no other programming languages, to my knowledge, that lack transitivity, so this is uncharted territory. We would need to conduct an empirical evaluation to answer this question. If I had to take a wild guess, I would guess that transitivity comes up once in every 10 lines of code. So in a 1000-line module of generic components, one might need 100 observe declarations.

The next question is when a need for transivity arises, how difficult is it for the programmer to add the appropriate observe declarations. In the previous example, it was trivial, but in general this may not be the case. The body of a generic may contain a type conversion from a complicated type that involves A into another complicated type that involves C. The programmer would need to analyze the two type expressions and reason about why they are not equal. First, the programmer would need to identify which subexpressions are syntactially different. For those corresponding subexpressions, the programer would need to determine which of them are equal by one hop, and therefore not the problem, and which of them require transitivity. The presence of associated types of course can further complicate the story. The programmer would then add observe declarations for the later. The Carbon design docs suggest providing automation to help the programmer in this process, but it is unknown how helpful that will be.

While the lack of transitivity would be uncharted territory for a programming language, there are examples of proof assistants that lack transitivity of equality. For example, the Agda proof assistant lacks transitivity (one must explicitly apply the trans rule) whereas Coq, Isabelle, and ACL2 provide automated reasoning about equality that includes transitivity. My experience with Agda compared to Isabelle is that Agda's lack of transitivity is a constant annoyance. Part of why it is so annoying is that we all take transitivity of equality for granted. For example, one learns about transivity in high school algebra, but throughout college mathematics, one never talks about transivity, it is a trivial step that is usually handled subconsciously.

Finally, there's the question of the maintenance of observe declarations. As the body of a generic component changes, the need for observe declarations can also change. For example, a change in the code may mean that an observe declaration is no longer necessary. How does the programmer know which observe declarations are still necessary? Perhaps the type checker would need to warn about unused observe declarations, which involves some additional complexity in the type checker. Even with that help, there would remain extra churn to add and remove observe declarations.

To sum up the above discussion, I think it is likely that transitivity will be important for Carbon and that a lack of transitivity would be a constant annoyance for programmers developing generic components.

Are Recursive Interfaces Important?

While it is true that the Carbon standard library will need to have interfaces that support methods like GetSlice, there are ways to support that without using recursive interfaces. The following alternative takes advantage of the fact that the slice of a slice is the same type as the first slice. (Otherwise, the compiler would not be able to monomorphize a recursive function over slices.) In the following, the Container interface has been split into a top-level Container interface and a separate Slice interface, with their common features in the Collection interface. For Slice, the GetSlice method returns Self, whereas for Container, the GetSlice method returns the associated SliceType.

interface Collection {
  let ElementType:! Type;
}
interface Slice {
  extends Collection;
  fn GetSlice[addr me: Self*]
	  (start: IteratorType, end: IteratorType) -> Self;
}
interface Container {
  extends Collection;
  let SliceType:! Slice
	  where .ElementType == ElementType and
			.SliceType == .Self;
  fn GetSlice[addr me: Self*]
	  (start: IteratorType, end: IteratorType) -> SliceType;
}

Conclusion: Transitivity is More Important than Recursive Interfaces

To conclude, let us explicitly compare transitivity of type equality and recursive interfaces. On the one hand, transitivity has the potential to affect a significant percentage of all generic code. On the other hand, recursive interfaces make it more convenient to specify a few interfaces. Given this situation, it seems much more likely that transitivity will be more important for Carbon than recursive interfaces. I recommend that we remove recursive interfaces from the Carbon design and instead guarantee that type equality is transitive.

[josh11b]

As a FYI, the goal here is to avoid unbounded searches and arbitrary search-depth limits. I believe there are other cases where non-transitivity and observe declarations are needed to avoid those unbounded searches, though there may be some other solution that I'm not aware of. The main question requiring search besides "are these two types equal" is "does this type implement this interface". For example, an interface A could be known to be implemented if a type implements interface D due to a chain of interface requirements, as in:

interface A { }
interface B { impl as A; }
interface C { impl as B; }
interface D { impl as C; }

This could also happen due to a chain of blanket impls:

interface A { }
interface B { }
interface C { }
interface D { }

impl forall [T:! D] T as C { }
impl forall [T:! C] T as B { }
impl forall [T:! B] T as A { }

There may be another way to limit these searches, likely using some formation of the acyclic rule, though that has not been established, nor how expensive that would be at compile time.

[jsiek]

Just to be clear, the intent here is to remove the need for observe declarations for type equality. This question-for-leads does not apply to other kinds of observe declarations, such as observe declarations for impls that @josh11b mentions above.

[josh11b]

It would be valuable to go through the standard libraries of Rust and Swift to see where recursive interfaces are used, though I probably won't have time to tackle that before CppNorth. Another case to consider is mutually recursive interfaces, such as the Edge and Vertex of a graph.

A compromise position we could take is to only require observe when recursion is involved. The concern with this is it would require more complicated rules, but it could be significantly more usable in practice (given the awkward situations @zygoloid has been uncovering as part of his efforts to implement the current design), without the loss in expressivity from forbidding recursive interfaces entirely.

[josh11b]

I'd like to copy something I said on #1384 that is relevant to this issue:

The observe experiment is aiming for a simple rule to achieve these goals:

• Easy to explain
• Easy to predict
• Easy to implement
• Fast to compile

But it is an experiment since there are definite downsides that may outweigh the benefits. In particular, observe declarations themselves add code detracting from readability, writability, and compilation speed, so we really want them to be rare. They are particularly bad if which declarations are needed is difficult to predict in advance (have to round trip through a compile cycle), and if they only answer a question for the compiler not the reader.

I feel like [@zygoloid 's] recent work has been calling into question whether this rule is easy to predict and has been coming up with a variety of situations where observe declarations are needed, raising concerns that they are going to be too frequent. So I think it is definitely worth considering alternatives to the current "one-step equality" rule, and considering rules that make [the example from #1384 ] compile is a part of that.

[josh11b]

@jsiek , @zygoloid and I talked about it for a while and we could not come up with a transitive rule that was incomplete when there were recursive interfaces, nor could we figure out type equality with no recursive interfaces. For example, we were concerned about parameterization would allow users to "tie the knot" and make something that simple rules would not handle. Could you explain how you could get transitive equality even in the absence of recursive interfaces? What queries could it support ("are these two types equal?" versus "what are the type equal to this type?")?

[zygoloid]

I thought about this more over the long weekend and came up with a possible path forward that I think will give us canonical types (and hence transitive type equality) with good ergonomics for the (hopefully) common case where constraints can be viewed as one-directional rewrite rules, and admits an efficient implementation.

[github-actions[bot]]

We triage inactive PRs and issues in order to make it easier to find active work. If this issue should remain active or becomes active again, please comment or remove the inactive label. The long term label can also be added for issues which are expected to take time. This issue is labeled inactive because the last activity was over 90 days ago.

[chandlerc]

@zygoloid @josh11b - is this "decided" in as much as we have a path forward that provides (limited) transitive type equality that we're going to get some experience using?

[josh11b]

Yes, #2173 is our current attempt to address this concern.

[chandlerc]

Closing this as decided "yes we want transitive type equality". We also think we have a good compromise that preserves even more expressivity than the original issue proposed while still addressing the fundamental challenges.

The rationale for this direction (towards adding back transitive type equality) and for the particular set of tradeoffs with the current approach is documented in #2173 as well.