diff --git a/docs/design/generics/README.md b/docs/design/generics/README.md
index 878f7ab78f9aa..a927a57926158 100644
--- a/docs/design/generics/README.md
+++ b/docs/design/generics/README.md
@@ -12,6 +12,7 @@ feature of Carbon:
- ~~Overview~~ - not implemented yet
- [Goals](goals.md) - The motivation and principles guiding the design
direction.
-- ~~Terminology~~ - not implemented yet
+- [Terminology](terminology.md) - A glossary establishing common terminology
+ for describing the design.
- ~~Detailed design~~ - not implemented yet
- ~~Rejected alternatives~~ - not implemented yet
diff --git a/docs/design/generics/goals.md b/docs/design/generics/goals.md
index 6c17e998741f5..09150a0226124 100644
--- a/docs/design/generics/goals.md
+++ b/docs/design/generics/goals.md
@@ -12,7 +12,6 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
- [Purpose of this document](#purpose-of-this-document)
- [Background](#background)
- - [Definition of generics](#definition-of-generics)
- [Generic parameters](#generic-parameters)
- [Interfaces](#interfaces)
- [Relationship to templates](#relationship-to-templates)
@@ -52,36 +51,25 @@ forward-looking.
## Background
-### Definition of generics
+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
+[complete definition checking](terminology.md#complete-definition-checking).
-**TODO** This should be replaced with a link to a terminology doc, once that is
-accepted.
-
-C++ supports
-[parametric polymorphism](https://en.wikipedia.org/wiki/Parametric_polymorphism)
-and [generic programming](https://en.wikipedia.org/wiki/Generic_programming)
-through templates. Templates use
+This is in contrast with the
[compile-time duck typing](https://en.wikipedia.org/wiki/Duck_typing#Templates_or_generic_types)
-to decide whether arguments are valid. This is a form of
-[structural typing](https://en.wikipedia.org/wiki/Structural_type_system) that
-is usage based.
-
-Carbon will support _generics_ in order to allow definition checking in generic
-programming. Definition checking is accomplished by using
-[bounded parametric polymorphism](https://en.wikipedia.org/wiki/Parametric_polymorphism#Bounded_parametric_polymorphism)
-instead of compile-time duck typing. This means the legal arguments and the
-legal uses of a parameter are both goverened by explicit bounds on the parameter
-in a generic function's signature.
-
-This would be _in addition_ to
+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.
### Generic parameters
Generic functions and generic types will all take some "generic parameters",
-which will frequently be types, and in some cases will be implicit or inferred
-from the types of the values of explicit parameters.
+which will frequently be types, and in some cases will be
+[implicit or inferred](terminology.md#implicit-parameter) from the types of the
+values of explicit parameters.
If a generic parameter is a type, the generic function's signature can specify
constraints that the caller's type must satisfy. For example, a resizable array
@@ -97,13 +85,13 @@ the same type.
We need some way to express the constraints on a generic type parameter. In
Carbon we express these "type constraints" by saying we restrict to types that
-implement specific _interfaces_. Interfaces describe an API a type could
-implement; for example, it might specify a set of functions, including names and
-signatures. A type implementing an interface may be passed as a generic type
-argument to a function that has that interface as a requirement of its generic
-type parameter. Then, the functions defined in the interface may be called in
-the body of the function. Further, interfaces have names that allow them to be
-reused.
+implement specific [_interfaces_](terminology.md#interface). Interfaces describe
+an API a type could implement; for example, it might specify a set of functions,
+including names and signatures. A type implementing an interface may be passed
+as a generic type argument to a function that has that interface as a
+requirement of its generic type parameter. Then, the functions defined in the
+interface may be called in the body of the function. Further, interfaces have
+names that allow them to be reused.
Similar compile-time and run-time constructs may be found in other programming
languages:
diff --git a/docs/design/generics/terminology.md b/docs/design/generics/terminology.md
new file mode 100644
index 0000000000000..5794925a7cd1f
--- /dev/null
+++ b/docs/design/generics/terminology.md
@@ -0,0 +1,613 @@
+# Carbon: Generics - Terminology
+
+
+
+
+
+## Table of contents
+
+- [Parameterized language constructs](#parameterized-language-constructs)
+- [Generic versus template parameters](#generic-versus-template-parameters)
+ - [Polymorphism](#polymorphism)
+ - [Parametric polymorphism](#parametric-polymorphism)
+ - [Compile-time duck typing](#compile-time-duck-typing)
+ - [Ad-hoc polymorphism](#ad-hoc-polymorphism)
+ - [Constrained genericity](#constrained-genericity)
+ - [Definition checking](#definition-checking)
+ - [Complete definition checking](#complete-definition-checking)
+ - [Early versus late type checking](#early-versus-late-type-checking)
+- [Implicit parameter](#implicit-parameter)
+- [Interface](#interface)
+ - [Structural interfaces](#structural-interfaces)
+ - [Nominal interfaces](#nominal-interfaces)
+- [Impls: Implementations of interfaces](#impls-implementations-of-interfaces)
+- [Compatible types](#compatible-types)
+- [Subtyping and casting](#subtyping-and-casting)
+- [Adapting a type](#adapting-a-type)
+- [Type erasure](#type-erasure)
+- [Facet type](#facet-type)
+- [Extending/refining an interface](#extendingrefining-an-interface)
+- [Witness tables](#witness-tables)
+ - [Dynamic-dispatch witness table](#dynamic-dispatch-witness-table)
+ - [Static-dispatch witness table](#static-dispatch-witness-table)
+- [Instantiation](#instantiation)
+- [Specialization](#specialization)
+ - [Template specialization](#template-specialization)
+ - [Generic specialization](#generic-specialization)
+- [Conditional conformance](#conditional-conformance)
+- [Interface type parameters versus associated types](#interface-type-parameters-versus-associated-types)
+- [Type constraints](#type-constraints)
+- [Type-type](#type-type)
+
+
+
+## Parameterized language constructs
+
+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-versus-associated-types).
+
+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
+
+When we are distinguishing between generics and templates in Carbon, it is on an
+parameter by parameter basis. A single function can take a mix of regular,
+generic, and template parameters.
+
+- **Regular parameters**, or "dynamic parameters", are designated using the
+ "<type>`:` <name>" syntax (or "<value>").
+- **Generic parameters** are temporarily designated using a `$` between the
+ type and the name (so it is "<type>`$` <name>"). However, the `$`
+ symbol is not easily typed on non-US keyboards, so we intend to switch to
+ some other syntax. Some possibilities that have been suggested are: `!`,
+ `@`, `#`, and `:`.
+- **Template parameters** are temporarily designated using "<type> `$$`
+ <name>", for similar reasons.
+
+Expected difference between generics and templates:
+
+
+
+ Generics
+ |
+ Templates
+ |
+
+
+ bounded parametric polymorphism
+ |
+ compile-time duck typing and ad-hoc polymorphism
+ |
+
+
+ constrained genericity
+ |
+ optional constraints
+ |
+
+
+ name lookup resolved for definitions in isolation ("early")
+ |
+ some name lookup may require information from calls (name lookup may be "late")
+ |
+
+
+ sound to typecheck definitions in isolation ("early")
+ |
+ complete type checking may require information from calls (may be "late")
+ |
+
+
+ supports separate type checking; may also support separate compilation, for example when implemented using dynamic witness tables
+ |
+ separate compilation only to the extent that C++ supports it
+ |
+
+
+ allowed but not required to be implemented using dynamic dispatch
+ |
+ does not support implementation by way of dynamic dispatch, just static by way of instantiation
+ |
+
+
+ monomorphization is an optional optimization that cannot render the program invalid
+ |
+ monomorphization is mandatory and can fail, resulting in the program being invalid
+ |
+
+
+
+### Polymorphism
+
+Generics and templates provide different forms of
+[polymorphism]()
+than object-oriented programming with inheritance. That uses
+[subtype polymorphism](https://en.wikipedia.org/wiki/Subtyping) where different
+descendants, or "subtypes", of a base class can provide different
+implementations of a method, subject to some compatibility restrictions on the
+signature.
+
+#### Parametric polymorphism
+
+Parametric polymorphism
+([Wikipedia](https://en.wikipedia.org/wiki/Parametric_polymorphism)) is when a
+function or a data type can be written generically so that it can handle values
+_identically_ without depending on their type.
+[Bounded parametric polymorphism](https://en.wikipedia.org/wiki/Parametric_polymorphism#Bounded_parametric_polymorphism)
+is where the allowed types are restricted to satisfy some constraints. Within
+the set of allowed types, different types are treated uniformly.
+
+#### Compile-time duck typing
+
+Duck typing ([Wikipedia](https://en.wikipedia.org/wiki/Duck_typing)) is when the
+legal types for arguments are determined implicitly by the usage of the values
+of those types in the body of the function. Compile-time duck typing is when the
+usages in the body of the function are checked at compile-time, along all code
+paths. Contrast this with ordinary duck typing in a dynamic language such as
+Python where type errors are only diagnosed at runtime when a usage is reached
+dynamically.
+
+#### Ad-hoc polymorphism
+
+Ad-hoc polymorphism
+([Wikipedia](https://en.wikipedia.org/wiki/Ad_hoc_polymorphism)), also known as
+"overloading", is when a single function name has multiple implementations for
+handling different argument types. There is no enforcement of any consistency
+between the implementations. For example, the return type of each overload can
+be arbitrary, rather than being the result of some consistent rule being applied
+to the argument types.
+
+Templates work with ad-hoc polymorphism in two ways:
+
+- A function with template parameters can be
+ [specialized](#template-specialization) in
+ [C++](https://en.cppreference.com/w/cpp/language/template_specialization) as
+ a form of ad-hoc polymorphism.
+- A function with template parameters can call overloaded functions since it
+ 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:
+
+```
+fn F[Type$$ T](Ptr(T) x) -> T;
+fn F(Int x) -> Bool;
+```
+
+A generic function `G` can call `F` with a type like `Ptr(T)` that can not
+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. (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 `F`. This still poses problems for the dynamic strategy for
+compiling generics.)
+
+### Constrained genericity
+
+We will allow some way of specifying constraints as part of a function (or type
+or other parameterized language construct). These constraints are a limit on
+what callers are allowed to pass in. The distinction between constrained and
+unconstrained genericity is whether the body of the function is limited to just
+those operations that are guaranteed by the constraints.
+
+With templates using unconstrained genericity, you may perform any operation in
+the body of the function, and they will be checked against the specific types
+used in calls. You can still have constraints, but they are optional. They will
+only be used 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.
+
+### 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 dependent on any
+template parameter in the definition. Adding constraints to template parameters
+and/or switching them to be generic allows the compiler to increase how much of
+the definition can be checked. Any remaining checks are delayed until
+[instantiation](#instantiation), which can fail.
+
+#### Complete definition checking
+
+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
+[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.
+
+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 values.
+
+## Implicit parameter
+
+An implicit parameter is listed in the optional `[` `]` section right after the
+function name in a function signature:
+
+`fn` <name> `[` <implicit parameters> `](` <explicit parameters `) ->`
+<return type>
+
+Implicit 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 implicit
+parameters:
+
+```
+fn F[Type$$ T](T value);
+// is equivalent to:
+fn F((Type$$ T) value);
+```
+
+See more [here](overview.md#implicit-parameters).
+
+## Interface
+
+An interface is an API constraint used in a function signature to provide
+encapsulation. Encapsulation here means that callers of the function only need
+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).
+
+### Structural interfaces
+
+A "structural" interface is one where we say a type satisfies the interface as
+long as it has members with a specific list of names, and for each name it must
+have some type or signature. A type can satisfy a structural interface without
+ever naming that interface, just by virtue of having members with the right
+form.
+
+### Nominal interfaces
+
+A "nominal" interface is one where we say a type can only satisfy an interface
+if there is some explicit statement saying so, for example by defining an
+[impl](#impls-implementations-of-interfaces). This allows "satisfies the
+interface" to have additional semantic meaning beyond what is directly checkable
+by the compiler. For example, knowing whether the "Draw" function means "render
+an image to the screen" or "take a card from the top of a deck of cards"; or
+that a `+` operator is commutative (and not, say, string concatenation).
+
+We use the "structural" versus "nominal" terminology as a generalization of the
+same terms being used in a
+[subtyping context](https://en.wikipedia.org/wiki/Subtyping#Subtyping_schemes).
+
+## Impls: Implementations of interfaces
+
+An _impl_ is an implementation of an interface for a specific type. It is the
+place where the function bodies are defined, values for associated types, etc.
+are given. A given generics programming model may support default impls, named
+impls, or both. Impls are mostly associated with nominal interfaces; structural
+interfaces define conformance implicitly instead of by requiring an impl to be
+defined.
+
+## Compatible types
+
+Two types are compatible if they have the same notional set of values and
+represent those values in the same way, even if they expose different APIs. The
+representation of a type describes how the values of that type are represented
+as a sequence of bits in memory. The set of values of a type includes properties
+that the compiler can't directly see, such as invariants that the type
+maintains.
+
+We can't just say two types are compatible based on structural reasons. Instead,
+we have specific constructs that create compatible types from existing types in
+ways that encourage preserving the programmer's intended semantics and
+invariants, such as implementing the API of the new type by calling (public)
+methods of the original API, instead of accessing any private implementation
+details.
+
+## Subtyping and casting
+
+Both subtyping and casting are different names for changing the type of a value
+to a compatible type.
+
+[Subtyping](https://en.wikipedia.org/wiki/Subtyping) is a relationship between
+two types where you can safely operate on a value of one type using a variable
+of another. For example, using C++'s object-oriented features, you can operate
+on a value of a derived class using a pointer to the base class. In most cases,
+you can pass a more specific type to a function that can handle a more general
+type. Return types work the opposite way, a function can return a more specific
+type to a caller prepared to handle a more general type. This determines how
+function signatures can change from base class to derived class, see
+[covariance and contravariance in Wikipedia]().
+
+In a generics context, we are specifically interested in the subtyping
+relationships between [type-types](#type-type). In particular, a type-type
+encompasses a set of [type constraints](#type-constraints), and you can convert
+a type from a more-restrictive type-type to another type-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
+[object-oriented subtyping terminology](https://en.wikipedia.org/wiki/Subtyping#Subsumption).
+
+Note that subtyping is a bit like
+[coercion](https://en.wikipedia.org/wiki/Type_conversion), except we want to
+make it clear that the data representation of the value is not changing, just
+its type as reflected in the API available to manipulate the value.
+
+Casting is indicated explicitly by way of some syntax in the source code. You
+might use a cast to switch between [type adaptations](#adapting-a-type), or to
+be explicit where an implicit cast would otherwise occur. For now, we are saying
+"`x as y`" is the provisional syntax in Carbon for casting the value `x` to the
+type `y`. Note that outside of generics, the term "casting" includes any
+explicit type change, including those that change the data representation.
+
+## Adapting a type
+
+A type can be adapted by creating a new type that is
+[compatible](#compatible-types) with an existing type, but has a different API.
+In particular, the new type might implement different interfaces or provide
+different implementations of the same interfaces.
+
+Unlike extending a type (as with C++ class inheritance), you are not allowed to
+add new data fields onto the end of the representation -- you may only change
+the API. This means that it is safe to [cast](#subtyping-and-casting) a value
+between those two types without any dynamic checks or danger of
+[object slicing](https://en.wikipedia.org/wiki/Object_slicing).
+
+This is called "newtype" in Rust, and is used for capturing additional
+information in types to improve type safety of move some checking to compile
+time ([1](https://doc.rust-lang.org/rust-by-example/generics/new_types.html),
+[2](https://doc.rust-lang.org/book/ch19-04-advanced-types.html#using-the-newtype-pattern-for-type-safety-and-abstraction),
+[3](https://www.worthe-it.co.za/blog/2020-10-31-newtype-pattern-in-rust.html))
+and as a workaround for Rust's orphan rules for coherence.
+
+## Type erasure
+
+"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.
+
+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
+the base type is available on the result, even though the implementation of
+those methods still come from the derived type.
+
+The term "type erasure" can also refer to
+[the specific strategy used by Java to implement generics](https://en.wikipedia.org/wiki/Generics_in_Java).
+which includes erasing the identity of type parameters. This is not the meaning
+of "type erasure" used in Carbon.
+
+## Facet type
+
+A facet type is a [compatible type](#compatible-types) of some original type
+written by the user, that has a specific API. This API might correspond to a
+specific [interface](#interface), or the API required by particular
+[type constraints](#type-constraints). In either case, the API can be specified
+using a [type-type](#type-type). Casting a type to a type-type results in a
+facet type, with data representation matching the original type and API matching
+the type-type.
+
+Casting to a facet type is one way of modeling compile-time
+[type erasure](#type-erasure) when calling a generic function. It is also a way
+of accessing APIs for a type that would otherwise be hidden, possibly to avoid a
+name conflict or because the implementation of that API was external to the
+definition of the type.
+
+A facet type associated with a specific interface, corresponds to the
+[impl](#impls-implementations-of-interfaces) of that interface for the type.
+Using such a facet type removes ambiguity about where to find the declaration
+and definition of any accessed methods.
+
+## Extending/refining an interface
+
+An interface can be extended by defining an interface that includes the full API
+of another interface, plus some additional API. Types implementing the extended
+interface should automatically be considered to have implemented the narrower
+interface.
+
+## Witness tables
+
+For witness tables, 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.
+
+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.
+
+Witness tables are called "dictionary passing" in Haskell. Outside of generics,
+a [vtable](https://en.wikipedia.org/wiki/Virtual_method_table) is a witness
+table that witnesses that a class is a descendant of an abstract base class, and
+is passed as part of the object instead of separately.
+
+### Dynamic-dispatch witness table
+
+For dynamic-dispatch witness tables, actual function pointers are formed and
+used as a dynamic, runtime indirection. As a result, the generic code **will
+not** be duplicated for different witness tables.
+
+### Static-dispatch witness table
+
+For static-dispatch witness tables, the implementation is required to collapse
+the table indirections at compile time. As a result, the generic code **will**
+be duplicated for different witness tables.
+
+Static-dispatch may be implemented as a performance optimization for
+dynamic-dispatch that increases generated code size. The final compiled output
+may not retain the witness table.
+
+## Instantiation
+
+Instantiation is the implementation strategy for templates in both C++ and
+Carbon. Instantiation explicitly creates a copy of the template code and
+replaces the template components with the concrete type and its implementation
+operations. It allows duck typing and lazy binding. Instantiation implies
+template code **will** be duplicated.
+
+Unlike [static-dispatch witness tables](#static-dispatch-witness-table) and
+[monomorphization (as in Rust)](https://doc.rust-lang.org/book/ch10-01-syntax.html#performance-of-code-using-generics),
+this is done **before** type checking completes. Only when the template is used
+with a concrete type is the template fully type checked, and it type checks
+against the actual concrete type after substituting it into the template. This
+means that different instantiations may interpret the same construct in
+different ways, and that templates can include constructs that are not valid for
+some possible instantiations. However, it also means that some errors in the
+template implementation may not produce errors until the instantiation occurs,
+and other errors may only happen for **some** instantiations.
+
+## Specialization
+
+### 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
+possible template argument values. For example, the C++ type `std::vector`
+might have a specialization `std::vector` that is implemented in terms of
+`std::vector` to reduce code size. In C++, even the interface of a
+templated type can be changed in a specialization, as happens for
+`std::vector`.
+
+### 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.
+
+While there is nothing fundamentally incompatible about specialization with
+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
+still satisfies the fundamental constraints of generics.
+
+## Conditional conformance
+
+Conditional conformance is when you have a parameterized type that has one API
+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 versus associated types
+
+Let's say you have an interface defining a container. Different containers will
+contain different types of values, and the container API will have to refer to
+that "element type" when defining the signature of methods like "insert" or
+"find". If that element type is a parameter (input) to the interface type, we
+say it is a type parameter; if it is an output, we say it is an associated type.
+
+Type parameter example:
+
+```
+interface Stack(Type$ ElementType) {
+ fn Push(Self* this, ElementType value);
+ fn Pop(Self* this) -> ElementType;
+}
+```
+
+Associated type example:
+
+```
+interface Stack {
+ var Type$ ElementType;
+ fn Push(Self* this, ElementType value);
+ fn Pop(Self* this) -> ElementType;
+}
+```
+
+Associated types are particularly called for when the implementation controls
+the type, 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.
+
+```
+interface Iterator { ... }
+interface Container {
+ // This does not make sense as an parameter to the container interface,
+ // since this type is determined from the container type.
+ var Iterator$ IteratorType;
+ ...
+ fn Insert(Self* this, IteratorType position, ElementType value);
+}
+struct ListIterator(Type$ ElementType) {
+ ...
+ impl Iterator;
+}
+struct List(Type$ ElementType) {
+ // Iterator type is determined by the container type.
+ var Iterator$ IteratorType = ListIterator(ElementType);
+ fn Insert(Self* this, IteratorType position, ElementType value) {
+ ...
+ }
+ impl Container;
+}
+```
+
+Since type parameters are directly under the user's control, it is easier to
+express things like "this type parameter is the same for all these interfaces",
+and other type constraints.
+
+If you have an interface with type parameters, there is a question of whether a
+type can have multiple impls for different combinations of type parameters, or
+if you can only have a single impl (in which case you can directly infer the
+type parameters given just a type implementing the interface). You can always
+infer associated types.
+
+## 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.
+
+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
+ 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
+ implement some interfaces.
+- This type parameter 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 can
+define a relationship between multiple type parameters.
+
+## Type-type
+
+A type-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-type does. For generic parameters, it also determines the API that is
+available in the body of the function. Calling a function with a type `T` passed
+to a generic type parameter `U` with type-type `I`, ends up setting `U` to the
+facet type `T as I`. This has the API determined by `I`, with the implementation
+of that API coming from `T`.
diff --git a/proposals/README.md b/proposals/README.md
index c873aea084489..f55b1238f335b 100644
--- a/proposals/README.md
+++ b/proposals/README.md
@@ -51,5 +51,6 @@ request:
- [0415 - Syntax: `return`](p0415.md)
- [0426 - Governance & evolution revamp](p0426.md)
- [0444 - GitHub Discussions](p0444.md)
+- [0447 - Generics terminology](p0447.md)
diff --git a/proposals/p0447.md b/proposals/p0447.md
new file mode 100644
index 0000000000000..f8f9f7716d1c5
--- /dev/null
+++ b/proposals/p0447.md
@@ -0,0 +1,36 @@
+# Generics terminology
+
+
+
+[Pull request](https://github.com/carbon-language/carbon-lang/pull/447)
+
+## Problem
+
+To talk about generics as a programming language feature, you need a lot of
+specialized terminology. We need to agree on the words we are using and their
+meaning before we can meaningfully talk about the design of the feature itself.
+
+There a number of problems a glossary solves:
+
+- Not everyone knows every term, so having a single place to look them up will
+ improve the ease of understanding, ease of contributing, and accessibility
+ of the project.
+- There may not be widespread agreement on the meaning of some terms. In
+ particular, individual programming languages tend to assign very specific
+ meanings to terms used within their ecosystem.
+- Some terms may be used in multiple ways, but we only use the term with one
+ specific meaning.
+- Some terms are our invention and we need to introduce them.
+
+## Proposal
+
+See the [generics terminology document](../docs/design/generics/terminology.md).
+
+## Rationale
+
+This gives a common vocabulary for discussing the design of the generics
+feature.