Generics: Set associated constants using `where` constraints (#1013)

Change the syntax for setting the associated constants and types in an interface implementation for a type from using `let` declarations as in:
```
class Vector(T:! Type) {
  impl as Iterable {
    let ElementType:! Type = T;
    ...
  }
}
```
to using `where` clauses as in:
```
class Vector(T:! Type) {
  impl as Iterable where .ElementType = T {
    ...
  }
}
```

This is an attempt to simplify by removing redundancy, improve consistency by removing a use of `let` that was different than other examples, and better support forward declaration that a type implements an interface while retaining the information needed for type checking.

Co-authored-by: Richard Smith <richard@metafoo.co.uk>

docs/design/generics/details.md

@@ -112,6 +112,7 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
     -   [Bridge for C++ customization points](#bridge-for-c-customization-points)
     -   [Variadic arguments](#variadic-arguments)
     -   [Range constraints on generic integers](#range-constraints-on-generic-integers)
+    -   [Separate declaration and definition of impl](#separate-declaration-and-definition-of-impl)
 -   [References](#references)
 
 <!-- tocstop -->
@@ -1900,13 +1901,13 @@ interface NSpacePoint {
 }
 ```
 
-Implementations of `NSpacePoint` for different types might have different values
-for `N`:
+An implementation of an interface specifies values for associated constants with
+a [`where` clause](#where-constraints). For example, implementations of
+`NSpacePoint` for different types might have different values for `N`:
 
 ```
 class Point2D {
-  impl as NSpacePoint {
-    let N:! i32 = 2;
+  impl as NSpacePoint where .N = 2 {
     fn Get[addr me: Self*](i: i32) -> f64 { ... }
     fn Set[addr me: Self*](i: i32, value: f64) { ... }
     fn SetAll[addr me: Self*](value: Array(f64, 2)) { ... }
@@ -1914,8 +1915,7 @@ class Point2D {
 }
 
 class Point3D {
-  impl as NSpacePoint {
-    let N:! i32 = 3;
+  impl as NSpacePoint where .N = 3 {
     fn Get[addr me: Self*](i: i32) -> f64 { ... }
     fn Set[addr me: Self*](i: i32, value: f64) { ... }
     fn SetAll[addr me: Self*](value: Array(f64, 3)) { ... }
@@ -1923,7 +1923,16 @@ class Point3D {
 }
 ```
 
-And these values may be accessed as members of the type:
+Multiple assignments to associated constants may be joined using the `and`
+keyword. The list of assignments is subject to two restrictions:
+
+-   An implementation of an interface cannot specify a value for a
+    [`final`](#final-members) associated constant.
+-   If an associated constant doesn't have a
+    [default value](#interface-defaults), every implementation must specify its
+    value.
+
+These values may be accessed as members of the type:
 
 ```
 Assert(Point2D.N == 2);
@@ -2021,9 +2030,8 @@ class DynamicArray(T:! Type) {
   fn Insert[addr me: Self*](pos: IteratorType, value: T);
   fn Remove[addr me: Self*](pos: IteratorType);
 
-  impl as StackAssociatedType {
-    // Set the associated type `ElementType` to `T`.
-    let ElementType:! Type = T;
+  // Set the associated type `ElementType` to `T`.
+  impl as StackAssociatedType where .ElementType = T {
     fn Push[addr me: Self*](value: ElementType) {
       me->Insert(me->End(), value);
     }
@@ -2442,6 +2450,10 @@ constraint Point2DInterface {
 }
 ```
 
+This syntax is also used to specify the values of
+[associated constants](#associated-constants) when implementing an interface for
+a type.
+
 **Concern:** Using `=` for this use case is not consistent with other `where`
 clauses that write a boolean expression that evaluates to `true` when the
 constraint is satisfied.
@@ -2486,6 +2498,9 @@ constraint IntStack {
 }
 ```
 
+This syntax is also used to specify the values of
+[associated types](#associated-types) when implementing an interface for a type.
+
 ##### Equal generic types
 
 Alternatively, two generic types could be constrained to be equal to each other,
@@ -3534,8 +3549,7 @@ lexically in the class' scope:
 
 ```
 class Vector(T:! Type) {
-  impl as Iterable {
-    let ElementType:! Type = T;
+  impl as Iterable where .ElementType = T {
     ...
   }
 }
@@ -3545,8 +3559,7 @@ This is equivalent to naming the type between `impl` and `as`:
 
 ```
 class Vector(T:! Type) {
-  impl Vector(T) as Iterable {
-    let ElementType:! Type = T;
+  impl Vector(T) as Iterable where .ElementType = T {
     ...
   }
 }
@@ -3556,13 +3569,13 @@ An impl may be declared [external](#external-impl) by adding an `external`
 keyword before `impl`. External impls may also be declared out-of-line:
 
 ```
-external impl [T:! Type] Vector(T) as Iterable {
-  let ElementType:! Type = T;
+external impl [T:! Type] Vector(T) as Iterable
+    where .ElementType = T {
   ...
 }
 // This syntax is also allowed:
-external impl Vector(T:! Type) as Iterable {
-  let ElementType:! Type = T;
+external impl Vector(T:! Type) as Iterable
+    where .ElementType = T {
   ...
 }
 ```
@@ -3758,9 +3771,8 @@ where blanket impls arise:
 -   `T` implements `CommonType(T)` for all `T`
 
     ```
-    external impl [T:! Type] T as CommonType(T) {
-      let Result:! auto = T;
-    }
+    external impl [T:! Type] T as CommonType(T)
+        where .Result = T { }
     ```
 
     This means that every type is the common type with itself.
@@ -3857,6 +3869,8 @@ parameters are replaced the declarations are normalized as follows:
     between the `impl` and `as` keywords if the type is left out.
 -   Pointer types `T*` are replaced with `Ptr(T)`.
 -   The `external` keyword is removed, if present.
+-   Any `where` clauses that are setting associated constants or types are
+    removed.
 
 The type structure will always contain a single interface name, which is the
 name of the interface being implemented, and some number of type names. Type
@@ -3995,12 +4009,10 @@ interface True {}
 impl Y as True {}
 interface Z(T:! Type) { let Cond:! Type; }
 match_first {
-  impl [T:! Type, U:! Z(T) where .Cond is True] T as Z(U) {
-    let Cond:! Type = N;
-  }
-  impl [T:! Type, U:! Type] T as Z(U) {
-    let Cond:! Type = Y;
-  }
+  impl [T:! Type, U:! Z(T) where .Cond is True] T as Z(U)
+      where .Cond = N { }
+  impl [T:! Type, U:! Type] T as Z(U)
+      where .Cond = Y { }
 }
 ```
 
@@ -4026,15 +4038,12 @@ class B {}
 class C {}
 interface D(T:! Type) { let Cond:! Type; }
 match_first {
-  impl [T:! Type, U:! D(T) where .Cond = B] T as D(U) {
-    let Cond:! Type = C;
-  }
-  impl [T:! Type, U:! D(T) where .Cond = A] T as D(U) {
-    let Cond:! Type = B;
-  }
-  impl [T:! Type, U:! Type] T as D(U) {
-    let Cond:! Type = A;
-  }
+  impl [T:! Type, U:! D(T) where .Cond = B] T as D(U)
+      where .Cond = C { }
+  impl [T:! Type, U:! D(T) where .Cond = A] T as D(U)
+      where .Cond = B { }
+  impl [T:! Type, U:! Type] T as D(U)
+      where .Cond = A { }
 }
 ```
 
@@ -4121,15 +4130,13 @@ interface Deref {
 // Types implementing `Deref`
 class Ptr(T:! Type) {
   ...
-  external impl as Deref {
-    let Result:! Type = T;
+  external impl as Deref where .Result = T {
     fn DoDeref[me: Self]() -> Result { ... }
   }
 }
 class Optional(T:! Type) {
   ...
-  external impl as Deref {
-    let Result:! Type = T;
+  external impl as Deref where .Result = T {
     fn DoDeref[me: Self]() -> Result { ... }
   }
 }
@@ -4159,16 +4166,14 @@ To mark an impl as not able to be specialized, prefix it with the keyword
 class Ptr(T:! Type) {
   ...
   // Note: added `final`
-  final external impl as Deref {
-    let Result:! Type = T;
+  final external impl as Deref where .Result = T {
     fn DoDeref[me: Self]() -> Result { ... }
   }
 }
 class Optional(T:! Type) {
   ...
   // Note: added `final`
-  final external impl as Deref {
-    let Result:! Type = T;
+  final external impl as Deref where .Result = T {
     fn DoDeref[me: Self]() -> Result { ... }
   }
 }
@@ -4539,6 +4544,14 @@ between multiple generic integer parameters. For example, if `J < K` and
 secondary syntactic concern about how to write this kind of constraint on a
 parameter, as opposed to an associated type, as in `N:! u32 where ___ >= 2`.
 
+### Separate declaration and definition of impl
+
+There is a desire to support a short declaration that a type implements an
+interface without giving a full definition of that implementation for API files.
+Everything needed for type checking is provided in the interface definition,
+except for the assignments to associated constants and types, and so those must
+be included in the declaration as well.
+
 ## References
 
 -   [#553: Generics details part 1](https://github.com/carbon-language/carbon-lang/pull/553)
@@ -4549,3 +4562,4 @@ parameter, as opposed to an associated type, as in `N:! u32 where ___ >= 2`.
 -   [#950: Generic details 6: remove facets](https://github.com/carbon-language/carbon-lang/pull/950)
 -   [#983: Generic details 7: final impls](https://github.com/carbon-language/carbon-lang/pull/983)
 -   [#990: Generics details 8: interface default and final members](https://github.com/carbon-language/carbon-lang/pull/990)
+-   [#1013: Generics: Set associated constants using where constraints](https://github.com/carbon-language/carbon-lang/pull/1013)

docs/design/generics/overview.md

@@ -197,8 +197,8 @@ class Song {
   // ...
 
   // Implementing `Printable` for `Song` inside the definition of `Song`
-  // means all names of `Printable`, such as `F`, are included as a part
-  // of the `Song` API.
+  // without the keyword `external` means all names of `Printable`, such
+  // as `F`, are included as a part of the `Song` API.
   impl as Printable {
     // Could use `Self` in place of `Song` here.
     fn Print[me: Song]() { ... }
@@ -594,6 +594,15 @@ Constraints limit the types that the generic function can operate on, but
 increase the knowledge that may be used in the body of the function to operate
 on values of those types.
 
+Constraints are also used when implementing an interface to specify the values
+of associated types (and other associated constants).
+
+```
+class Vector(T:! Movable) {
+  impl as Stack where .ElementType = T { ... }
+}
+```
+
 ### Parameterized impls
 
 Implementations can be parameterized to apply to multiple types. Those
@@ -634,3 +643,4 @@ priority order in a prioritization block.
 -   [#818: Constraints for generics (generics details 3)](https://github.com/carbon-language/carbon-lang/pull/818)
 -   [#920: Generic parameterized impls (details 5)](https://github.com/carbon-language/carbon-lang/pull/920)
 -   [#950: Generic details 6: remove facets](https://github.com/carbon-language/carbon-lang/pull/950)
+-   [#1013: Generics: Set associated constants using `where` constraints](https://github.com/carbon-language/carbon-lang/pull/1013)

docs/design/generics/terminology.md

@@ -655,11 +655,11 @@ class ListIterator(ElementType:! Type) {
 }
 class List(ElementType:! Type) {
   // Iterator type is determined by the container type.
-  let IteratorType:! Iterator = ListIterator(ElementType);
-  fn Insert[addr me: Self*](position: IteratorType, value: ElementType) {
-    ...
+  impl as Container where .IteratorType = ListIterator(ElementType) {
+    fn Insert[addr me: Self*](position: IteratorType, value: ElementType) {
+      ...
+    }
   }
-  impl as Container;
 }
 ```
 
@@ -682,18 +682,9 @@ interface Addable(T:! Type) {
 An `i32` value might support addition with `i32`, `u16`, and `f64` values.
 
 ```
-impl i32 as Addable(i32) {
-  let ResultType:! Type = i32;
-  // ...
-}
-impl i32 as Addable(u16) {
-  let ResultType:! Type = i32;
-  // ...
-}
-impl i32 as Addable(f64) {
-  let ResultType:! Type = f64;
-  // ...
-}
+impl i32 as Addable(i32) where .ResultType = i32 { ... }
+impl i32 as Addable(u16) where .ResultType = i32 { ... }
+impl i32 as Addable(f64) where .ResultType = f64 { ... }
 ```
 
 To write a generic function requiring a parameter to be `Addable`, there needs
@@ -756,3 +747,4 @@ available in the body of the function.
 -   [#447: Generics terminology](https://github.com/carbon-language/carbon-lang/pull/447)
 -   [#731: Generics details 2: adapters, associated types, parameterized interfaces](https://github.com/carbon-language/carbon-lang/pull/731)
 -   [#950: Generic details 6: remove facets](https://github.com/carbon-language/carbon-lang/pull/950)
+-   [#1013: Generics: Set associated constants using where constraints](https://github.com/carbon-language/carbon-lang/pull/1013)

proposals/p1013.md

@@ -0,0 +1,172 @@
+# Generics: Set associated constants using `where` constraints
+
+<!--
+Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+Exceptions. See /LICENSE for license information.
+SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+-->
+
+[Pull request](https://github.com/carbon-language/carbon-lang/pull/1013)
+
+<!-- toc -->
+
+## Table of contents
+
+-   [Problem](#problem)
+-   [Background](#background)
+-   [Proposal](#proposal)
+-   [Rationale based on Carbon's goals](#rationale-based-on-carbons-goals)
+-   [Alternatives considered](#alternatives-considered)
+    -   [Status quo](#status-quo)
+    -   [`with` and `,` instead of `where` and `and`](#with-and--instead-of-where-and-and)
+-   [Future work](#future-work)
+
+<!-- tocstop -->
+
+## Problem
+
+There are a variety of contexts that currently use the keyword `let`:
+
+-   declaring associated constants or types in an interface,
+-   defining associated constants or types in an implementation,
+-   defining local constant in a function body, and
+-   defining class constants.
+
+In all but the implementation case, the semantics are generally similar to the
+semantics of passing a value into a function, with some erasing of the specific
+value passed and using the type to determine how the name can legally be used.
+However,
+[proposal #950](https://github.com/carbon-language/carbon-lang/pull/950) has
+changed the `let` in an implementation to use the value specified, not its type,
+creating an inconsistency with the other uses of `let`.
+
+Furthermore, we have come to the realization that we still want to specify the
+values of associated constants and types for an implementation even in an API
+file where we only want to make a forward declaration. This makes that
+information available to clients that only look at the API file, who need to
+know those values for type checking, but otherwise don't need to see the full
+definition of the implementation. This suggests that those assignments should be
+declared outside of definition block's curly braces `{`...`}`.
+
+Lastly, there is a bit of redundancy in Carbon since `where` clauses are also a
+way of specifying the values of associated constants and types in other Carbon
+contexts.
+
+## Background
+
+The `let` syntax for setting an associated type in an interface implementation
+was originally decided in issue
+[#739: Associated type syntax](https://github.com/carbon-language/carbon-lang/issues/739)
+and implemented in proposal
+[#731: Generics details 2: adapters, associated types, parameterized interfaces](https://github.com/carbon-language/carbon-lang/pull/731).
+
+Proposal
+[#950: Generics details 6: remove facets](https://github.com/carbon-language/carbon-lang/pull/950)
+made two relevant changes:
+
+-   The type part of a `let` in an `impl` block is no longer "load bearing": the
+    only legal types are `auto` and whatever was in the corresponding interface.
+    In particular, the `let` in an `impl` block does not erase.
+-   There is now a defined meaning for a generic `let` statement in a function
+    body that can erase depending on the type specified.
+
+Combined with the `let` in an interface giving you an erased type, or archetype,
+this has made the meaning of `let` in an `impl` block inconsistent with other
+places using `let`.
+
+## Proposal
+
+The suggested change is to use a `where` clause as part of an `impl` declaration
+to specify associated constants and types instead of `let` declarations inside
+of the `impl` definition. In effect, it removes `let` declarations from `impl`
+blocks in exchange for allowing an `impl` declaration to implement a constraint
+expression instead of a simple interface or named constraint.
+
+This proposal updates the following design docs on the generics feature to
+reflect this change:
+
+-   [docs/design/generics/overview.md](/docs/design/generics/overview.md)
+-   [docs/design/generics/terminology.md](/docs/design/generics/terminology.md)
+-   [docs/design/generics/details.md](/docs/design/generics/details.md)
+
+## Rationale based on Carbon's goals
+
+As a simplification, this proposal advances the goal of having Carbon
+[code that is easy to read, understand, and write](/docs/project/goals.md#code-that-is-easy-to-read-understand-and-write).
+In particular, having a simple specification and be simple to implement.
+
+This is an example of
+[the "prefer providing only one way to do a given thing" principle](/docs/project/principles/one_way.md),
+by switching to a single way of specifying associated constants and values.
+
+## Alternatives considered
+
+### Status quo
+
+The main alternative considered was the status quo. We did have two concerns
+with this proposal, however we felt that this behavior would not be surprising
+to developers in practice.
+
+**Concern:** Due to interface defaults, it is possible for copy-pasting the
+type-of-type expression from an `impl` block in a `class` into a constraint in a
+function signature to give a constraint that is weaker than what that impl block
+actually delivers.
+
+**Concern:** Because a specialization of an `impl` can change the values of
+associated constants, a type might not actually satisfy a constraint that it
+appears to implement when that constraint specifies the values of associated
+constants. In this example:
+
+```
+interface Bar {
+  let X:! Type;
+}
+class Foo(T:! Type) {
+  impl as Bar where .X = T { ... }
+}
+```
+
+it appears that `Foo(T)` satisfies the constraint that `Bar where .X = T`, but
+there could be specializations that set `.X` to different values for some
+specific values of `T`.
+
+### `with` and `,` instead of `where` and `and`
+
+Instead of matching the syntax used when specifying constraints, we could have
+used a different syntax to highlight that this is assigning instead of
+constraining. The suggestion that came up in discussion was using `with` instead
+of `where` and a comma `,` instead of `and` to join multiple clauses.
+
+We decided that it would not be good to have two syntaxes that were very similar
+but different, and that there was some benefit to be able to copy-paste between
+the constraint context and the implementation context.
+
+## Future work
+
+This proposal will allow us to support declaring that a type implements an
+interface inside an API file separate from the definition of the `impl`, even
+for internal `impl`s. However, that feature is waiting on resolution of
+[#472: Open question: Calling functions defined later in the same file](https://github.com/carbon-language/carbon-lang/issues/472)
+and proposal
+[#875: Principle: information accumulation](https://github.com/carbon-language/carbon-lang/pull/875).
+
+If and when we do add support declaration of impls without definition, we will
+need to answer the question: do you have to repeat `where` constraints from a
+forward declaration of an impl when it is later defined?
+
+```
+class Vector(T:! Type) {
+  impl as Container where .Element = T and .Iter = VectIter(T);
+}
+
+// Probably okay:
+fn Vector(T:! Type).(Container.Begin)[me: Self]() ...
+
+// Maybe okay:
+class Vector(T:! Type) {
+  // Not repeating constraints on .Element and .Iter above:
+  impl as Container {
+    fn Begin[me: Self]() ...
+  }
+}
+```