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]

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.