Associated constant assignment versus equality

proposals/p2173.md

@@ -31,6 +31,8 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 -   [Alternatives considered](#alternatives-considered)
     -   [Status quo](#status-quo)
     -   [Restrict constraints to allow computable type equality](#restrict-constraints-to-allow-computable-type-equality)
+    -   [Find a fully transitive approach to type equality](#find-a-fully-transitive-approach-to-type-equality)
+    -   [Use a different rule for "same rewrite"](#use-a-different-rule-for-same-rewrite)
     -   [Different names for same-type constraint](#different-names-for-same-type-constraint)
 
 <!-- tocstop -->
@@ -169,11 +171,23 @@ There has been a lot of work in this space. Some previous relevant proposals:
 -   [#818: generics details 3](https://github.com/carbon-language/carbon-lang/pull/818)
     introduced `where` constraints for generics, with an open question for
     whether and how we might restrict constraints in order to give a decidable
-    type equality rule. #818 addressed that question by using a non-transitive
-    rule with `observe` declarations to close the transitivity gaps.
+    type equality rule.
+    -   #818 represents the status quo of approved proposals. It has both `=`
+        and `==` where constraints, which are similar to, but somewhat different
+        from, those in this proposal.
+    -   `=` constraints require a concrete type on their right-hand side. The
+        left-hand side is not restricted. The type-of-type of the left-hand side
+        is changed to match the right-hand side.
+    -   `==` constraints do not affect the type-of-type of either operand.
+    -   As an ansewr to the question of how to produce a decidable type equality
+        rule, both kinds of constraints are applied automatically, but only at a
+        depth of one constraint. Neither form is transitive but both can be
+        transitively extended using `observe` declarations.
 -   [#2070: always `==` not `=` in `where` clauses](https://github.com/carbon-language/carbon-lang/pull/2070)
-    describes our previous approach to the "equal types with different
-    interfaces" problem.
+    describes an attempt to unify the syntax and semantics of `=` and `==`
+    constraints, under which we would always merge the type-of-types of the
+    operands. That proposal has not yet been accepted, and this proposal intends
+    to supersede it.
 
 ## Proposal
 
@@ -195,33 +209,55 @@ constraint:
     types implementing `SameAs(T)`.
 
 A type implements `C where .A = T` if and only if it implements
-`C where .A == T` – the inhabitants of these two type-of-types are the same, but
-they are different type-of-types and provide different interfaces for
-corresponding type values.
+`C where .A == T`, assuming both constraints are valid – the inhabitants of
+these two type-of-types are the same, but they are different type-of-types and
+provide different interfaces for corresponding type values.
 
 ## Details
 
 ### Rewrite constraints
 
 In a rewrite constraint, the left-hand operand of `=` must be a `.` followed by
 the name of an associated constant. `.Self` is not permitted.
-This notation is permitted anywhere a constraint can be
-written, and results in a new constraint with a different interface: the named
-member effectively no longer names an associated constant of the constrained
-type, and is instead treated as a rewrite rule that expands to the right-hand
-side of the constraint, with any mentioned parameters substituted into that
-type.
+
+```
+interface RewriteSelf {
+  // ❌ Error: `.Self` is not the name of an associated constant.
+  let Me:! Type where .Self = Self;
+}
+interface HasAssoc {
+  let Assoc:! Type;
+}
+interface RewriteSingleLevel {
+  // ✅ Argument `y` has the same type `T.Element` as parameter `x`.
+  let A:! HasAssoc where .Assoc = i32;
+}
+interface RewriteMultiLevel {
+  // ❌ Error: Only one level of associated constant is permitted.
+  let B:! RewriteSingleLevel where .A.Assoc = i32;
+}
+```
+
+This notation is permitted anywhere a constraint can be written, and results in
+a new constraint with a different interface: the named member effectively no
+longer names an associated constant of the constrained type, and is instead
+treated as a rewrite rule the expands to the right-hand side of the constraint,
+with any mentioned parameters substituted into that type.
 
 ```
 interface Container {
   let Element:! Type;
   let Slice:! Container where .Element = Element;
+  fn Add[addr me: Self*](x: Element);
 }
 // `T.Slice.Element` rewritten to `T.Element`
 //     because type of `T.Slice` says `.Element = Element`.
 // `T.Element` rewritten to `i32`
 //     because type of `T` says `.Element = i32`.
-fn A[T:! Container where .Element = i32](x: T.Slice.Element) {}
+fn Add[T:! Container where .Element = i32](p: T*, y: T.Slice.Element) {
+  // ✅ Argument `y` has the same type `T.Element` as parameter `x`.
+  p->Add(y);
+}
 ```
 
 Rewrites aren't performed on the left-hand side of such an `=`, so
@@ -237,38 +273,76 @@ is performed again, the program is invalid.
 ```
 interface Container {
   let Element:! Type;
-  // (1), bad constraint
-  let Slice:! Container where .Element = .Slice.Element;
+  let Slice:! Container where .Element = Element;
 }
-// Error, `T.Slice.Element` rewritten to
-// `T.Slice.Slice.Element` by (1), then to
-// `T.Slice.Slice.Slice.Element` by (1)
-fn A[T:! Container](x: T.Slice.Element) {}
+// ❌ Error: `.Slice.Element` rewritten to `.Element` by (1),
+// resulting in `where .Element = .Element`.
+// `T.Element` is then rewritten to `T.Element`,
+// to which the same rewrite applies again.
+fn Bad[T:! Container where .Element = .Slice.Element](x: T.Element) {}
 ```
 
+```
+interface Helper {
+  let D:! Type;
+}
+interface Example {
+  let B:! Type;
+  let C:! Helper where .D = B;
+}
+// ✅ `where .D = ...` by itself is fine.
+// `T.C.D` is rewritten to `T.B`.
+fn Allowed(T:! Example, x: T.C.D);
+// ❌ But combined with another rewrite, creates an infinite loop.
+// `.C.D` is rewritten to `.B`, resulting in `where .B = .B`.
+// Then `T.C.D` is rewritten to `T.B`, which is rewritten to itself repeatedly.
+// Using `==` instead of `=` would make this constraint redundant,
+// rather than it being an error.
+fn Error(T:! Example where .B = .C.D, x: T.C.D);
+```
+
+To determine whether two rewrite constraints are the same, each such constraint
+tracks the location of its `=` token and an optional location of a `:!` binding.
+When a constraint is used in a `:!` binding, its rewrite constraints are
+replaced with ones that track the location of that `:!` binding. Two rewrite
+constraints are the same if they track the same `=` location and the same
+optional `:!` location.
+
+> TODO: Alternative rule: if the rewrite constraint would rewrite its own
+> right-hand side, then reject. So far we have neither a proof that this is
+> sufficient to ensure termination nor a counterexample.
+
 It is valid for the same rewrite rule to be used multiple times within a type
 expression, so long as it is not used during substitution into its own
 right-hand side:
 
 ```
-interface BInterface {
-  let C:! Type;
+interface Allowed {
+  let A:! Allowed where .A = .Self;
 }
-interface AInterface {
-  let D:! AInterface;
-  let B:! BInterface where .C = Self.D;
+fn F(T:! Allowed, x: T.A.A.A);
+// ✅ Allowed, since rewrite is only applied once per sub-expression
+// In `(T.A.A).A`, the inner `T.A.A` is rewritten to `T.A`,
+// resulting in `(T.A).A`, which is then rewritten to `T.A`.
+```
+
+This rule does disallow some cases which would terminate:
+
+```
+interface FalsePositive;
+constraint ForwardDeclaredConstraint(X:! Error3);
+interface FalsePositive {
+  let X:! FalsePositive;
+  // Means `Y:! FalsePositive where .X = X.Y`
+  let Y:! ForwardDeclaredConstraint(X);
 }
-// `A.B.C` is rewritten to `Self.D`, because the type of `A.B` says `.C = Self.D`.
-//     `Self`=`A` is substituted into this giving `A.D`.
-//     During this substitution, the same rewrite rule is not used again,
-//     so this is OK.
-// Then `A.D.B.C` is rewritten to `Self.D`, because the type of `A.D.B` says
-// `.C = Self.D`.
-//     `Self`=`A.D` is substituted into this giving `A.D.D`.
-//     During this substitution, the same rewrite rule is not used again,
-//     so this is also OK, even though the same rule was used twice
-//     in forming the overall type.
-fn F(A:! AInterface, d: A.B.C.B.C) {}
+constraint ForwardDeclaredConstraint(X:! FalsePositive) {
+  extends FalsePositive where .X = X.Y;
+}
+// T.Y.Y.X -> T.Y.X.Y -> T.X.Y.Y
+// ❌ Error: applies the same rewrite twice, even
+// though there is no infinite loop.
+fn F4(T:! FalsePositive, x: T.Y.Y.X);
 ```
 
 Rewrite constraints thereby give us a deterministic, terminating type
@@ -445,6 +519,56 @@ of how we would do this have not been worked out, but this might lead to a
 coherent rule that has transitive type equality. However, this would not solve
 the "equal types with different interfaces" problem.
 
+### Find a fully transitive approach to type equality
+
+This proposal makes type equality transitive, but still has non-transitive
+"same-type" constraints describing types that are known to always eventual be
+the same after substitution, but which are not treated as the same type value
+while type-checking a generic. We could seek a type equality rule that would
+avoid having these two different kinds of equality.
+
+One candidate approach is to accept that the full generality of the equality
+problem is
+[hard](https://link.springer.com/content/pdf/10.1007/3-540-17220-3_7.pdf), but
+attempt to solve it anyway. Because of the close correspondence between Turing
+machines and string rewriting systems, this results in a type system with no
+upper bound on its runtime. We consider this unacceptable for Carbon. Swift
+handles this problem by placing a limit on the complexity of cases they will
+accept, but that seems undesirable too, as the rule cannot be readily understood
+by a developer nor effectively worked around.
+
+Another candidate approach is to find a way to reduce the inputs to the
+type-checking step as a set of non-quantified equalities. The resulting system
+of equalities can then be
+[solved efficiently](https://dl.acm.org/doi/pdf/10.1145/322186.322198) to
+determine whether two types are known to be the same. This approach appears
+sufficient to cope with locally-declared constraints, but when constraints
+appear within interfaces, they can give rise to an infinite family of
+equalities, and picking any finite subset risks the result being non-transitive
+in general, if a different subset of equalities might be considered in a
+different type-checking context.
+
+### Use a different rule for "same rewrite"
+
+We considered various rules for determining if two rewrites are using the same
+rule. The goal is to select a rule that ensures there are only finitely many
+different rewrites in a program, so that any non-termination will always be
+detected, and to minimize the occurrence of false-positives.
+
+One candidate was to consider rewrites the same if they apply to the same
+associated constant. However, it seems likely that the false positive rate for
+such a rule would be unacceptably high.
+
+Another rule would be to consider rewrites the same if they correspond to the
+same `=` token. This has the disadvantage that factoring out a common
+subexpression can result in two constraints that were previously considered
+different to now be considered the same, potentially breaking users.
+
+Connecting sameness to both the `=` token and the `:!` token is intended to
+minimize the risk of refactorings introducing false positives, while retaining a
+set of rewrite constraints that grows at most quadratically in the size of the
+program, and in practice much slower than that.
+
 ### Different names for same-type constraint
 
 We considered various options for the spelling of a same-type constraint: