Update Generics terminology document (#3048)

This reflects changes from a number of approved proposals:
- #920 : concrete statements about orphan and overlap in Carbon
- #2138 : "generic" -> "checked generic", "template" -> "template
generic"
- #2188 : binding patterns are forbidden in type position
- #2360 : "type", "facet type", "facet". Note: I am not using the term
"generic type" from #2360 since that meaning conflicts with the
generally accepted meaning of "generic type" of a type with a
compile-time parameter.
- #2760 / #2770 : internal/external impl -> extending impl
- #2964 : "symbolic constant" and "template constant"

---------

Co-authored-by: Geoff Romer <gromer@google.com>
Co-authored-by: Richard Smith <richard@metafoo.co.uk>

docs/design/classes.md

@@ -1595,7 +1595,7 @@ class MyDerivedClass {
 
 The properties of a type, whether type is abstract, base, or final, and whether
 the destructor is virtual or non-virtual, determines which
-[type-of-types](/docs/design/generics/terminology.md#type-of-type) it satisfies.
+[type-of-types](/docs/design/generics/terminology.md#facet-type) it satisfies.
 
 -   Non-abstract classes are `Concrete`. This means you can create local and
     member variables of this type. `Concrete` types have destructors that are
@@ -1623,7 +1623,7 @@ conform to the decision on
 | final    | any         | yes        | yes         | yes            |
 
 The compiler automatically determines which of these
-[type-of-types](/docs/design/generics/terminology.md#type-of-type) a given type
+[type-of-types](/docs/design/generics/terminology.md#facet-type) a given type
 satisfies. It is illegal to directly implement `Concrete`, `Deletable`, or
 `Destructible` directly. For more about these constraints, see
 ["destructor constraints" in the detailed generics design](/docs/design/generics/details.md#destructor-constraints).

docs/design/expressions/implicit_conversions.md

@@ -184,8 +184,8 @@ var r: Base** = &p;
 
 ### Type-of-types
 
-A type `T` with [type-of-type](../generics/terminology.md#type-of-type) `TT1`
-can be implicitly converted to the type-of-type `TT2` if `T`
+A type `T` with [type-of-type](../generics/terminology.md#facet-type) `TT1` can
+be implicitly converted to the type-of-type `TT2` if `T`
 [satisfies the requirements](../generics/details.md#subtyping-between-type-of-types)
 of `TT2`.
 

docs/design/generics/details.md

@@ -202,9 +202,9 @@ When the implementation of `ConvertibleToString` for `Song` is defined as
 internal, every member of `ConvertibleToString` is also a member of `Song`. This
 includes members of `ConvertibleToString` that are not explicitly named in the
 `impl` definition but have defaults. Whether the implementation is defined as
-[internal](terminology.md#internal-impl) or
-[external](terminology.md#external-impl), you may access the `ToString` function
-for a `Song` value `s` by a writing function call
+[internal](terminology.md#extending-an-impl) or
+[external](terminology.md#extending-an-impl), you may access the `ToString`
+function for a `Song` value `s` by a writing function call
 [using a qualified member access expression](terminology.md#qualified-member-access-expression),
 like `s.(ConvertibleToString.ToString)()`.
 
@@ -359,8 +359,8 @@ class Player {
 ### External impl
 
 Interfaces may also be implemented for a type
-[externally](terminology.md#external-impl), by using `impl` without `extend`. An
-external impl does not add the interface's methods to the type.
+[externally](terminology.md#extending-an-impl), by using `impl` without
+`extend`. An external impl does not add the interface's methods to the type.
 
 ```
 class Point2 {
@@ -597,7 +597,7 @@ var v: Point = AddAndScaleGeneric(a, w, 2.5);
 ```
 
 Here `T` is a type whose type is `Vector`. The `:!` syntax means that `T` is a
-_[generic parameter](terminology.md#generic-versus-template-parameters)_. That
+_[generic parameter](terminology.md#checked-versus-template-parameters)_. That
 means it must be known to the caller, but we will only use the information
 present in the signature of the function to type check the body of
 `AddAndScaleGeneric`'s definition. In this case, we know that any value of type
@@ -628,13 +628,13 @@ acts like a [supertype](https://en.wikipedia.org/wiki/Subtyping) of any `T`
 implementing `Vector`.
 
 For name lookup purposes, an archetype is considered to have
-[implemented its constraint internally](terminology.md#internal-impl). The only
-oddity is that the archetype may have different names for members than specific
-types `T` that implement interfaces from the constraint
-[externally](terminology.md#external-impl). This difference in names can also
-occur for supertypes in C++, for example members in a derived class can hide
-members in the base class with the same name, though it is not that common for
-it to come up in practice.
+[implemented its constraint internally](terminology.md#extending-an-impl). The
+only oddity is that the archetype may have different names for members than
+specific types `T` that implement interfaces from the constraint
+[externally](terminology.md#extending-an-impl). This difference in names can
+also occur for supertypes in C++, for example members in a derived class can
+hide members in the base class with the same name, though it is not that common
+for it to come up in practice.
 
 The behavior of calling `AddAndScaleGeneric` with a value of a specific type
 like `Point` is to set `T` to `Point` after all the names have been qualified.
@@ -648,8 +648,8 @@ fn AddAndScaleForPoint(a: Point, b: Point, s: Double) -> Point {
 
 This qualification gives a consistent interpretation to the body of the function
 even when the type supplied by the caller
-[implements the interface externally](terminology.md#external-impl), as `Point2`
-does:
+[implements the interface externally](terminology.md#extending-an-impl), as
+`Point2` does:
 
 ```
 // AddAndScaleGeneric with T = Point2
@@ -805,7 +805,7 @@ An interface's name may be used in a few different contexts:
 -   to define [an `impl` for a type](#implementing-interfaces),
 -   as a namespace name in
     [a qualified name](#qualified-member-names-and-compound-member-access), and
--   as a [type-of-type](terminology.md#type-of-type) for
+-   as a [type-of-type](terminology.md#facet-type) for
     [a generic type parameter](#generics).
 
 While interfaces are examples of type-of-types, type-of-types are a more general
@@ -813,7 +813,7 @@ concept, for which interfaces are a building block.
 
 ## Type-of-types
 
-A [type-of-type](terminology.md#type-of-type) consists of a set of requirements
+A [type-of-type](terminology.md#facet-type) consists of a set of requirements
 and a set of names. Requirements are typically a set of interfaces that a type
 must satisfy, though other kinds of requirements are added below. The names are
 aliases for qualified names in those interfaces.
@@ -883,7 +883,7 @@ whenever an interface may be. This includes all of these
     [a qualified name](#qualified-member-names-and-compound-member-access). For
     example, `VectorLegoFish.VAdd` refers to the same name as `Vector.Add`.
 -   A named constraint may be used as a
-    [type-of-type](terminology.md#type-of-type) for
+    [type-of-type](terminology.md#facet-type) for
     [a generic type parameter](#generics).
 
 We don't expect developers to directly define many named constraints, but other
@@ -1910,7 +1910,7 @@ fn Complex64.CloserToOrigin[self: Self](them: Self) -> bool {
 ### Use case: Accessing external names
 
 Consider a case where a function will call several functions from an interface
-that is [implemented externally](terminology.md#external-impl) for a type.
+that is [implemented externally](terminology.md#extending-an-impl) for a type.
 
 ```
 interface DrawingContext {
@@ -1924,9 +1924,10 @@ impl Window as DrawingContext { ... }
 ```
 
 An adapter can make that much more convenient by making a compatible type where
-the interface is [implemented internally](terminology.md#internal-impl). This
-avoids having to [qualify](terminology.md#qualified-member-access-expression)
-each call to methods in the interface.
+the interface is [implemented internally](terminology.md#extending-an-impl).
+This avoids having to
+[qualify](terminology.md#qualified-member-access-expression) each call to
+methods in the interface.
 
 ```
 class DrawInWindow {
@@ -2195,7 +2196,7 @@ class DynamicArray(T:! type) {
 ```
 
 For context, see
-["Interface type parameters and associated types" in the generics terminology document](terminology.md#interface-type-parameters-and-associated-types).
+["Interface type parameters and associated types" in the generics terminology document](terminology.md#interface-parameters-and-associated-constants).
 
 **Comparison with other languages:** Both
 [Rust](https://doc.rust-lang.org/book/ch19-03-advanced-traits.html#specifying-placeholder-types-in-trait-definitions-with-associated-types)
@@ -2245,7 +2246,7 @@ interface at most once.
 If instead you want a family of related interfaces, one per possible value of a
 type parameter, multiple of which could be implemented for a single type, you
 would use
-[parameterized interfaces](terminology.md#interface-type-parameters-and-associated-types).
+[parameterized interfaces](terminology.md#interface-parameters-and-associated-constants).
 To write a parameterized version of the stack interface, instead of using
 associated types, write a parameter list after the name of the interface instead
 of the associated type declaration:
@@ -3166,8 +3167,8 @@ fn F[T:! Transitive](t: T) {
 A value of type `A`, such as the return value of `GetA()`, has the API of `P`.
 Any such value also implements `Q`, and since the compiler can see that by way
 of a single `where` equality, values of type `A` are treated as if they
-implement `Q` [externally](terminology.md#external-impl). However, the compiler
-will require a cast to `B` or `C` to see that the type implements `R`.
+implement `Q` [externally](terminology.md#extending-an-impl). However, the
+compiler will require a cast to `B` or `C` to see that the type implements `R`.
 
 ```
 fn TakesPQR[U:! P & Q & R](u: U);
@@ -3624,8 +3625,8 @@ In particular, the compiler should in general avoid monomorphizing to generate
 multiple instantiations of the function in this case.
 
 **Open question:** Should `TypeId` be
-[implemented externally](terminology.md#external-impl) for types to avoid name
-pollution (`.TypeName`, `.TypeHash`, etc.) unless the function specifically
+[implemented externally](terminology.md#extending-an-impl) for types to avoid
+name pollution (`.TypeName`, `.TypeHash`, etc.) unless the function specifically
 requests those capabilities?
 
 ### Destructor constraints
@@ -5695,9 +5696,9 @@ be [implied constraints](#implied-constraints) on the function's parameters.
 
 ### Specialization
 
-[Specialization](terminology.md#generic-specialization) is used to improve
-performance in specific cases when a general strategy would be inefficient. For
-example, you might use
+[Specialization](terminology.md#checked-generic-specialization) is used to
+improve performance in specific cases when a general strategy would be
+inefficient. For example, you might use
 [binary search](https://en.wikipedia.org/wiki/Binary_search_algorithm) for
 containers that support random access and keep their contents in sorted order
 but [linear search](https://en.wikipedia.org/wiki/Linear_search) in other cases.

docs/design/generics/goals.md

@@ -53,18 +53,18 @@ forward-looking.
 
 ## Background
 
-Carbon will support
-[generics](terminology.md#generic-versus-template-parameters) to support generic
-programming by way of
-[parameterization of language constructs](terminology.md#parameterized-language-constructs)
-with [early type checking](terminology.md#early-versus-late-type-checking) and
+Carbon will support both
+[checked and template generics](terminology.md#checked-versus-template-parameters)
+to support generic programming by way of
+[compile-time parameterization of language constructs](terminology.md#generic-means-compile-time-parameterized).
+
+Carbon's checked generics will feature
+[early type checking](terminology.md#early-versus-late-type-checking) and
 [complete definition checking](terminology.md#complete-definition-checking).
 
-This is in contrast with the
+Carbon's template generics, in contrast, will more closely follow the
 [compile-time duck typing](https://en.wikipedia.org/wiki/Duck_typing#Templates_or_generic_types)
-approach of C++ templates, and _in addition_ to
-[template support in Carbon](#relationship-to-templates), if we decide to
-support templates in Carbon beyond interoperability with C++ templates.
+approach of C++ templates.
 
 ### Generic parameters
 

docs/design/generics/overview.md

@@ -180,7 +180,7 @@ definition is required after seeing the call sites once all the
 [instantiations](terminology.md#instantiation) are known.
 
 Note: [Generics terminology](terminology.md) goes into more detail about the
-[differences between generics and templates](terminology.md#generic-versus-template-parameters).
+[differences between generics and templates](terminology.md#checked-versus-template-parameters).
 
 ### Implementing interfaces
 
@@ -259,7 +259,7 @@ specific type value assigned to `T` is not known when type checking the
 `SortVector` function. Instead it is the constraints on `T` that let the
 compiler know what operations may be performed on values of type `T`. Those
 constraints are represented by the type of `T`, a
-[**_type-of-type_**](terminology.md#type-of-type).
+[**_type-of-type_**](terminology.md#facet-type).
 
 In general, a type-of-type describes the capabilities of a type, while a type
 defines specific implementations of those capabilities. An interface, like
@@ -519,7 +519,7 @@ specific sort order.
 
 ### Interface input and output types
 
-[Associated types and interface parameters](terminology.md#interface-type-parameters-and-associated-types)
+[Associated types and interface parameters](terminology.md#interface-parameters-and-associated-constants)
 allow function signatures to vary with the implementing type. The biggest
 difference between these is that associated types ("output types") may be
 deduced from a type, and types can implement the same interface multiple times

docs/design/generics/terminology.md

@@ -10,8 +10,8 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 
 ## Table of contents
 
--   [Parameterized language constructs](#parameterized-language-constructs)
--   [Generic versus template parameters](#generic-versus-template-parameters)
+-   [Generic means compile-time parameterized](#generic-means-compile-time-parameterized)
+-   [Checked versus template parameters](#checked-versus-template-parameters)
     -   [Polymorphism](#polymorphism)
         -   [Parametric polymorphism](#parametric-polymorphism)
         -   [Compile-time duck typing](#compile-time-duck-typing)
@@ -21,6 +21,12 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
     -   [Definition checking](#definition-checking)
         -   [Complete definition checking](#complete-definition-checking)
         -   [Early versus late type checking](#early-versus-late-type-checking)
+-   [Bindings](#bindings)
+-   [Types and `type`](#types-and-type)
+-   [Facet type](#facet-type)
+-   [Facet](#facet)
+-   [Type expression](#type-expression)
+-   [Facet binding](#facet-binding)
 -   [Deduced parameter](#deduced-parameter)
 -   [Interface](#interface)
     -   [Structural interfaces](#structural-interfaces)
@@ -28,8 +34,7 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
     -   [Named constraints](#named-constraints)
 -   [Associated entity](#associated-entity)
 -   [Impl: Implementation of an interface](#impl-implementation-of-an-interface)
-    -   [Internal impl](#internal-impl)
-    -   [External impl](#external-impl)
+    -   [Extending an impl](#extending-an-impl)
 -   [Member access](#member-access)
     -   [Simple member access](#simple-member-access)
     -   [Qualified member access expression](#qualified-member-access-expression)
@@ -46,50 +51,60 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 -   [Instantiation](#instantiation)
 -   [Specialization](#specialization)
     -   [Template specialization](#template-specialization)
-    -   [Generic specialization](#generic-specialization)
+    -   [Checked-generic specialization](#checked-generic-specialization)
 -   [Conditional conformance](#conditional-conformance)
--   [Interface type parameters and associated types](#interface-type-parameters-and-associated-types)
+-   [Interface parameters and associated constants](#interface-parameters-and-associated-constants)
 -   [Type constraints](#type-constraints)
--   [Type-of-type](#type-of-type)
 -   [References](#references)
 
 <!-- tocstop -->
 
-## Parameterized language constructs
+## Generic means compile-time parameterized
 
-Generally speaking, when we talk about either templates or a generics system, we
-are talking about generalizing some language construct by adding a parameter to
-it. Language constructs here primarily would include functions and types, but we
-may want to support parameterizing other language constructs like
-[interfaces](#interface-type-parameters-and-associated-types).
+Generally speaking, when we talk about _generics_, either
+[checked or template](#checked-versus-template-parameters), we are talking about
+generalizing some language construct by adding a compile-time parameter, called
+a _generic parameter_, to it. So:
+
+-   a _generic function_ is a function with at least one compile-time parameter,
+    which could be an explicit argument to the function or
+    [deduced](#deduced-parameter);
+-   a _generic type_ is a function with a compile-time parameter, for example a
+    container type parameterized by the type of the contained elements;
+-   a _generic interface_ is an [interface](#interface) with
+    [a compile-time parameter](#interface-parameters-and-associated-constants).
 
 This parameter broadens the scope of the language construct on an axis defined
 by that parameter, for example it could define a family of functions instead of
 a single one.
 
-## Generic versus template parameters
+Note that different languages allow different things to be parameterized; for
+example, Rust supports
+[generic associated types](https://rust-lang.github.io/rfcs/1598-generic_associated_types.html).
+
+## Checked versus template parameters
 
-When we are distinguishing between generics and templates in Carbon, it is on a
+When we distinguish between checked and template generics in Carbon, it is on a
 parameter by parameter basis. A single function can take a mix of regular,
-generic, and template parameters.
+checked, and template parameters.
 
 -   **Regular parameters**, or "dynamic parameters", are designated using the
     "\<name>`:` \<type>" syntax (or "\<value>").
--   **Generic parameters** are designated using `:!` between the name and the
+-   **Checked parameters** are designated using `:!` between the name and the
     type (so it is "\<name>`:!` \<type>").
 -   **Template parameters** are designated using "`template` \<name>`:!`
     \<type>".
 
-The syntax for generic and template parameters was decided in
+The syntax for checked and template parameters was decided in
 [questions-for-leads issue #565](https://github.com/carbon-language/carbon-lang/issues/565).
 
-Expected difference between generics and templates:
+Expected difference between checked and template parameters:
 
 <table>
   <tr>
-   <td><strong>Generics</strong>
+   <td><strong>Checked</strong>
    </td>
-   <td><strong>Templates</strong>
+   <td><strong>Template</strong>
    </td>
   </tr>
   <tr>
@@ -107,7 +122,7 @@ Expected difference between generics and templates:
   <tr>
    <td>name lookup resolved for definitions in isolation ("early")
    </td>
-   <td>some name lookup may require information from calls (name lookup may be "late")
+   <td>name lookup can use information from arguments (name lookup may be "late")
    </td>
   </tr>
   <tr>
@@ -138,7 +153,7 @@ Expected difference between generics and templates:
 
 ### Polymorphism
 
-Generics and templates provide different forms of
+Generics provide different forms of
 [polymorphism](<https://en.wikipedia.org/wiki/Polymorphism_(computer_science)>)
 than object-oriented programming with inheritance. That uses
 [subtype polymorphism](https://en.wikipedia.org/wiki/Subtyping) where different
@@ -186,19 +201,19 @@ Templates work with ad-hoc polymorphism in two ways:
     will only resolve that call after the types are known.
 
 In Carbon, we expect there to be a compile error if overloading of some name
-prevents a generic function from being typechecked from its definition alone.
-For example, let's say we have some overloaded function called `F` that has two
-overloads:
+prevents a checked-generic function from being typechecked from its definition
+alone. For example, let's say we have some overloaded function called `F` that
+has two overloads:
 
 ```
 fn F[template T:! type](x: T*) -> T;
 fn F(x: Int) -> bool;
 ```
 
-A generic function `G` can call `F` with a type like `T*` that cannot possibly
-call the `F(Int)` overload for `F`, and so it can consistently determine the
-return type of `F`. But `G` can't call `F` with an argument that could match
-either overload.
+A checked generic function `G` can call `F` with a type like `T*` that cannot
+possibly call the `F(Int)` overload for `F`, and so it can consistently
+determine the return type of `F`. But `G` can't call `F` with an argument that
+could match either overload.
 
 **Note:** It is undecided what to do in the situation where `F` is overloaded,
 but the signatures are consistent and so callers could still typecheck calls to
@@ -220,15 +235,15 @@ they could be removed and the function would still have the same capabilities.
 Constraints only affect the caller, which will use them to resolve overloaded
 calls to the template and provide clearer error messages.
 
-With generics using constrained genericity, the function body can be checked
-against the signature at the time of definition. Note that it is still perfectly
-permissible to have no constraints on a type; that just means that you can only
-perform operations that work for all types (such as manipulate pointers to
-values of that type) in the body of the function.
+With checked generics using constrained genericity, the function body can be
+checked against the signature at the time of definition. Note that it is still
+perfectly permissible to have no constraints on a type; that just means that you
+can only perform operations that work for all types (such as manipulate pointers
+to values of that type) in the body of the function.
 
 ### Dependent names
 
-A name is said to be _dependent_ if it depends on some generic or template
+A name is said to be _dependent_ if it depends on some checked or template
 parameter. Note: this matches
 [the use of the term "dependent" in C++](https://www.google.com/search?q=c%2B%2B+dependent+name),
 not as in [dependent types](https://en.wikipedia.org/wiki/Dependent_type).
@@ -236,11 +251,11 @@ not as in [dependent types](https://en.wikipedia.org/wiki/Dependent_type).
 ### Definition checking
 
 Definition checking is the process of semantically checking the definition of
-parameterized code for correctness _independently_ of any particular arguments.
-It includes type checking and other semantic checks. It is possible, even with
-templates, to check semantics of expressions that are not
+parameterized code for correctness _independently_ of any particular argument
+values. It includes type checking and other semantic checks. It is possible,
+even with templates, to check semantics of expressions that are not
 [dependent](#dependent-names) on any template parameter in the definition.
-Adding constraints to template parameters and/or switching them to be generic
+Adding constraints to template parameters and/or switching them to be checked
 allows the compiler to increase how much of the definition can be checked. Any
 remaining checks are delayed until [instantiation](#instantiation), which can
 fail.
@@ -250,21 +265,114 @@ fail.
 Complete definition checking is when the definition can be _fully_ semantically
 checked, including type checking. It is an especially useful property because it
 enables _separate_ semantic checking of the definition, a prerequisite to
-separate compilation. It also enables implementation strategies that don’t
-instantiate the implementation (for example, [type erasure](#type-erasure) or
+separate compilation. It also is a requirement for implementation strategies
+that don’t instantiate the implementation (for example,
+[type erasure](#type-erasure) or
 [dynamic-dispatch witness tables](#dynamic-dispatch-witness-table)).
 
 #### Early versus late type checking
 
 Early type checking is where expressions and statements are type checked when
 the definition of the function body is compiled, as part of definition checking.
-This occurs for regular and generic values.
+This occurs for regular and checked-generic values.
 
 Late type checking is where expressions and statements may only be fully
 typechecked once calling information is known. Late type checking delays
 complete definition checking. This occurs for
 [template-dependent](#dependent-names) values.
 
+## Bindings
+
+_Binding patterns_ associate a name with a type and a value. This is used to
+declare function parameters, in `let` and `var` declarations, as well as to
+declare [generic parameters](#generic-means-compile-time-parameterized). There
+are three kinds of binding patterns, corresponding to
+[the three value phases](/docs/design/README.md#value-categories-and-value-phases):
+
+-   A _runtime binding pattern_ binds to a dynamic value at runtime, and is
+    written using a `:`, as in `x: i32`.
+-   A _symbolic constant binding pattern_ or _symbolic binding pattern_ binds to
+    a compile-time value that is not known when type checking, and is used to
+    declare [checked generic](#checked-versus-template-parameters) parameters.
+    These binding use `:!`, as in `T:! type`.
+-   A _template constant binding pattern_ or _template binding pattern_ binds to
+    a compile-time value that is known when type checking, and is used to
+    declare [template](#checked-versus-template-parameters) parameters. These
+    bindings use the keyword `template` in addition to `:!`, as in
+    `template T:! type`.
+
+The last two binding patterns, which are about binding a compile-time value, are
+called _constant binding patterns_, and correspond to those binding patterns
+that use `:!`.
+
+The name being declared, which is the identifier to the left of the `:` or `:!`,
+is called a _binding_, or more specifically a _runtime binding_, _constant
+binding_, _symbolic binding_, or _template binding_. The expression to the right
+defining the type of the binding pattern is called the _binding type
+expression_, a kind of [type expression](#type-expression). For example, in
+`T:! Hashable`, `T` is the binding (a symbolic binding in this case), and
+`Hashable` is the binding type expression.
+
+## Types and `type`
+
+A _type_ is a value of type `type`. Conversely, `type` is the type of all types.
+
+Expressions in type position, for example a [binding type expression](#bindings)
+or the return type of a function, are implicitly cast to type `type`. This means
+that it is legal to put a value that is not a type where a type is expected, as
+long as it has an implicit conversion to `type` that may be performed at compile
+time.
+
+## Facet type
+
+> **TODO:** Documents using the obsolete term "type-of-type" should be updated
+> to say "facet type" instead.
+
+A _facet type_ is a [type](#types-and-type) whose values are some subset of the
+values of `type`, determined by a set of [type constraints](#type-constraints):
+
+-   [Interfaces](#interface) and [named constraints](#named-constraints) are
+    facet types whose constraints are that the interface or named constraint is
+    satisfied by the type.
+-   The values produced by `&` operations between facet types and by `where`
+    expressions are facet types, whose set of constraints are determined by the
+    `&` or `where` expression.
+-   `type` is a facet type whose set of constraints is empty.
+
+A facet type is the type used when declaring some type parameter. It foremost
+determines which types are legal arguments for that type parameter. For template
+parameters, that is all a facet type does. For checked parameters, it also
+determines the API that is available in the body of the definition of the
+[generic function, class, or other entity](#generic-means-compile-time-parameterized).
+
+## Facet
+
+A _facet_ is a value of a [facet type](#facet-type). For example,
+`i32 as Hashable` is a facet, and `Hashable` is a facet type. Note that all
+types are facets, since [`type`](#types-and-type) is considered a facet type.
+Not all facets are types, though: `i32 as Hashable` is of type `Hashable` not
+`type`, so it is a facet that is not a type. However, in places where a type is
+expected, for example in a [binding type expression](#bindings) or after the
+`->` in a function declaration, there is an automatic implicit conversion to
+`type`. This means that a facet may be used in those positions. For example, the
+facet `i32 as Hashable` will implicitly convert to `(i32 as Hashable) as type`,
+which is `i32`, in those contexts.
+
+## Type expression
+
+A _type expression_ is an expression that can be used as a type. In some cases,
+what is written in the source code is a value, like a [facet](#facet) or tuple
+of types, that is not a type but has an implicit conversion to `type`. In those
+cases, we are concerned with the type value after the implicit conversion.
+
+## Facet binding
+
+We use the term _facet binding_ to refer to the name introduced by a
+[constant binding pattern](#bindings) (using `:!` with or without the `template`
+modifier) where the declared type is a [facet type](#facet-type). In the binding
+pattern `T:! Hashable`, `T` is a facet binding, and the value of `T` is a
+[facet](#facet).
+
 ## Deduced parameter
 
 A deduced parameter is listed in the optional `[` `]` section right after the
@@ -275,14 +383,6 @@ function name in a function signature:
 
 Deduced arguments are determined as a result of pattern matching the explicit
 argument values (usually the types of those values) to the explicit parameters.
-Note that function signatures can typically be rewritten to avoid using deduced
-parameters:
-
-```
-fn F[template T:! type](value: T);
-// is equivalent to:
-fn F(value: (template T:! type));
-```
 
 See more [here](overview.md#deduced-parameters).
 
@@ -294,7 +394,8 @@ to know about the interface requirements to call the function, not anything
 about the implementation of the function body, and the compiler can check the
 function body without knowing anything more about the caller. Callers of the
 function provide a value that has an implementation of the API and the body of
-the function may then use that API (and nothing else).
+the function may then use that API. In the case of a checked generic, the
+function may _only_ use that API.
 
 ### Structural interfaces
 
@@ -326,15 +427,20 @@ definition. The criteria for a named constraint, however, are less focused on
 the type's API and instead might include a set of nominal interfaces that the
 type must implement and constraints on the
 [associated entities](#associated-entity) and
-[interface type parameters](#interface-type-parameters-and-associated-types).
+[interface parameters](#interface-parameters-and-associated-constants).
 
 ## Associated entity
 
 An _associated entity_ is a requirement in an interface that a type's
-implementation of the interface must satisfy by having a matching member. A
+implementation of the interface must satisfy by having a matching definition. A
 requirement that the type define a value for a member constant is called an
-_associated constant_, and similarly an _associated function_ or _associated
-type_.
+_associated constant_. If the type of the associated constant is a
+[facet type](#facet-type), then it is called an _associated [facet](#facet)_,
+which corresponds to what is called an "associated type" in other languages
+([Swift](https://docs.swift.org/swift-book/documentation/the-swift-programming-language/generics/#Associated-Types),
+[Rust](https://doc.rust-lang.org/reference/items/associated-items.html#associated-types)).
+Similarly, an interface can have _associated function_, _associated method_, or
+_associated class function_.
 
 Different types can satisfy an interface with different definitions for a given
 member. These definitions are _associated_ with what type is implementing the
@@ -349,27 +455,24 @@ instead of associated entity.
 
 An _impl_ is an implementation of an interface for a specific type, called the
 _implementing type_. It is the place where the function bodies are defined,
-values for associated types, etc. are given. Implementations are needed for
+values for associated constants, etc. are given. Implementations are needed for
 [nominal interfaces](#nominal-interfaces);
 [structural interfaces](#structural-interfaces) and
 [named constraints](#named-constraints) define conformance implicitly instead of
-by requiring an impl to be defined. In can still make sense to implement a named
-constraint as a way to implement all of the interfaces it requires.
+by requiring an impl to be defined. In can still make sense to explicitly
+implement a named constraint as a way to implement all of the interfaces it
+requires.
 
-### Internal impl
+### Extending an impl
 
-A type that implements an interface _internally_ has all the named members of
-the interface as named members of the type. This means that the members of the
-interface are available by way of both
+A type that _extends_ the implementation of an interface has all the named
+members of the interface as named members of the type. This means that the
+members of the interface are available by way of both
 [simple member access and qualified member access expressions](#member-access).
 
-### External impl
-
-In contrast, a type that implements an interface _externally_ does not include
-the named members of the interface in the type. The members of the interface are
-still implemented by the type, though, and so may be accessed using
-[qualified member access expressions](#qualified-member-access-expression) for
-those members.
+If a type implements an interface without extending, the members of the
+interface may only be accessed using
+[qualified member access expressions](#qualified-member-access-expression).
 
 ## Member access
 
@@ -382,12 +485,13 @@ qualified names, which we call a _qualified member access expression_.
 
 Simple member access has the from `object.member`, where `member` is a word
 naming a member of `object`. This form may be used to access members of
-interfaces [implemented internally](#internal-impl) by the type of `object`.
+interfaces when the type of `object`
+[extends the implementation](#extending-an-impl) of that interface.
 
-If `String` implements `Printable` internally, then `s1.Print()` calls the
-`Print` method of `Printable` using simple member access. In this case, the name
-`Print` is used without qualifying it with the name of the interface it is a
-member of since it is recognized as a member of the type itself as well.
+If `String` extends its implementation of `Printable`, then `s1.Print()` calls
+the `Print` method of `Printable` using simple member access. In this case, the
+name `Print` is used without qualifying it with the name of the interface it is
+a member of since it is recognized as a member of the type itself as well.
 
 ### Qualified member access expression
 
@@ -406,8 +510,7 @@ method may be called using the qualified member name by writing the qualified
 member access expression `s1.(Comparable.Less)(s2)`.
 
 This form may be used to access any member of an interface implemented for a
-type, whether it is implemented [internally](#internal-impl) or
-[externally](#external-impl).
+type, whether or not it [extends the implementation](#extending-an-impl).
 
 ## Compatible types
 
@@ -441,11 +544,10 @@ function signatures can change from base class to derived class, see
 [covariance and contravariance in Wikipedia](<https://en.wikipedia.org/wiki/Covariance_and_contravariance_(computer_science)>).
 
 In a generics context, we are specifically interested in the subtyping
-relationships between [type-of-types](#type-of-type). In particular, a
-type-of-type encompasses a set of [type constraints](#type-constraints), and you
-can convert a type from a more-restrictive type-of-type to another type-of-type
-whose constraints are implied by the first. C++ concepts terminology uses the
-term
+relationships between [facet types](#facet-type). In particular, a facet type
+encompasses a set of [type constraints](#type-constraints), and you can convert
+a type from a more-restrictive facet type to another facet type whose
+constraints are implied by the first. C++ concepts terminology uses the term
 ["subsumes"](https://en.cppreference.com/w/cpp/language/constraints#Partial_ordering_of_constraints)
 to talk about this partial ordering of constraints, but we avoid that term since
 it is at odds with the use of the term in
@@ -470,23 +572,26 @@ permitted, always has the same meaning as an explicit cast.
 
 ## Coherence
 
-A generics system has the _implementation coherence_ property, or simply
-_coherence_, if there is a single answer to the question "what is the
+A generics or interface system has the _implementation coherence_ property, or
+simply _coherence_, if there is a single answer to the question "what is the
 implementation of this interface for this type, if any?" independent of context,
 such as the libraries imported into a given file.
 
-This is typically enforced by making sure the definition of the implementation
-must be imported if you import both the interface and the type. This may be done
-by requiring the implementation to be in the same library as the interface or
-type. This is called an _orphan rule_, meaning we don't allow an implementation
-that is not with either of its parents (parent type or parent interface).
-
-Note that in addition to an orphan rule that implementations are visible when
-queried, coherence also requires a rule for resolving what happens if there are
-multiple non-orphan implementations. In Rust, this is called the
-[overlap rule or overlap check](https://rust-lang.github.io/chalk/book/clauses/coherence.html#chalk-overlap-check).
-This could be just producing an error in that situation, or picking one using
-some specialization rule.
+This is enforced using two kinds of rules:
+
+-   An _orphan rule_ is a restriction on which files may declare a particular
+    implementation. This is to ensure that the implementation is imported any
+    time it could be used. For example, if neither the type nor the interface is
+    parameterized, the orphan rule requires that the implementation must be in
+    the same library as the interface or type. The rule is we don't allow an
+    _orphan_ implementation that is not with either of its parents (parent type
+    or parent interface).
+-   An _overlap rule_ is a way to _consistently_ select a single implementation
+    when multiple implementations apply. In Carbon, overlap is resolved by
+    picking a single implementation using a rule that picks the one that is
+    considered most specialized. In Rust, by contrast, the
+    [overlap rule or overlap check](https://rust-lang.github.io/chalk/book/clauses/coherence.html#chalk-overlap-check)
+    instead produces an error if two implementations apply at once.
 
 ## Adapting a type
 
@@ -513,9 +618,9 @@ and as a workaround for
 
 "Type erasure" is where a type's API is replaced by a subset. Everything outside
 of the preserved subset is said to have been "erased". This can happen in a
-variety of contexts including both generics and runtime polymorphism. For
-generics, type erasure restricts a type to just the API required by the
-constraints on a generic function.
+variety of contexts including both checked generics and runtime polymorphism.
+For checked generics, type erasure restricts a type to just the API required by
+the constraints on that type stated in the signature of the function.
 
 An example of type erasure in runtime polymorphism in C++ is casting from a
 pointer of a derived type to a pointer to an abstract base type. Only the API of
@@ -531,13 +636,13 @@ of "type erasure" used in Carbon.
 
 A placeholder type is used when type checking a function in place of a generic
 type parameter. This allows type checking when the specific type to be used is
-not known at type checking time. The type satisfies just its constraint and no
+not known at type-checking time. The type satisfies just its constraint and no
 more, so it acts as the most general type satisfying the interface. In this way
 the archetype is the supertype of all types satisfying the interface.
 
 In addition to satisfying all the requirements of its constraint, the archetype
 also has the member names of its constraint. Effectively it is considered to
-[implement the constraint internally](#internal-impl).
+[extend the implementation of the constraint](#extending-an-impl).
 
 ## Extending an interface
 
@@ -549,18 +654,18 @@ interface.
 ## Witness tables
 
 [Witness tables](https://forums.swift.org/t/where-does-the-term-witness-table-come-from/54334/4)
-are an implementation strategy where values passed to a generic parameter are
-compiled into a table of required functionality. That table is then filled in
-for a given passed-in type with references to the implementation on the original
-type. The generic is implemented using calls into entries in the witness table,
-which turn into calls to the original type. This doesn't necessarily imply a
-runtime indirection: it may be a purely compile-time separation of concerns.
-However, it insists on a full abstraction boundary between the generic user of a
-type and the concrete implementation.
+are an implementation strategy where values passed to a generic type parameter
+are compiled into a table of required functionality. That table is then filled
+in for a given passed-in type with references to the implementation on the
+original type. The generic is implemented using calls into entries in the
+witness table, which turn into calls to the original type. This doesn't
+necessarily imply a runtime indirection: it may be a purely compile-time
+separation of concerns. However, it insists on a full abstraction boundary
+between the generic user of a type and the concrete implementation.
 
 A simple way to imagine a witness table is as a struct of function pointers, one
 per method in the interface. However, in practice, it's more complex because it
-must model things like associated types and interfaces.
+must model things like associated facets and interfaces.
 
 Witness tables are called "dictionary passing" in Haskell. Outside of generics,
 a [vtable](https://en.wikipedia.org/wiki/Virtual_method_table) is a witness
@@ -606,24 +711,25 @@ and other errors may only happen for **some** instantiations.
 
 ### Template specialization
 
-Specialization in C++ is essentially overloading in the context of a template.
-The template is overloaded to have a different definition for some subset of the
+Specialization in C++ is essentially overloading, or
+[ad-hoc polymorphism](#ad-hoc-polymorphism), in the context of a template. The
+template is overloaded to have a different definition for some subset of the
 possible template argument values. For example, the C++ type `std::vector<T>`
 might have a specialization `std::vector<T*>` that is implemented in terms of
 `std::vector<void*>` to reduce code size. In C++, even the interface of a
 templated type can be changed in a specialization, as happens for
 `std::vector<bool>`.
 
-### Generic specialization
+### Checked-generic specialization
 
-Specialization of generics, or types used by generics, is restricted to changing
-the implementation _without_ affecting the interface. This restriction is needed
-to preserve the ability to perform type checking of generic definitions that
-reference a type that can be specialized, without statically knowing which
-specialization will be used.
+Specialization of checked generics, or types used by checked generics, is
+restricted to changing the implementation _without_ affecting the interface.
+This restriction is needed to preserve the ability to perform type checking of
+generic definitions that reference a type that can be specialized, without
+statically knowing which specialization will be used.
 
 While there is nothing fundamentally incompatible about specialization with
-generics, even when implemented using witness tables, the result may be
+checked generics, even when implemented using witness tables, the result may be
 surprising because the selection of the specialized generic happens outside of
 the witness-table-based indirection between the generic code and the concrete
 implementation. Provided all selection relies exclusively on interfaces, this
@@ -636,10 +742,11 @@ that it always supports, but satisfies additional interfaces under some
 conditions on the type argument. For example: `Array(T)` might implement
 `Comparable` if `T` itself implements `Comparable`, using lexicographical order.
 
-## Interface type parameters and associated types
+## Interface parameters and associated constants
 
-_Interface type parameters_ and _associated types_ are both ways of allowing the
-types in function signatures in an interface to vary. For example, different
+_Interface parameters_ and [associated constants](#associated-entity) are both
+ways of allowing the types in function signatures in an interface to vary. For
+example, different
 [stacks](<https://en.wikipedia.org/wiki/Stack_(abstract_data_type)>) will have
 different element types. That element type would be used as the parameter type
 of the `Push` function and the return type of the `Pop` function. As
@@ -647,19 +754,18 @@ of the `Push` function and the return type of the `Pop` function. As
 we can distinguish these by whether they are input parameters or output
 parameters:
 
--   An interface type parameter is a parameter or input to the interface type.
-    That means they must be specified before an implementation of the interface
-    may be determined.
--   In contrast, associated types are outputs. This means that they are
-    determined by the implementation, and need not be specified in a type
-    constraint.
+-   An interface parameter is a parameter or input to the interface. That means
+    they must be specified before an implementation of the interface may be
+    determined.
+-   In contrast, associated constants are outputs. This means that they are
+    determined by the implementation, and need not be specified in a
+    [type constraint](#type-constraints).
 
 Functions using an interface as a constraint need not specify the value of its
-associated types. An associated type is a kind of
-[associated entity](#associated-entity).
+associated constants.
 
 ```
-// Stack using associated types
+// Stack using associated facets
 interface Stack {
   let ElementType:! type;
   fn Push[addr self: Self*](value: ElementType);
@@ -668,7 +774,7 @@ interface Stack {
 
 // Works on any type implementing `Stack`. Return type
 // is determined by the type's implementation of `Stack`.
-fn PeekAtTopOfStack[T: Stack](s: T*) -> T.ElementType {
+fn PeekAtTopOfStack[T:! Stack](s: T*) -> T.ElementType {
   let ret: T.ElementType = s->Pop();
   s->Push(ret);
   return ret;
@@ -682,17 +788,17 @@ class FruitStack {
 }
 ```
 
-Associated types are particularly called for when the implementation of the
-interface determines the type, not the caller. For example, the iterator type
+Associated constants are particularly called for when the implementation of the
+interface determines the value, not the caller. For example, the iterator type
 for a container is specific to the container and not something you would expect
 a user of the interface to specify.
 
-If you have an interface with type parameters, a type can have multiple matching
-impl declarations for different combinations of type parameters. As a result,
-type parameters may not be deduced in a function call. However, if the interface
-parameters are specified, a type can only have a single implementation of the
-given interface. This unique implementation choice determines the values of
-associated types.
+If you have an interface with parameters, a type can have multiple matching
+`impl` declarations for different combinations of argument values. As a result,
+interface parameters may not be deduced in a function call. However, if the
+interface parameters are specified, a type can only have a single implementation
+of the given interface. This unique implementation choice determines the values
+of associated constants.
 
 For example, we might have an interface that says how to perform addition with
 another type:
@@ -726,8 +832,8 @@ fn DoAdd[T:! type, U:! AddWith(T)](x: U, y: T) -> U.ResultType {
 fn CompileError[T:! type, U:! AddWith(T)](x: U) -> T;
 ```
 
-Once the interface parameter can be determined, that determines the values for
-associated types, such as `ResultType` in the example. As always, calls with
+Once the interface parameters can be determined, that determines the values for
+associated constants, such as `ResultType` in the example. As always, calls with
 types for which no implementation exists will be rejected at the call site:
 
 ```
@@ -736,36 +842,32 @@ types for which no implementation exists will be rejected at the call site:
 DoAdd(apple, orange);
 ```
 
+The type of an interface parameters and associated constants is commonly a
+[facet type](#facet-type), but not always. For example, an interface parameter
+that specifies an array bound might have an integer type.
+
 ## Type constraints
 
-Type constraints restrict which types are legal for template or generic
-parameters or associated types. They help define semantics under which they
-should be called, and prevent incorrect calls.
+Type constraints restrict which types are legal for generic parameters or
+associated facets. They help define semantics under which they should be called,
+and prevent incorrect calls.
 
 In general there are a number of different type relationships we would like to
 express, for example:
 
 -   This function accepts two containers. The container types may be different,
     but the element types need to match.
--   For this container interface we have associated types for iterators and
+-   For this container interface we have associated facets for iterators and
     elements. The iterator type's element type needs to match the container's
     element type.
--   An interface may define an associated type that needs to be constrained to
+-   An interface may define an associated facet that needs to be constrained to
     implement some interfaces.
 -   This type must be [compatible](#compatible-types) with another type. You
     might use this to define alternate implementations of a single interfaces,
     such as sorting order, for a single type.
 
-Note that type constraints can be a restriction on one type parameter or
-associated type, or can define a relationship between multiple types.
-
-## Type-of-type
-
-A type-of-type is the type used when declaring some type parameter. It foremost
-determines which types are legal arguments for that type parameter, also known
-as [type constraints](#type-constraints). For template parameters, that is all a
-type-of-type does. For generic parameters, it also determines the API that is
-available in the body of the function.
+Note that type constraints can be a restriction on one facet parameter or
+associated facet, or can define a relationship between multiple facets.
 
 ## References
 
@@ -773,3 +875,6 @@ available in the body of the function.
 -   [#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)
+-   [#2138: Checked and template generic terminology](https://github.com/carbon-language/carbon-lang/pull/2138)
+-   [#2360: Types are values of type `type`](https://github.com/carbon-language/carbon-lang/pull/2360)
+-   [#2760: Consistent `class` and `interface` syntax](https://github.com/carbon-language/carbon-lang/pull/2760)

docs/project/faq.md

@@ -461,7 +461,7 @@ migration of C++ code.
 References:
 
 -   [Generics: Goals: Better compiler experience](/docs/design/generics/goals.md#better-compiler-experience)
--   [Generics: Terminology: Generic versus template parameters](/docs/design/generics/terminology.md#generic-versus-template-parameters)
+-   [Generics: Terminology: Generic versus template parameters](/docs/design/generics/terminology.md#checked-versus-template-parameters)
 
 ### What is Carbon's memory model?
 

proposals/p0990.md

@@ -102,10 +102,9 @@ default implementations of interfaces they require:
 -   It would be unclear how to resolve the ambiguity of which default to use
     when two different interfaces provide different defaults for a common
     interface requirement.
--   It would be ambiguous whether the required interface should be
-    [external](/docs/design/generics/terminology.md#external-impl) or
-    [internal](/docs/design/generics/terminology.md#internal-impl) unless
-    `PartialOrder` is implemented explicitly.
+-   It would be ambiguous whether the required interface should be external or
+    [internal](/docs/design/generics/terminology.md#extending-an-interface)
+    unless `PartialOrder` is implemented explicitly.
 -   There would be a lot of overlap between default impls and blanket impls.
     Eliminating default impls keeps the language smaller and simpler.
 

proposals/p1146.md

@@ -30,7 +30,7 @@ types, but there are a few things specific to types. In particular:
     implied constraints.
 
 We also want a
-[generic specialization](/docs/design/generics/terminology.md#generic-specialization)
+[generic specialization](/docs/design/generics/terminology.md#checked-generic-specialization)
 story that works well for types, without giving up the ability to type check
 users of a type without knowing which specializations apply.