From 9aac6ff2a461d2150d48e1afc53b3d8bc04fc80c Mon Sep 17 00:00:00 2001 From: Josh L Date: Fri, 22 Sep 2023 21:12:42 +0000 Subject: [PATCH 01/19] Update generics details including #2495, #2687, and others --- docs/design/generics/details.md | 3634 ++++++++++++++++++++----------- 1 file changed, 2352 insertions(+), 1282 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 3a738703341f8..74f86e71e852f 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -49,39 +49,46 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception - [Parameterized interfaces](#parameterized-interfaces) - [Parameterized named constraints](#parameterized-named-constraints) - [Where constraints](#where-constraints) - - [Constraint use cases](#constraint-use-cases) - - [Set an associated constant to a specific value](#set-an-associated-constant-to-a-specific-value) - - [Same type constraints](#same-type-constraints) - - [Set an associated type to a specific value](#set-an-associated-type-to-a-specific-value) - - [Equal generic types](#equal-generic-types) - - [Satisfying both type-of-types](#satisfying-both-type-of-types) - - [Type bound for associated type](#type-bound-for-associated-type) - - [Type bounds on associated types in declarations](#type-bounds-on-associated-types-in-declarations) - - [Type bounds on associated types in interfaces](#type-bounds-on-associated-types-in-interfaces) - - [Combining constraints](#combining-constraints) + - [Kinds of `where` constraints](#kinds-of-where-constraints) - [Recursive constraints](#recursive-constraints) + - [Rewrite constraints](#rewrite-constraints) + - [Combining constraints with `&`](#combining-constraints-with-) + - [Combining constraints with `and`](#combining-constraints-with-and) + - [Combining constraints with `extends`](#combining-constraints-with-extends) + - [Combining constraints with `impl as` and `impls`](#combining-constraints-with-impl-as-and-impls) + - [Rewrite constraint resolution](#rewrite-constraint-resolution) + - [Precise rules and termination](#precise-rules-and-termination) + - [Qualified name lookup](#qualified-name-lookup) + - [Type substitution](#type-substitution) + - [Examples](#examples) + - [Termination](#termination) + - [Same-type constraints](#same-type-constraints) + - [Implementation of same-type `ImplicitAs`](#implementation-of-same-type-implicitas) + - [Manual type equality](#manual-type-equality) + - [Observe declarations](#observe-declarations) + - [Implements constraints](#implements-constraints) + - [Implied constraints](#implied-constraints) + - [Combining constraints](#combining-constraints) + - [Satisfying both facet types](#satisfying-both-facet-types) + - [Constraints must use a designator](#constraints-must-use-a-designator) + - [Referencing names in the interface being defined](#referencing-names-in-the-interface-being-defined) + - [Constraint examples and use cases](#constraint-examples-and-use-cases) - [Parameterized type implements interface](#parameterized-type-implements-interface) - [Another type implements parameterized interface](#another-type-implements-parameterized-interface) - - [Constraints must use a designator](#constraints-must-use-a-designator) - - [Implied constraints](#implied-constraints) - [Must be legal type argument constraints](#must-be-legal-type-argument-constraints) - - [Referencing names in the interface being defined](#referencing-names-in-the-interface-being-defined) - - [Manual type equality](#manual-type-equality) - - [`observe` declarations](#observe-declarations) -- [Other constraints as type-of-types](#other-constraints-as-type-of-types) + - [Named constraint constants](#named-constraint-constants) +- [Other constraints as facet types](#other-constraints-as-facet-types) - [Is a derived class](#is-a-derived-class) - [Type compatible with another type](#type-compatible-with-another-type) - [Same implementation restriction](#same-implementation-restriction) - [Example: Multiple implementations of the same interface](#example-multiple-implementations-of-the-same-interface) - [Example: Creating an impl out of other implementations](#example-creating-an-impl-out-of-other-implementations) - - [Sized types and type-of-types](#sized-types-and-type-of-types) - - [`TypeId`](#typeid) + - [Sized types and facet types](#sized-types-and-facet-types) - [Destructor constraints](#destructor-constraints) -- [Generic `let`](#generic-let) +- [Compile-time `let`](#compile-time-let) - [Parameterized impl declarations](#parameterized-impl-declarations) - [Impl for a parameterized type](#impl-for-a-parameterized-type) - [Conditional conformance](#conditional-conformance) - - [Conditional methods](#conditional-methods) - [Blanket impl declarations](#blanket-impl-declarations) - [Difference between a blanket impl and a named constraint](#difference-between-a-blanket-impl-and-a-named-constraint) - [Wildcard impl declarations](#wildcard-impl-declarations) @@ -93,6 +100,7 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception - [Prioritization rule](#prioritization-rule) - [Acyclic rule](#acyclic-rule) - [Termination rule](#termination-rule) + - [Non-facet arguments](#non-facet-arguments) - [`final` impl declarations](#final-impl-declarations) - [Libraries that can contain a `final` impl](#libraries-that-can-contain-a-final-impl) - [Comparison to Rust](#comparison-to-rust) @@ -111,10 +119,13 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception - [Observing a type implements an interface](#observing-a-type-implements-an-interface) - [Observing interface requirements](#observing-interface-requirements) - [Observing blanket impl declarations](#observing-blanket-impl-declarations) + - [Observing equal to a type implementing an interface](#observing-equal-to-a-type-implementing-an-interface) - [Operator overloading](#operator-overloading) - [Binary operators](#binary-operators) - [`like` operator for implicit conversions](#like-operator-for-implicit-conversions) - [Parameterized types](#parameterized-types) + - [Generic methods](#generic-methods) + - [Conditional methods](#conditional-methods) - [Specialization](#specialization) - [Future work](#future-work) - [Dynamic types](#dynamic-types) @@ -130,7 +141,7 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception - [Field requirements](#field-requirements) - [Bridge for C++ customization points](#bridge-for-c-customization-points) - [Variadic arguments](#variadic-arguments) - - [Range constraints on symbolic integers](#range-constraints-on-symbolic-integers) + - [Value constraints for template parameters](#value-constraints-for-template-parameters) - [References](#references) @@ -229,7 +240,7 @@ An [interface](terminology.md#interface), defines an API that a given type can implement. For example, an interface capturing a linear-algebra vector API might have two methods: -``` +```carbon interface Vector { // Here the `Self` keyword means // "the type implementing this interface". @@ -266,7 +277,7 @@ what is associated with the implementing type for that interface. An impl may be defined inline inside the type definition: -``` +```carbon class Point_Inline { var x: f64; var y: f64; @@ -288,7 +299,7 @@ class Point_Inline { Interfaces that are implemented inline with the `extend` keyword contribute to the type's API: -``` +```carbon class Point_Extend { var x: f64; var y: f64; @@ -311,7 +322,7 @@ Assert(p1.Add(p1) == p2); Without `extend`, those methods may only be accessed with [qualified member names and compound member access](#qualified-member-names-and-compound-member-access): -``` +```carbon // Point_Inline did not use `extend` when // implementing `Vector`: var a: Point_Inline = {.x = 1.0, .y = 2.0}; @@ -340,7 +351,7 @@ This syntax was changed to use `extend` in An impl may also be defined after the type definition, by naming the type between `impl` and `as`: -``` +```carbon class Point_OutOfLine { var x: f64; var y: f64; @@ -425,7 +436,7 @@ done using [`extend` to add to the type's API](#extend-impl), only the declaration in the class definition will use the `extend` keyword, as in this example: -``` +```carbon class Point_ExtendForward { var x: f64; var y: f64; @@ -454,7 +465,7 @@ More about forward declaring implementations in To implement more than one interface when defining a type, simply include an `impl` block or forward declaration per interface. -``` +```carbon class Point_2Extend { var x: f64; var y: f64; @@ -481,7 +492,7 @@ names to be given the same implementation? It seems like that might be a common case, but we won't really know if this is an important case until we get more experience. -``` +```carbon class Player { var name: String; extend impl as Icon { @@ -503,7 +514,7 @@ class Player { To avoid name collisions, you can't extend implementations of two interfaces that have a name in common: -``` +```carbon class GameBoard { extend impl as Drawable { fn Draw[self: Self]() { ... } @@ -524,7 +535,7 @@ cluttering the API of that type or to avoid a name collision with another member of that type. A syntax for reusing method implementations allows us to include names from an implementation selectively: -``` +```carbon class Point_ReuseMethodInImpl { var x: f64; var y: f64; @@ -585,7 +596,7 @@ impl Point_ReuseByOutOfLine as Vector { ### Qualified member names and compound member access -``` +```carbon class Point_NoExtend { var x: f64; var y: f64; @@ -602,7 +613,7 @@ whether or not the implementation is done with an expression writes the member's _qualified name_ in the parentheses of the [compound member access syntax](/docs/design/expressions/member_access.md): -``` +```carbon var p1: Point_NoExtend = {.x = 1.0, .y = 2.0}; var p2: Point_NoExtend = {.x = 2.0, .y = 4.0}; Assert(p1.(Vector.Scale)(2.0) == p2); @@ -614,7 +625,7 @@ the names of members of `Point_NoExtend`. So if there was another interface `Drawable` with method `Draw` defined in the `Plot` package also implemented for `Point_NoExtend`, as in: -``` +```carbon package Plot; import Points; @@ -627,7 +638,7 @@ impl Points.Point_NoExtend as Drawable { ... } You could access `Draw` with a qualified name: -``` +```carbon import Plot; import Points; @@ -662,7 +673,7 @@ declaration of the `impl`. Here is a function that can accept values of any type that has implemented the `Vector` interface: -``` +```carbon fn AddAndScaleGeneric[T:! Vector](a: T, b: T, s: f64) -> T { return a.Add(b).Scale(s); } @@ -704,7 +715,7 @@ to adding a `Vector` [qualification](#qualified-member-names-and-compound-member-access) to replace all simple member accesses of `T`: -``` +```carbon fn AddAndScaleGeneric[T:! Vector](a: T, b: T, s: Double) -> T { return a.(Vector.Add)(b).(Vector.Scale)(s); } @@ -731,7 +742,7 @@ The behavior of calling `AddAndScaleGeneric` with a value of a specific type like `Point_Extend` is to set `T` to `Point_Extend` after all the names have been qualified. -``` +```carbon // AddAndScaleGeneric with T = Point_Extend fn AddAndScaleForPoint_Extend( a: Point_Extend, b: Point_Extend, s: Double) @@ -745,7 +756,7 @@ even when the type supplied by the caller does not [extend the implementation of the interface](terminology.md#extending-an-impl), like `Point_NoExtend`: -``` +```carbon // AddAndScaleGeneric with T = Point_NoExtend fn AddAndScaleForPoint_NoExtend( a: Point_NoExtend, b: Point_NoExtend, s: Double) @@ -777,7 +788,7 @@ substitution process to determine the return type, but the result may be a symbolic value. In this example of calling a checked generic from another checked generic, -``` +```carbon fn DoubleThreeTimes[U:! Vector](a: U) -> U { return AddAndScaleGeneric(a, a, 2.0).Scale(2.0); } @@ -793,7 +804,7 @@ capabilities of `U`. For example, given a parameterized type `GeneralPoint` implementing `Vector`, and a function that takes a `GeneralPoint` and calls `AddAndScaleGeneric` with it: -``` +```carbon class GeneralPoint(C:! Numeric) { impl as Vector { ... } fn Get[self: Self](i: i32) -> C; @@ -903,7 +914,7 @@ A named constraint definition can contain interface requirements using `require Self impls` declarations and names using `alias` declarations. Note that this allows us to declare the aspects of a facet type directly. -``` +```carbon constraint VectorLegoFish { // Interface implementation requirements require Self impls Vector; @@ -919,7 +930,7 @@ A `require Self impls` requirement may alternatively be on a named constraint, instead of an interface, to add all the requirements of another named constraint without adding any of the names: -``` +```carbon constraint DrawVectorLegoFish { // The same as requiring both `Vector` and `LegoFish`. require Self impls VectorLegoFish; @@ -948,14 +959,14 @@ constructs we do expect them to use will be defined in terms of them. For example, if `type` were not a keyword, we could define the Carbon builtin `type` as: -``` +```carbon constraint type { } ``` That is, `type` is the facet type with no requirements (so matches every type), and defines no names. -``` +```carbon fn Identity[T:! type](x: T) -> T { // Can accept values of any type. But, since we know nothing about the // type, we don't know about any operations on `x` inside this function. @@ -982,7 +993,7 @@ There is an analogy between declarations used in a `template constraint` and in an `interface` definition. If an `interface` `I` has (non-`alias`, non-`require`) declarations `X`, `Y`, and `Z`, like so: -``` +```carbon interface I { X; Y; @@ -993,7 +1004,7 @@ interface I { Then a type implementing `I` would have `impl as I` with definitions for `X`, `Y`, and `Z`, as in: -``` +```carbon class ImplementsI { // ... impl as I { @@ -1006,7 +1017,7 @@ class ImplementsI { But a `template constraint`, `S`: -``` +```carbon template constraint S { X; Y; @@ -1016,7 +1027,7 @@ template constraint S { would match any type with definitions for `X`, `Y`, and `Z` directly: -``` +```carbon class ImplementsS { // ... X { ... } @@ -1035,7 +1046,7 @@ type `I2` as long as the requirements of `I1` are a superset of the requirements of `I2`. This means a value `x: T` may be passed to functions requiring types to satisfy `I2`, as in this example: -``` +```carbon interface Printable { fn Print[self: Self](); } interface Renderable { fn Draw[self: Self](); } @@ -1067,7 +1078,7 @@ implemented, we provide a combination operator on facet types, written `&`. This operator gives the facet type with the union of all the requirements and the union of the names. -``` +```carbon interface Printable { fn Print[self: Self](); } @@ -1108,7 +1119,7 @@ PrintThenDraw(s); It is an error to use any names that conflict between the two interfaces. -``` +```carbon interface Renderable { fn Center[self: Self]() -> (i32, i32); fn Draw[self: Self](); @@ -1128,7 +1139,7 @@ Conflicts can be resolved at the call site using a [qualified member access expression](#qualified-member-names-and-compound-member-access), or by defining a named constraint explicitly and renaming the methods: -``` +```carbon constraint RenderableAndEndOfGame { require Self impls Renderable; require Self impls EndOfGame; @@ -1156,8 +1167,8 @@ gives itself, `MyTypeOfType & MyTypeOfType == MyTypeOfType`. Also, given two combination should not conflict on any names in the common base. To add to the requirements of a facet type without affecting the names, and so -avoid the possibility of name conflicts, names, use a `where .Self impls` -clause. +avoid the possibility of name conflicts, names, use a +[`where .Self impls` clause](#implements-constraints). ``` // `Printable where .Self impls Renderable` is equivalent to: @@ -1193,13 +1204,12 @@ Some interfaces will depend on other interfaces being implemented for the same type. For example, in C++, [the `Container` concept](https://en.cppreference.com/w/cpp/named_req/Container#Other_requirements) requires all containers to also satisfy the requirements of -`DefaultConstructible`, `CopyConstructible`, `EqualityComparable`, and -`Swappable`. This is already a capability for -[facet types in general](#facet-types). For consistency we will use the same -semantics and `require Self impls` syntax as we do for +`DefaultConstructible`, `CopyConstructible`, `Eq`, and `Swappable`. This is +already a capability for [facet types in general](#facet-types). For consistency +we will use the same semantics and `require Self impls` syntax as we do for [named constraints](#named-constraints): -``` +```carbon interface Equatable { fn Equals[self: Self](rhs: Self) -> bool; } interface Iterable { @@ -1227,7 +1237,7 @@ Like with named constraints, an interface implementation requirement doesn't by itself add any names to the interface, but again those can be added with `alias` declarations: -``` +```carbon interface Hashable { fn Hash[self: Self]() -> u64; require Self impls Equatable; @@ -1253,7 +1263,7 @@ When implementing an interface, we should allow implementing the aliased names as well. In the case of `Hashable` above, this includes all the members of `Equatable`, obviating the need to implement `Equatable` itself: -``` +```carbon class Song { extend impl as Hashable { fn Hash[self: Self]() -> u64 { ... } @@ -1276,7 +1286,7 @@ benefits: We expect this concept to be common enough to warrant dedicated `interface` syntax: -``` +```carbon interface Equatable { fn Equals[self: Self](rhs: Self) -> bool; } interface Hashable { @@ -1319,7 +1329,7 @@ The [`SetAlgebra` protocol](https://swiftdoc.org/v5.1/protocol/setalgebra/) extends `Equatable` and `ExpressibleByArrayLiteral`, which would be declared in Carbon: -``` +```carbon interface SetAlgebra { extend Equatable; extend ExpressibleByArrayLiteral; @@ -1331,7 +1341,7 @@ interface SetAlgebra { [associated constants](terminology.md#associated-entity) also defined in the body in parameters or constraints of the interface being extended. -``` +```carbon // A type can implement `ConvertibleTo` many times, // using different values of `T`. interface ConvertibleTo(T:! type) { ... } @@ -1351,7 +1361,7 @@ interface PreferredConversion { The `extend` declaration makes sense with the same meaning inside a [`constraint`](#named-constraints) definition, and so is also supported. -``` +```carbon interface Media { fn Play[self: Self](); } @@ -1368,7 +1378,7 @@ constraint Combined { This definition of `Combined` is equivalent to requiring both the `Media` and `Job` interfaces being implemented, and aliases their methods. -``` +```carbon // Equivalent constraint Combined { require Self impls Media; @@ -1382,7 +1392,7 @@ Notice how `Combined` has aliases for all the methods in the interfaces it requires. That condition is sufficient to allow a type to `impl` the named constraint: -``` +```carbon class Song { extend impl as Combined { fn Play[self: Self]() { ... } @@ -1393,7 +1403,7 @@ class Song { This is equivalent to implementing the required interfaces directly: -``` +```carbon class Song { extend impl as Media { fn Play[self: Self]() { ... } @@ -1410,7 +1420,7 @@ This is just like when you get an implementation of `Equatable` by implementing Conversely, an `interface` can extend a `constraint`: -``` +```carbon interface MovieCodec { extend Combined; @@ -1421,7 +1431,7 @@ interface MovieCodec { This gives `MovieCodec` the same requirements and names as `Combined`, and so is equivalent to: -``` +```carbon interface MovieCodec { require Self impls Media; alias Play = Media.Play; @@ -1437,7 +1447,7 @@ interface MovieCodec { Consider this set of interfaces, simplified from [this example generic graph library doc](https://docs.google.com/document/d/15Brjv8NO_96jseSesqer5HbghqSTJICJ_fTaZOH0Mg4/edit?usp=sharing&resourcekey=0-CYSbd6-xF8vYHv9m1rolEQ): -``` +```carbon interface Graph { fn Source[addr self: Self*](e: EdgeDescriptor) -> VertexDescriptor; fn Target[addr self: Self*](e: EdgeDescriptor) -> VertexDescriptor; @@ -1459,7 +1469,7 @@ We need to specify what happens when a graph type implements both `IncidenceGraph` and `EdgeListGraph`, since both interfaces extend the `Graph` interface. -``` +```carbon class MyEdgeListIncidenceGraph { extend impl as IncidenceGraph { ... } extend impl as EdgeListGraph { ... } @@ -1473,7 +1483,7 @@ though could be defined in the `impl` block of `IncidenceGraph`, - `IncidenceGraph` implements all methods of `Graph`, `EdgeListGraph` implements none of them. - ``` + ```carbon class MyEdgeListIncidenceGraph { extend impl as IncidenceGraph { fn Source[self: Self](e: EdgeDescriptor) -> VertexDescriptor { ... } @@ -1490,7 +1500,7 @@ though could be defined in the `impl` block of `IncidenceGraph`, - `IncidenceGraph` and `EdgeListGraph` implement all methods of `Graph` between them, but with no overlap. - ``` + ```carbon class MyEdgeListIncidenceGraph { extend impl as IncidenceGraph { fn Source[self: Self](e: EdgeDescriptor) -> VertexDescriptor { ... } @@ -1506,7 +1516,7 @@ though could be defined in the `impl` block of `IncidenceGraph`, - Explicitly implementing `Graph`. - ``` + ```carbon class MyEdgeListIncidenceGraph { extend impl as Graph { fn Source[self: Self](e: EdgeDescriptor) -> VertexDescriptor { ... } @@ -1519,7 +1529,7 @@ though could be defined in the `impl` block of `IncidenceGraph`, - Implementing `Graph` out-of-line. - ``` + ```carbon class MyEdgeListIncidenceGraph { extend impl as IncidenceGraph { ... } extend impl as EdgeListGraph { ... } @@ -1562,11 +1572,11 @@ therefore provides a way to create new types APIs, in particular with different interface implementations, by [adapting](terminology.md#adapting-a-type) them: -``` +```carbon interface Printable { fn Print[self: Self](); } -interface Comparable { +interface Ordered { fn Less[self: Self](rhs: Self) -> bool; } class Song { @@ -1574,7 +1584,7 @@ class Song { } class SongByTitle { adapt Song; - extend impl as Comparable { + extend impl as Ordered { fn Less[self: Self](rhs: Self) -> bool { ... } } } @@ -1585,7 +1595,7 @@ class FormattedSong { class FormattedSongByTitle { adapt Song; extend impl as Printable = FormattedSong; - extend impl as Comparable = SongByTitle; + extend impl as Ordered = SongByTitle; } ``` @@ -1610,10 +1620,10 @@ This allows developers to provide implementations of new interfaces (as in Inside an adapter, the `Self` type matches the adapter. Members of the original type may be accessed either by a cast: -``` +```carbon class SongByTitle { adapt Song; - extend impl as Comparable { + extend impl as Ordered { fn Less[self: Self](rhs: Self) -> bool { return (self as Song).Title() < (rhs as Song).Title(); } @@ -1623,10 +1633,10 @@ class SongByTitle { or using a qualified member access expression: -``` +```carbon class SongByTitle { adapt Song; - extend impl as Comparable { + extend impl as Ordered { fn Less[self: Self](rhs: Self) -> bool { return self.(Song.Title)() < rhs.(Song.Title)(); } @@ -1635,8 +1645,8 @@ class SongByTitle { ``` **Comparison with other languages:** This matches the Rust idiom called -"newtype", which is used to implement traits on types while avoiding coherence -problems, see +"newtype", which is used to implement traits on types while avoiding +[coherence](terminology.md#coherence) problems, see [here](https://doc.rust-lang.org/book/ch19-03-advanced-traits.html#using-the-newtype-pattern-to-implement-external-traits-on-external-types) and [here](https://github.com/Ixrec/rust-orphan-rules#user-content-why-are-the-orphan-rules-controversial). @@ -1649,9 +1659,9 @@ compiler provides it as ### Adapter compatibility -Consider a type with a facet parameter, like a hash map: +Consider a [type with a facet parameter, like a hash map](#parameterized-types): -``` +```carbon interface Hashable { ... } class HashMap(KeyT:! Hashable, ValueT:! type) { fn Find[self: Self](key: KeyT) -> Optional(ValueT); @@ -1661,7 +1671,7 @@ class HashMap(KeyT:! Hashable, ValueT:! type) { A user of this type will provide specific values for the key and value types: -``` +```carbon class Song { extend impl as Hashable { ... } // ... @@ -1678,7 +1688,7 @@ specified as requirements. This allows us to evaluate when we can convert between two different arguments to a parameterized type. Consider two adapters of `Song` that implement `Hashable`: -``` +```carbon class PlayableSong { adapt Song; extend impl as Hashable = Song; @@ -1710,7 +1720,7 @@ replacing an interface implementation. Users would indicate that an adapter starts from the original type's existing API by using the `extend` keyword before `adapt`: -``` +```carbon class Song { extend impl as Hashable { ... } extend impl as Printable { ... } @@ -1720,7 +1730,7 @@ class SongByArtist { extend adapt Song; // Add an implementation of a new interface - extend impl as Comparable { ... } + extend impl as Ordered { ... } // Replace an existing implementation of an interface // with an alternative. @@ -1730,7 +1740,7 @@ class SongByArtist { The resulting type `SongByArtist` would: -- implement `Comparable`, unlike `Song`, +- implement `Ordered`, unlike `Song`, - implement `Hashable`, but differently than `Song`, and - implement `Printable`, inherited from `Song`. @@ -1750,7 +1760,7 @@ To avoid or resolve name conflicts between interfaces, an `impl` may be declared without [`extend`](#extend-impl). The names in that interface may then be pulled in individually or renamed using `alias` declarations. -``` +```carbon class SongRenderToPrintDriver { extend adapt Song; @@ -1782,7 +1792,7 @@ an adapter that provides an implementation of `CompareLib.Comparable` for [`extend` facility of adapters](#extending-adapter) to preserve the `SongLib.Song` API. -``` +```carbon import CompareLib; import SongLib; @@ -1805,7 +1815,7 @@ class Song { The caller can either convert `SongLib.Song` values to `Song` when calling `CompareLib.Sort` or just start with `Song` values in the first place. -``` +```carbon var lib_song: SongLib.Song = ...; CompareLib.Sort((lib_song as Song,)); @@ -1824,7 +1834,7 @@ syntax. For example, given an interface `Comparable` for deciding which value is smaller: -``` +```carbon interface Comparable { fn Less[self: Self](rhs: Self) -> bool; } @@ -1833,7 +1843,7 @@ interface Comparable { We might define an adapter that implements `Comparable` for types that define another interface `Difference`: -``` +```carbon interface Difference { fn Sub[self: Self](rhs: Self) -> i32; } @@ -1859,7 +1869,7 @@ class IntWrapper { **TODO:** If we support function types, we could potentially pass a function to use to the adapter instead: -``` +```carbon class ComparableFromDifferenceFn (T:! type, Difference:! fnty(T, T)->i32) { adapt T; @@ -1889,7 +1899,7 @@ implement the interface on that instead. Any member of the class can cast its `self` parameter to the adapter type when it wants to make use of the private impl. -``` +```carbon // Public, in API file class Complex64 { // ... @@ -1924,7 +1934,7 @@ Consider a case where a function will call several functions from an interface that the type does not [extend the implementation of](terminology.md#extending-an-impl). -``` +```carbon interface DrawingContext { fn SetPen[self: Self](...); fn SetFill[self: Self](...); @@ -1940,7 +1950,7 @@ extend the implementation of the interface. This avoids having to [qualify](terminology.md#qualified-member-access-expression) each call to methods in the interface. -``` +```carbon class DrawInWindow { adapt Window; extend impl as DrawingContext = Window; @@ -1955,7 +1965,7 @@ fn Render(w: Window) { ``` **Note:** Another way to achieve this is to use a -[local symbolic facet constant](#generic-let). +[local symbolic facet constant](#compile-time-let). ```carbon fn Render(w: Window) { @@ -1991,7 +2001,7 @@ without assigning a value. As constants, they are declared using the `let` introducer. For example, a fixed-dimensional point type could have the dimension as an associated constant. -``` +```carbon interface NSpacePoint { let N:! i32; // The following require: 0 <= i < N. @@ -2006,7 +2016,7 @@ 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`: -``` +```carbon class Point2D { extend impl as NSpacePoint where .N = 2 { fn Get[addr self: Self*](i: i32) -> f64 { ... } @@ -2035,7 +2045,7 @@ keyword. The list of assignments is subject to two restrictions: These values may be accessed as members of the type: -``` +```carbon Assert(Point2D.N == 2); Assert(Point3D.N == 3); @@ -2071,7 +2081,7 @@ To be consistent with normal [class function](/docs/design/classes.md#class-functions) declaration syntax, associated class functions are written using a `fn` declaration: -``` +```carbon interface DeserializeFromString { fn Deserialize(serialized: String) -> Self; } @@ -2112,7 +2122,7 @@ implementation. We already have one example of this: the `Self` type discussed interface declares that each implementation will provide a facet constant under a specified name. For example: -``` +```carbon interface StackAssociatedFacet { let ElementType:! type; fn Push[addr self: Self*](value: ElementType); @@ -2127,7 +2137,7 @@ accepting or returning values with the type `ElementType`, which any implementer of `StackAssociatedFacet` must also define. For example, maybe a `DynamicArray` [parameterized type](#parameterized-types) implements `StackAssociatedFacet`: -``` +```carbon class DynamicArray(T:! type) { class IteratorType { ... } fn Begin[addr self: Self*]() -> IteratorType; @@ -2159,7 +2169,7 @@ The keyword `Self` can be used after the `as` in an `impl` declaration as a shorthand for the type being implemented, including in the `where` clause specifying the values of associated facets, as in: -``` +```carbon impl VeryLongTypeName as Add // `Self` here means `VeryLongTypeName` where .Result == Self { @@ -2177,7 +2187,7 @@ The definition of the `StackAssociatedFacet` is sufficient for writing a checked-generic function that operates on anything implementing that interface, for example: -``` +```carbon fn PeekAtTopOfStack[StackType:! StackAssociatedFacet](s: StackType*) -> StackType.ElementType { var top: StackType.ElementType = s->Pop(); @@ -2197,7 +2207,7 @@ Outside the checked-generic, associated facets have the concrete facet values determined by impl lookup, rather than the erased version of that facet used inside a checked-generic. -``` +```carbon var my_array: DynamicArray(i32) = (1, 2, 3); // PeekAtTopOfStack's `StackType` is set to `DynamicArray(i32)` // with `StackType.ElementType` set to `i32`. @@ -2211,7 +2221,7 @@ discussed in the [return type section](#return-type). Associated facets can also be implemented using a [member type](/docs/design/classes.md#member-type). -``` +```carbon interface Container { let IteratorType:! Iterator; ... @@ -2249,7 +2259,7 @@ also known as _generic interfaces_. To write a parameterized version of the stack interface, instead of using associated constants, write a parameter list after the name of the interface: -``` +```carbon interface StackParameterized(ElementType:! type) { fn Push[addr self: Self*](value: ElementType); fn Pop[addr self: Self*]() -> ElementType; @@ -2260,7 +2270,7 @@ interface StackParameterized(ElementType:! type) { Then `StackParameterized(Fruit)` and `StackParameterized(Veggie)` would be considered different interfaces, with distinct implementations. -``` +```carbon class Produce { var fruit: DynamicArray(Fruit); var veggie: DynamicArray(Veggie); @@ -2294,7 +2304,7 @@ parameters can't be deduced. For example, if we were to rewrite [the `PeekAtTopOfStack` example in the "associated facets" section](#associated-facets) for `StackParameterized(T)` it would generate a compile error: -``` +```carbon // ❌ Error: can't deduce interface parameter `T`. fn BrokenPeekAtTopOfStackParameterized [T:! type, StackType:! StackParameterized(T)] @@ -2305,7 +2315,7 @@ This error is because the compiler can not determine if `T` should be `Fruit` or `Veggie` when passing in argument of type `Produce*`. Either `T` should be replaced by a concrete type, like `Fruit`: -``` +```carbon fn PeekAtTopOfFruitStack [StackType:! StackParameterized(Fruit)] (s: StackType*) -> T { ... } @@ -2318,7 +2328,7 @@ var top_fruit: Fruit = Or the value for `T` would be passed explicitly, using `where` constraints described [in this section](#another-type-implements-parameterized-interface): -``` +```carbon fn PeekAtTopOfStackParameterizedImpl (T:! type, StackType:! StackParameterized(T), s: StackType*) -> T { ... @@ -2344,7 +2354,7 @@ Parameterized interfaces are useful for `OrderedWith(T)` interfaces have a parameter that allows type to be comparable with multiple other types, as in: -``` +```carbon interface EqWith(T:! type) { fn Equal[self: Self](rhs: T) -> bool; ... @@ -2375,7 +2385,7 @@ vast majority of cases. As an example, if we had an interface that allowed a type to define how the tuple-member-read operator would work, the index of the member could be an interface parameter: -``` +```carbon interface ReadTupleMember(index:! u32) { let T:! type; // Returns self[index] @@ -2389,7 +2399,7 @@ indices to be associated with different values of `T`. **Caveat:** When implementing an interface twice for a type, the interface parameters are required to always be different. For example: -``` +```carbon interface Map(FromType:! type, ToType:! type) { fn Map[addr self: Self*](needle: FromType) -> Optional(ToType); } @@ -2406,7 +2416,7 @@ In this case, it would be better to have an [adapting type](#adapting-types) to contain the `impl` for the reverse map lookup, instead of implementing the `Map` interface twice: -``` +```carbon class Bijection(FromType:! type, ToType:! type) { extend impl as Map(FromType, ToType) { ... } } @@ -2434,16 +2444,16 @@ support parameters. Those parameters work the same way as for interfaces. ## Where constraints -So far, we have restricted a generic type parameter by saying it has to -implement an interface or a set of interfaces. There are a variety of other -constraints we would like to be able to express, such as applying restrictions -to its associated types and associated constants. This is done using the `where` -operator that adds constraints to a type-of-type. +So far, we have restricted a [symbolic facet binding](#symbolic-facet-bindings) +by saying it has to implement an interface or a set of interfaces. There are a +variety of other constraints we would like to be able to express, such as +applying restrictions to associated constants. This is done using the `where` +operator that adds constraints to a [facet type](#facet-types). -The where operator can be applied to a type-of-type in a declaration context: +The where operator can be applied to a facet type in a declaration context: -``` -// Constraints on function parameters: +```carbon +// Constraints on generic function parameters: fn F[V:! D where ...](v: V) { ... } // Constraints on a class parameter: @@ -2454,7 +2464,7 @@ class S(T:! B where ...) { // Constraints on an interface parameter: interface A(T:! B where ...) { - // Constraints on an associated type: + // Constraints on an associated facet: let U:! C where ...; // Constraints on an associated method: fn G[self: Self, V:! D where ...](v: V); @@ -2463,549 +2473,1280 @@ interface A(T:! B where ...) { We also allow you to name constraints using a `where` operator in a `let` or `constraint` definition. The expressions that can follow the `where` keyword are -described in the ["constraint use cases"](#constraint-use-cases) section, but -generally look like boolean expressions that should evaluate to `true`. - -The result of applying a `where` operator to a type-of-type is another -type-of-type. Note that this expands the kinds of requirements that -type-of-types can have from just interface requirements to also include the -various kinds of constraints discussed later in this section. In addition, it -can introduce relationships between different type variables, such as that a -member of one is equal to the member of another. The `where` operator is not -associative, so a type expression using multiple must use round parens `(`...`)` -to specify grouping. - -**Comparison with other languages:** Both Swift and Rust use `where` clauses on -declarations instead of in the expression syntax. These happen after the type -that is being constrained has been given a name and use that name to express the +described in the ["kinds of `where` constraints"](#kinds-of-where-constraints) +section, but generally look like boolean expressions that should evaluate to +`true`. + +The result of applying a `where` operator to a facet type is another facet type. +Note that this expands the kinds of requirements that facet types can have from +just interface requirements to also include the various kinds of constraints +discussed later in this section. In addition, it can introduce relationships +between different type variables, such as that a member of one is equal to the +member of another. The `where` operator is not associative, so a type expression +using multiple must use round parens `(`...`)` to specify grouping. + +> **Comparison with other languages:** Both Swift and Rust use `where` clauses +> on declarations instead of in the expression syntax. These happen after the +> type that is being constrained has been given a name and use that name to +> express the constraint. +> +> Rust also supports +> [directly passing in the values for associated types](https://rust-lang.github.io/rfcs/0195-associated-items.html#constraining-associated-types) +> when using a trait as a constraint. This is helpful when specifying concrete +> types for all associated types in a trait in order to +> [make it object safe so it can be used to define a trait object type](https://rust-lang.github.io/rfcs/0195-associated-items.html#trait-objects). +> +> Rust is adding trait aliases +> ([RFC](https://github.com/rust-lang/rfcs/blob/master/text/1733-trait-alias.md), +> [tracking issue](https://github.com/rust-lang/rust/issues/41517)) to support +> naming some classes of constraints. + +**References:** `where` constraints were added in proposal +[#818: Constraints for generics (generics details 3)](https://github.com/carbon-language/carbon-lang/pull/818). + +### Kinds of `where` constraints + +There are three kinds of `where` constraints, each of which uses a different +binary operator: + +- _Rewrite constraints_: `where`...`=`... +- _Same-type constraints_: `where`...`==`... +- _Implements constraints_: `where`...`impls`... + +A rewrite constraint is written `where .A = B`, where `A` is the name of an +[associated constant](#associated-constants) which is rewritten to `B`. + +The "dot followed by the name of a member" construct, like `.A`, is called a +_designator_. The name of the designator is looked up in the constraint, and +refers to the value of that member for whatever type is to satisfy this constraint. -Rust also supports -[directly passing in the values for associated types](https://rust-lang.github.io/rfcs/0195-associated-items.html#constraining-associated-types) -when using a trait as a constraint. This is helpful when specifying concrete -types for all associated types in a trait in order to -[make it object safe so it can be used to define a trait object type](https://rust-lang.github.io/rfcs/0195-associated-items.html#trait-objects). - -Rust is adding trait aliases -([RFC](https://github.com/rust-lang/rfcs/blob/master/text/1733-trait-alias.md), -[tracking issue](https://github.com/rust-lang/rust/issues/41517)) to support -naming some classes of constraints. - -### Constraint use cases +> **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. -#### Set an associated constant to a specific value +A same-type constraint is written `where X == Y`, where `X` and `Y` both name +facets. The constraint is that `X as type` must be the same as `Y as type`. In +cases where a constraint may be written in either form, prefer a rewrite +constraint over a same-type constraint. Note that switching between the two +forms does not change which types satisfies the constraint, and so is a +compatible change for callers. -We might need to write a function that only works with a specific value of an -[associated constant](#associated-constants) `N`. In this case, the name of the -associated constant is written after a `.`, followed by an `=`, and then the -value: +An implements constraint is written `where T impls C`, where `T` is a facet and +`C` is a facet type. The constraint is that `T` satisfies the requirements of +`C`. -``` -fn PrintPoint2D[PointT:! NSpacePoint where .N = 2](p: PointT) { - Print(p.Get(0), ", ", p.Get(1)); -} -``` +**References:** The definition of rewrite and same-type constraints were +[proposal #2173](https://github.com/carbon-language/carbon-lang/pull/2173). +Implements constraints switched using the `impls` keyword in +[proposal #2483](https://github.com/carbon-language/carbon-lang/pull/2483). -Similarly in an interface definition: +**Alternatives considered:** -``` -interface Has2DPoint { - let PointT:! NSpacePoint where .N = 2; -} -``` +- [Different equality constraint operators for symbolic and constants](/proposals/p2173.md#status-quo) +- [Single one-step equality constraint operators that merges constraints](/proposals/p2173.md#equal-types-with-different-interfaces) +- [Restrict constraints to allow computable type equality](/proposals/p2173.md#restrict-constraints-to-allow-computable-type-equality) +- [Find a fully transitive approach to type equality](/proposals/p2173.md#find-a-fully-transitive-approach-to-type-equality) +- [Different syntax for rewrite constraint](/proposals/p2173.md#different-syntax-for-rewrite-constraint) +- [Different syntax for same-type constraint](/proposals/p2173.md#different-syntax-for-same-type-constraint) +- [Required ordering for rewrites](/proposals/p2173.md#required-ordering-for-rewrites) +- [Multi-constraint `where` clauses](/proposals/p2173.md#multi-constraint-where-clauses) +- [Rewrite constraints in `impl as` constraints](/proposals/p2173.md#rewrite-constraints-in-impl-as-constraints) -The "dot followed by the name of a member" construct, `.N` in the examples -above, is called a _designator_. A designator refers to the value of that member -for whatever type is to satisfy this constraint. +#### Recursive constraints -To name such a constraint, you may use a `let` or a `constraint` declaration: +We sometimes need to constrain a type to equal one of its associated facets. In +this first example, we want to represent the function `Abs` which will return +`Self` for some but not all types, so we use an associated facet `MagnitudeType` +to encode the return type: -``` -let Point2DInterface:! auto = NSpacePoint where .N = 2; -constraint Point2DInterface { - extend NSpacePoint where .N = 2; +```carbon +interface HasAbs { + extend Numeric; + let MagnitudeType:! Numeric; + fn Abs[self: Self]() -> MagnitudeType; } ``` -This syntax is also used to specify the values of -[associated constants](#associated-constants) when implementing an interface for -a type. +For types representing subsets of the real numbers, such as `i32` or `f32`, the +`MagnitudeType` will match `Self`, the type implementing an interface. For types +representing complex numbers, the types will be different. For example, the +`Abs()` applied to a `Complex64` value would produce a `f32` result. The goal is +to write a constraint to restrict to the first case. -**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. +In a second example, when you take the slice of a type implementing `Container` +you get a type implementing `Container` which may or may not be the same type as +the original container type. However, taking the slice of a slice always gives +you the same type, and some functions want to only operate on containers whose +slice type is the same as the container type. -A constraint to say that two associated constants should have the same value -without specifying what specific value they should have must use `==` instead of -`=`: +To solve this problem, we think of `Self` as an actual associated facet member +of every interface. We can then address it using `.Self` in a `where` clause, +like any other associated facet member. -``` -interface PointCloud { - let Dim:! i32; - let PointT:! NSpacePoint where .N == Dim; +```carbon +fn Relu[T:! HasAbs where .MagnitudeType = .Self](x: T) { + // T.MagnitudeType == T so the following is allowed: + return (x.Abs() + x) / 2; +} +fn UseContainer[T:! Container where .SliceType = .Self](c: T) -> bool { + // T.SliceType == T so `c` and `c.Slice(...)` can be compared: + return c == c.Slice(...); } ``` -#### Same type constraints +Notice that in an interface definition, `Self` refers to the type implementing +this interface while `.Self` refers to the associated facet currently being +defined. -##### Set an associated type to a specific value +```carbon +interface Container { + let ElementType:! type; -Functions accepting a generic type might also want to constrain one of its -associated types to be a specific, concrete type. For example, we might want to -have a function only accept stacks containing integers: + let SliceType:! Container + where .ElementType = ElementType and + // `.Self` means `SliceType`. + .SliceType = .Self; -``` -fn SumIntStack[T:! Stack where .ElementType = i32](s: T*) -> i32 { - var sum: i32 = 0; - while (!s->IsEmpty()) { - // s->Pop() has type `T.ElementType` == i32: - sum += s->Pop(); - } - return sum; + // `Self` means the type implementing `Container`. + fn GetSlice[addr self: Self*] + (start: IteratorType, end: IteratorType) -> SliceType; } ``` -To name these sorts of constraints, we could use `let` declarations or -`constraint` definitions: +Note that [naming](#named-constraint-constants) a recursive constraint using the +[`constraint` introducer](#named-constraints) approach, we can name the +implementing type using `Self` instead of `.Self`, since they refer to the same +type: -``` -let IntStack:! auto = Stack where .ElementType = i32; -constraint IntStack { - extend Stack where .ElementType = i32; +```carbon +constraint RealAbs { + extend HasAbs where .MagnitudeType = Self; + // Equivalent to: + extend HasAbs where .MagnitudeType = .Self; +} + +constraint ContainerIsSlice { + extend Container where .SliceType = Self; + // Equivalent to: + extend Container where .SliceType = .Self; } ``` -This syntax is also used to specify the values of -[associated constants](#associated-constants) when implementing an interface for -a type. +The `.Self` construct follows these rules: -##### Equal generic types +- `X :!` introduces `.Self:! type`, where references to `.Self` are resolved. + to `X`. This allows you to use `.Self` as an interface parameter as in + `X:! I(.Self)`. +- `A where` introduces `.Self:! A` and `.Foo` _designator_ for each member + `Foo` of `A`. +- It's an error to reference `.Self` if it refers to more than one different + thing or isn't a facet. +- You get the innermost, most-specific type for `.Self` if it is introduced + twice in a scope. By the previous rule, it is only legal if they all refer + to the same facet binding. +- `.Self` may not be on the left side of the `=` in a rewrite constraint. -Alternatively, two generic types could be constrained to be equal to each other, -without specifying what that type is. This uses `==` instead of `=`. For -example, we could make the `ElementType` of an `Iterator` interface equal to the -`ElementType` of a `Container` interface as follows: +So in `X:! A where ...`, `.Self` is introduced twice, after the `:!` and the +`where`. This is allowed since both times it means `X`. After the `:!`, `.Self` +has the type `type`, which gets refined to `A` after the `where`. In contrast, +it is an error if `.Self` could mean two different things, as in: +```carbon +// ❌ Illegal: `.Self` could mean `T` or `T.A`. +fn F[T:! InterfaceA where .A impls + (InterfaceB where .B = .Self)](x: T); ``` -interface Iterator { - let ElementType:! type; - ... + +#### Rewrite constraints + +In a rewrite constraint, the left-hand operand of `=` must be a `.` followed by +the name of an associated constant. `.Self` is not permitted. + +```carbon +interface RewriteSelf { + // ❌ Error: `.Self` is not the name of an associated constant. + let Me:! type where .Self = Self; } -interface Container { - let ElementType:! type; - let IteratorType:! Iterator where .ElementType == ElementType; - ... +interface HasAssoc { + let Assoc:! type; +} +interface RewriteSingleLevel { + // ✅ Uses of `A.Assoc` will be rewritten to `i32`. + let A:! HasAssoc where .Assoc = i32; +} +interface RewriteMultiLevel { + // ❌ Error: Only one level of associated constant is permitted. + let B:! RewriteSingleLevel where .A.Assoc = i32; } ``` -Given an interface with two associated types +This notation is permitted anywhere a constraint can be written, and results in +a new constraint with a different interface: the named member effectively no +longer names an associated constant of the constrained type, and is instead +treated as a rewrite rule that expands to the right-hand side of the constraint, +with any mentioned parameters substituted into that type. -``` -interface PairInterface { - let Left:! type; - let Right:! type; -} +```carbon +interface Container { + let Element:! type; + let Slice:! Container where .Element = Element; + fn Add[addr self: Self*](x: Element); +} +// `T.Slice.Element` rewritten to `T.Element` +// because type of `T.Slice` says `.Element = Element`. +// `T.Element` rewritten to `i32` +// because type of `T` says `.Element = i32`. +fn Add[T:! Container where .Element = i32](p: T*, y: T.Slice.Element) { + // ✅ Argument `y` has the same type `i32` as parameter `x` of + // `T.(Container.Add)`, which is also rewritten to `i32`. + p->Add(y); +} +``` + +Rewrites aren't performed on the left-hand side of such an `=`, so +`where .A = .B and .A = C` is not rewritten to `where .A = .B and .B = C`. +Instead, such a `where` clause is invalid when the constraint is +[resolved](#rewrite-constraint-resolution) unless each rule for `.A` specifies +the same rewrite. + +Note that `T:! C where .R = i32` can result in a type `T.R` whose behavior is +different from the behavior of `T.R` given `T:! C`. For example, member lookup +into `T.R` can find different results and operations can therefore have +different behavior. However, this does not violate +[coherence](/proposals/p2173.md#coherence) because the facet types `C` and +`C where .R = i32` don't differ by merely having more type information; rather, +they are different facet types that have an isomorphic set of values, somewhat +like `i32` and `u32`. An `=` constraint is not merely learning a new fact about +a type, it is requesting different behavior. + +This approach has some good properties that +[same-type constraints](#same-type-constraints) have problems with: + +- [Equal types with different interfaces](/proposals/p2173.md#equal-types-with-different-interfaces): + When an associated facet is constrained to be a concrete type, it is + desirable for the associated facet to behave like that concrete type. +- [Type canonicalization](/proposals/p2173.md#type-canonicalization): to + enable efficient type equality. +- [Transitivity of equality of types](/proposals/p2173.md#transitivity-of-equality) + +##### Combining constraints with `&` + +Suppose we have `X = C where .R = A` and `Y = C where .R = B`. What should +`C & X` produce? What should `X & Y` produce? + +- Combining two rewrite rules with different rewrite targets results in a + facet type where the associated constant is ambiguous. Given `T:! X & Y`, + the type expression `T.R` is ambiguous between a rewrite to `A` and a + rewrite to `B`. But given `T:! X & X`, `T.R` is unambiguously rewritten to + `A`. +- Combining a constraint with a rewrite rule with a constraint with no rewrite + rule preserves the rewrite rule, so `C & X` is the same as `X`. For example, + supposing that `interface Container` extends `interface Iterable`, and + `Iterable` has an associated constant `Element`, the constraint + `Container & (Iterable where .Element = i32)` is the same as the constraint + `(Container & Iterable) where .Element = i32` which is the same as the + constraint `Container where .Element = i32`. + +If the rewrite for an associated constant is ambiguous, the facet type is +rejected during [constraint resolution](#rewrite-constraint-resolution). + +> **Alternative considered:** We could perhaps say that `X & Y` results in a +> facet type where the type of `R` has the union of the interface of `A` and the +> interface of `B`, and that `C & X` similarly results in a facet type where the +> type of `R` has the union of the interface of `A` and the interface originally +> specified by `C`. + +##### Combining constraints with `and` + +It's possible for one `=` constraint in a `where` to refer to another. When this +happens, the facet type `C where A and B` is interpreted as +`(C where A) where B`, so rewrites in `A` are applied immediately to names in +`B`, but rewrites in `B` are not applied to names in `A` until the facet type is +[resolved](#rewrite-constraint-resolution): + +```carbon +interface C { + let T:! type; + let U:! type; + let V:! type; +} +class M { + alias Me = Self; +} +// ✅ Same as `C where .T = M and .U = M.Me`, which is +// the same as `C where .T = M and .U = M`. +fn F[A:! C where .T = M and .U = .T.Me]() {} +// ❌ No member `Me` in `A.T:! type`. +fn F[A:! C where .U = .T.Me and .T = M]() {} ``` -we can constrain them to be equal in a function signature: +##### Combining constraints with `extends` -``` -fn F[MatchedPairType:! PairInterface where .Left == .Right] - (x: MatchedPairType*); -``` +Within an interface or named constraint, `extends` can be used to extend a +constraint that has rewrites. + +```carbon +interface A { + let T:! type; + let U:! type; +} +interface B { + extends A where .T = .U and .U = i32; +} -or in an interface definition: +var n: i32; +// ✅ Resolved constraint on `T` is +// `B where .(A.T) = i32 and .(A.U) = i32`. +// `T.(A.T)` is rewritten to `i32`. +fn F(T:! B) -> T.(A.T) { return n; } ``` -interface HasEqualPair { - let P:! PairInterface where .Left == .Right; + +##### Combining constraints with `impl as` and `impls` + +Within an interface or named constraint, the `impl T as C` syntax does not +permit `=` constraints to be specified directly. However, such constraints can +be specified indirectly, for example if `C` is a named constraint that contains +rewrites. Because these constraints don't change the type of `T`, rewrite +constraints in this context will never result in a rewrite being performed, and +instead are equivalent to `==` constraints. + +```carbon +interface A { + let T:! type; + let U:! type; +} +constraint C { + extends A where .T = .U and .U = i32; +} +constraint D { + extends A where .T == .U and .U == i32; +} +interface B { + // OK, equivalent to `impl as D;` or + // `impl as A where .T == .U and .U == i32;`. + impl as C; } -``` -This kind of constraint can be named: +var n: i32; +// ❌ No implicit conversion from `i32` to `T.(A.T)`. +// Resolved constraint on `T` is +// `B where T.(A.T) == T.(A.U) and T.(A.U) = i32`. +// `T.(A.T)` is single-step equal to `T.(A.U)`, and +// `T.(A.U)` is single-step equal to `i32`, but +// `T.(A.T)` is not single-step equal to `i32`. +fn F(T:! B) -> T.(A.T) { return n; } ``` -let EqualPair:! auto = - PairInterface where .Left == .Right; -constraint EqualPair { - extend PairInterface where .Left == .Right; + +A purely syntactic check is used to determine if an `=` is specified directly in +an expression: + +- An `=` constraint is specified directly in its enclosing `where` expression. +- If an `=` constraint is specified directly in an operand of an `&` or + `(`...`)`, then it is specified directly in that enclosing expression. + +In an `impl as C` or `impl T as C` declaration in an interface or named +constraint, `C` is not allowed to directly specify any `=` constraints: + +```carbon +// Compile-time identity function. +fn Identity[T:! type](x:! T) -> T { return x; } + +interface E { + // ❌ Rewrite constraint specified directly. + impl as A where .T = .U and .U = i32; + // ❌ Rewrite constraint specified directly. + impl as type & (A where .T = .U and .U = i32); + // ✅ Not specified directly, but does not result + // in any rewrites being performed. + impl as Identity(A where .T = .U and .U = i32); } ``` -Another example of same type constraints is when associated types of two -different interfaces are constrained to be equal: +The same rules apply to `impls` constraints. Note that `.T == U` constraints are +also not allowed in this context, because the reference to `.T` is rewritten to +`.Self.T`, and `.Self` is ambiguous. -``` -fn Map[CT:! Container, - FT:! Function where .InputType == CT.ElementType] - (c: CT, f: FT) -> Vector(FT.OutputType); -``` +```carbon +// ❌ Rewrite constraint specified directly in `impls`. +fn F[T:! A where .U impls (A where .T = i32)](); -###### Satisfying both type-of-types +// ❌ Reference to `.T` in same-type constraint is ambiguous: +// does this mean the outer or inner `.Self.T`? +fn G[T:! A where .U impls (A where .T == i32)](); -If the two types being constrained to be equal have been declared with different -type-of-types, then the actual type value they are set to will have to satisfy -both constraints. For example, if `SortedContainer.ElementType` is declared to -be `Comparable`, then in this declaration: +// ✅ Not specified directly, but does not result +// in any rewrites being performed. Return type +// is not rewritten to `i32`. +fn H[T:! type where .Self impls C]() -> T.(A.U); -``` -fn Contains - [SC:! SortedContainer, - CT:! Container where .ElementType == SC.ElementType] - (haystack: SC, needles: CT) -> bool; +// ✅ Return type is rewritten to `i32`. +fn I[T:! C]() -> T.(A.U); ``` -the `where` constraint means `CT.ElementType` must satisfy `Comparable` as well. -However, inside the body of `Contains`, `CT.ElementType` will act like the -implementation of `Comparable` is declared without [`extend`](#extend-impl). -That is, items from the `needles` container won't directly have a `Compare` -method member, but can still be implicitly converted to `Comparable` and can -still call `Compare` using the compound member access syntax, -`needle.(Comparable.Compare)(elt)`. The rule is that an `==` `where` constraint -between two type variables does not modify the set of member names of either -type. (If you write `where .ElementType = String` with a `=` and a concrete -type, then `.ElementType` is actually set to `String` including the complete -`String` API.) +##### Rewrite constraint resolution -Note that `==` constraints are symmetric, so the previous declaration of -`Contains` is equivalent to an alternative declaration where `CT` is declared -first and the `where` clause is attached to `SortedContainer`: +**FIXME: Should the precise rules for constraints be moved into an appendix?** -``` -fn Contains - [CT:! Container, - SC:! SortedContainer where .ElementType == CT.ElementType] - (haystack: SC, needles: CT) -> bool; -``` +When a facet type is used as the declared type of a facet `T`, the constraints +that were specified within that facet type are _resolved_ to determine the +constraints that apply to `T`. This happens: -#### Type bound for associated type +- When the constraint is used explicitly, when declaring symbolic binding, + like a generic parameter or associated constant, of the form + `T:! Constraint`. +- When declaring that a type implements a constraint with an `impl` + declaration, such as `impl T as Constraint`. Note that this does not include + `impl ... as` constraints appearing in `interface` or `constraint` + declarations. -A `where` clause can express that a type must implement an interface. This is -more flexible than the usual approach of including that interface in the type -since it can be applied to associated type members as well. +In each case, the following steps are performed to resolve the facet type's +abstract constraints into a set of constraints on `T`: -##### Type bounds on associated types in declarations +- If multiple rewrites are specified for the same associated constant, they + are required to be identical, and duplicates are discarded. +- Rewrites are performed on other rewrites in order to find a fixed point, + where no rewrite applies within any other rewrite. If no fixed point exists, + the generic parameter declaration or `impl` declaration is invalid. +- Rewrites are performed throughout the other constraints in the facet type -- + that is, in any `==` constraints and `impls` constraints -- and the type + `.Self` is replaced by `T` throughout the constraint. -In the following example, normally the `ElementType` of a `Container` can be any -type. The `SortContainer` function, however, takes a pointer to a type -satisfying `Container` with the additional constraint that its `ElementType` -must satisfy the `Comparable` interface, using an `impls` constraint: +```carbon +// ✅ `.T` in `.U = .T` is rewritten to `i32` when initially +// forming the facet type. +// Nothing to do during constraint resolution. +fn InOrder[A:! C where .T = i32 and .U = .T]() {} +// ✅ Facet type has `.T = .U` before constraint resolution. +// That rewrite is resolved to `.T = i32`. +fn Reordered[A:! C where .T = .U and .U = i32]() {} +// ✅ Facet type has `.U = .T` before constraint resolution. +// That rewrite is resolved to `.U = i32`. +fn ReorderedIndirect[A:! (C where .T = i32) & (C where .U = .T)]() {} +// ❌ Constraint resolution fails because +// no fixed point of rewrites exists. +fn Cycle[A:! C where .T = .U and .U = .T]() {} +``` + +To find a fixed point, we can perform rewrites on other rewrites, cycling +between them until they don't change or until a rewrite would apply to itself. +In the latter case, we have found a cycle and can reject the constraint. Note +that it's not sufficient to expand only a single rewrite until we hit this +condition: +```carbon +// ❌ Constraint resolution fails because +// no fixed point of rewrites exists. +// If we only expand the right-hand side of `.T`, +// we find `.U`, then `.U*`, then `.U**`, and so on, +// and never detect a cycle. +// If we alternate between them, we find +// `.T = .U*`, then `.U = .U**`, then `.V = .U***`, +// then `.T = .U**`, then detect that the `.U` rewrite +// would apply to itself. +fn IndirectCycle[A:! C where .T = .U and .U = .V* and .V = .U*](); ``` -interface Container { - let ElementType:! type; - ... -} -fn SortContainer - [ContainerType:! Container where .ElementType impls Comparable] - (container_to_sort: ContainerType*); +After constraint resolution, no references to rewritten associated constants +remain in the constraints on `T`. + +If a facet type is never used to constrain a type, it is never subject to +constraint resolution, and it is possible for a facet type to be formed for +which constraint resolution would always fail. For example: + +```carbon +package Broken api; + +interface X { + let T:! type; + let U:! type; +} +let Bad:! auto = (X where .T = .U) & (X where .U = .T); +// Bad is not used here. ``` -In contrast to [a same type constraint](#same-type-constraints), this does not -say what type `ElementType` exactly is, just that it must satisfy some -type-of-type. +In such cases, the facet type `Broken.Bad` is not usable: any attempt to use +that facet type to constrain a type would perform constraint resolution, which +would always fail because it would discover a cycle between the rewrites for +`.T` and for `.U`. In order to ensure that such cases are diagnosed, a trial +constraint resolution is performed for all facet types. Note that this trial +resolution can be skipped for facet types that are actually used, which is the +common case. -**Note:** `Container` defines `ElementType` as having type `type`, but -`ContainerType.ElementType` has type `Comparable`. This is because -`ContainerType` has type `Container where .ElementType impls Comparable`, not -`Container`. This means we need to be a bit careful when talking about the type -of `ContainerType` when there is a `where` clause modifying it. +##### Precise rules and termination -##### Type bounds on associated types in interfaces +This section explains the detailed rules used to implement rewrites. There are +two properties we aim to satisfy: -Given these definitions (omitting `ElementType` for brevity): +1. After type-checking, no symbolic references to associated constants that + have an associated rewrite rule remain. +2. Type-checking always terminates in a reasonable amount of time, ideally + linear in the size of the problem. -``` -interface IteratorInterface { ... } -interface ContainerInterface { - let IteratorType:! IteratorInterface; - ... +Rewrites are applied in two different phases of program analysis. + +- During qualified name lookup and type checking for qualified member access, + if a rewritten member is looked up, the right-hand side's value and type are + used for subsequent checks. +- During substitution, if the symbolic name of an associated constant is + substituted into, and substitution into the left-hand side results in a + value with a rewrite for that constant, that rewrite is applied. + +In each case, we always rewrite to a value that satisfies property 1 above, and +these two steps are the only places where we might form a symbolic reference to +an associated cosntant, so property 1 is recursively satisfied. Moreover, we +apply only one rewrite in each of the above cases, satisfying property 2. + +###### Qualified name lookup + +Qualified name lookup into either a facet parameter or into an expression whose +type is a symbolic type `T` -- either a facet parameter or an associated facet +-- considers names from the facet type `C` of `T`, that is, from `T`’s declared +type. + +```carbon +interface C { + let M:! i32; + let U:! C; } -interface RandomAccessIterator { - extend IteratorInterface; - ... +fn F[T:! C](x: T) { + // Value is C.M in all four of these + let a: i32 = x.M; + let b: i32 = T.M; + let c: i32 = x.U.M; + let d: i32 = T.U.M; } ``` -We can then define a function that only accepts types that implement -`ContainerInterface` where its `IteratorType` associated type implements -`RandomAccessIterator`: - -``` -fn F[ContainerType:! ContainerInterface - where .IteratorType impls RandomAccessIterator] - (c: ContainerType); -``` +When looking up the name `N`, if `C` is an interface `I` and `N` is the name of +an associated constant in that interface, the result is a symbolic value +representing "the member `N` of `I`". If `C` is formed by combining interfaces +with `&`, all such results are required to find the same associated constant, +otherwise we reject for ambiguity. -We would like to be able to name this constraint, defining a -`RandomAccessContainer` to be a type-of-type whose types satisfy -`ContainerInterface` with an `IteratorType` satisfying `RandomAccessIterator`. +If a member of a class or interface is named in a qualified name lookup, the +type of the result is determined by performing a substitution. For an interface, +`Self` is substituted for the self type, and any parameters for that class or +interface (and enclosing classes or interfaces, if any) are substituted into the +declared type. -``` -let RandomAccessContainer:! auto = - ContainerInterface where .IteratorType impls RandomAccessIterator; -// or -constraint RandomAccessContainer { - extend ContainerInterface - where .IteratorType impls RandomAccessIterator; +```carbon +interface SelfIface { + fn Get[self: Self]() -> Self; +} +class UsesSelf(T:! type) { + // Equivalent to `fn Make() -> UsesSelf(T)*;` + fn Make() -> Self*; + impl as SelfIface; } -// With the above definition: -fn F[ContainerType:! RandomAccessContainer](c: ContainerType); -// is equivalent to: -fn F[ContainerType:! ContainerInterface - where .IteratorType impls RandomAccessIterator] - (c: ContainerType); -``` +// ✅ `T = i32` is substituted into the type of `UsesSelf(T).Make`, +// so the type of `UsesSelf(i32).Make` is `fn () -> UsesSelf(i32)*`. +let x: UsesSelf(i32)* = UsesSelf(i32).Make(); -#### Combining constraints +// ✅ `Self = UsesSelf(i32)` is substituted into the type +// of `SelfIface.Get`, so the type of `UsesSelf(i32).(SelfIface.Get)` +// is `fn [self: UsesSelf(i32)]() -> UsesSelf(i32)`. +let y: UsesSelf(i32) = x->Get(); +``` -Constraints can be combined by separating constraint clauses with the `and` -keyword. This example expresses a constraint that two associated types are equal -and satisfy an interface: +If a facet type `C` into which lookup is performed includes a `where` clause +saying `.N = U`, and the result of qualified name lookup is the associated +constant `N`, that result is replaced by `U`, and the type of the result is the +type of `U`. No substitution is performed in this step, not even a `Self` +substitution -- any necessary substitutions were already performed when forming +the facet type `C`, and we don’t consider either the declared type or value of +the associated constant at all for this kind of constraint. Going through an +example in detail: +```carbon +interface A { + let T:! type; +} +interface B { + let U:! type; + // More explicitly, this is of type `A where .(A.T) = Self.(B.U)` + let V:! A where .T = U; +} +// Type of W is B. +fn F[W:! B](x: W) { + // The type of the expression `W` is `B`. + // `W.V` finds `B.V` with type `A where .(A.T) = Self.(B.U)`. + // We substitute `Self` = `W` giving the type of `u` as + // `A where .(A.T) = W.(B.U)`. + let u:! auto = W.V; + // The type of `u` is `A where .(A.T) = W.(B.U)`. + // Lookup for `u.T` resolves it to `u.(A.T)`. + // So the result of the qualified member access is `W.(B.U)`, + // and the type of `v` is the type of `W.(B.U)`, namely `type`. + // No substitution is performed in this step. + let v:! auto = u.T; +} ``` -fn EqualContainers - [CT1:! Container, - CT2:! Container where .ElementType impls HasEquality - and .ElementType == CT1.ElementType] - (c1: CT1*, c2: CT2*) -> bool; + +The more complex case of + +```carbon +fn F2[Z:! B where .U = i32](x: Z); ``` -**Comparison with other languages:** Swift and Rust use commas `,` to separate -constraint clauses, but that only works because they place the `where` in a -different position in a declaration. In Carbon, the `where` is attached to a -type in a parameter list that is already using commas to separate parameters. +is discussed later. -#### Recursive constraints +###### Type substitution -We sometimes need to constrain a type to equal one of its associated types. In -this first example, we want to represent the function `Abs` which will return -`Self` for some but not all types, so we use an associated type `MagnitudeType` -to encode the return type: +At various points during the type-checking of a Carbon program, we need to +substitute a set of (binding, value) pairs into a symbolic value. We saw an +example above: substituting `Self = W` into the type `A where .(A.T) = Self.U` +to produce the value `A where .(A.T) = W.U`. Another important case is the +substitution of inferred parameter values into the type of a function when +type-checking a function call: -``` -interface HasAbs { - extend Numeric; - let MagnitudeType:! Numeric; - fn Abs[self: Self]() -> MagnitudeType; +```carbon +fn F[T:! C](x: T) -> T; +fn G(n: i32) -> i32 { + // Deduces T = i32, which is substituted + // into the type `fn (x: T) -> T` to produce + // `fn (x: i32) -> i32`, giving `i32` as the type + // of the call expression. + return F(n); } ``` -For types representing subsets of the real numbers, such as `i32` or `f32`, the -`MagnitudeType` will match `Self`, the type implementing an interface. For types -representing complex numbers, the types will be different. For example, the -`Abs()` applied to a `Complex64` value would produce a `f32` result. The goal is -to write a constraint to restrict to the first case. +Qualified name lookup is not re-done as a result of type substitution. For a +template, we imagine there’s a completely separate step that happens before type +substitution, where qualified name lookup is redone based on the actual value of +template arguments; this proceeds as described in the previous section. +Otherwise, we performed the qualified name lookup when type-checking symbolic +expressions, and do not do it again: -In a second example, when you take the slice of a type implementing `Container` -you get a type implementing `Container` which may or may not be the same type as -the original container type. However, taking the slice of a slice always gives -you the same type, and some functions want to only operate on containers whose -slice type is the same as the container type. +```carbon +interface IfaceHasX { + let X:! type; +} +class ClassHasX { + class X {} +} +interface HasAssoc { + let Assoc:! IfaceHasX; +} -To solve this problem, we think of `Self` as an actual associated type member of -every interface. We can then address it using `.Self` in a `where` clause, like -any other associated type member. +// Qualified name lookup finds `T.(HasAssoc.Assoc).(IfaceHasX.X)`. +fn F(T:! HasAssoc) -> T.Assoc.X; +fn G(T:! HasAssoc where .Assoc = ClassHasX) { + // `T.Assoc` rewritten to `ClassHasX` by qualified name lookup. + // Names `ClassHasX.X`. + var a: T.Assoc.X = {}; + // Substitution produces `ClassHasX.(IfaceHasX.X)`, + // not `ClassHasX.X`. + var b: auto = F(T); +} ``` -fn Relu[T:! HasAbs where .MagnitudeType == .Self](x: T) { - // T.MagnitudeType == T so the following is allowed: - return (x.Abs() + x) / 2; + +During substitution, we might find a member access that named an opaque symbolic +associated constant in the original value can now be resolved to some specific +value. It’s important that we perform this resolution: + +```carbon +interface A { + let T:! type; } -fn UseContainer[T:! Container where .SliceType == .Self](c: T) -> bool { - // T.SliceType == T so `c` and `c.Slice(...)` can be compared: - return c == c.Slice(...); +class K { fn Member(); } +fn H[U:! A](x: U) -> U.T; +fn J[V:! A where .T = K](y: V) { + // We need the interface of `H(y)` to include + // `K.Member` in order for this lookup to succeed. + H(y).Member(); +} +``` + +The values being substituted into the symbolic value are themselves already +fully substituted and resolved, and in particular, satisfy property 1 given +above. + +Substitution proceeds by recursively rebuilding each symbolic value, bottom-up, +replacing each substituted binding with its value. Doing this naively will +propagate values like `i32` in the `F`/`G` case earlier in this section, but +will not propagate rewrite constants like in the `H`/`J` case. The reason is +that the `.T = K` constraint is in the _type_ of the substituted value, rather +than in the substituted value itself: deducing `T = i32` and converting `i32` to +the type `C` of `T` preserves the value `i32`, but deducing `U = V` and +converting `V` to the type `A` of `U` discards the rewrite constraint. + +In order to apply rewrites during substitution, we associate a set of rewrites +with each value produced by the recursive rebuilding procedure. This is somewhat +like having substitution track a refined facet type for the type of each value, +but we don’t need -- or want -- for the type to change during this process, only +for the rewrites to be properly applied. For a substituted binding, this set of +rewrites is the rewrites found on the type of the corresponding value prior to +conversion to the type of the binding. When rebuilding a member access +expression, if we have a rewrite corresponding to the accessed member, then the +resulting value is the target of the rewrite, and its set of rewrites is that +found in the type of the target of the rewrite, if any. Because the target of +the rewrite is fully resolved already, we can ask for its type without +triggering additional work. In other cases, the rewrite set is empty; all +necessary rewrites were performed when type-checking the value we're +substituting into. + +Continuing an example from [qualified name lookup](#qualified-name-lookup): + +```carbon +interface A { + let T:! type; +} +interface B { + let U:! type; + let V:! A where .T = U; +} + +// Type of the expression `Z` is `B where .(B.U) = i32` +fn F2[Z:! B where .U = i32](x: Z) { + // The type of the expression `Z` is `B where .U = i32`. + // `Z.V` is looked up and finds the associated facet `(B.V)`. + // The declared type is `A where .(A.T) = Self.U`. + // We substitute `Self = Z` with rewrite `.U = i32`. + // The resulting type is `A where .(A.T) = i32`. + // So `u` is `Z.V` with type `A where .(A.T) = i32`. + let u:! auto = Z.V; + // The type of `u` is `A where .(A.T) = i32`. + // Lookup for `u.T` resolves it to `u.(A.T)`. + // So the result of the qualified member access is `i32`, + // and the type of `v` is the type of `i32`, namely `type`. + // No substitution is performed in this step. + let v:! auto = u.T; } ``` -Notice that in an interface definition, `Self` refers to the type implementing -this interface while `.Self` refers to the associated type currently being -defined. +###### Examples -``` +```carbon interface Container { - let ElementType:! type; + let Element:! type; +} +interface SliceableContainer { + extends Container; + let Slice:! Container where .Element = Self.(Container.Element); +} +// ❌ Qualified name lookup rewrites this facet type to +// `SliceableContainer where .(Container.Element) = .Self.(Container.Element)`. +// Constraint resolution rejects this because this rewrite forms a cycle. +fn Bad[T:! SliceableContainer where .Element = .Slice.Element](x: T.Element) {} +``` - let SliceType:! Container - where .ElementType == ElementType and - .SliceType == .Self; +```carbon +interface Helper { + let D:! type; +} +interface Example { + let B:! type; + let C:! Helper where .D = B; +} +// ✅ `where .D = ...` by itself is fine. +// `T.C.D` is rewritten to `T.B`. +fn Allowed(T:! Example, x: T.C.D); +// ❌ But combined with another rewrite, creates an infinite loop. +// `.C.D` is rewritten to `.B`, resulting in `where .B = .B`, +// which causes an error during constraint resolution. +// Using `==` instead of `=` would make this constraint redundant, +// rather than it being an error. +fn Error(T:! Example where .B = .C.D, x: T.C.D); +``` - fn GetSlice[addr self: Self*] - (start: IteratorType, end: IteratorType) -> SliceType; +```carbon +interface Allowed; +interface AllowedBase { + let A:! Allowed; +} +interface Allowed { + extends AllowedBase where .A = .Self; } +// ✅ The final type of `x` is `T`. It is computed as follows: +// In `((T.A).A).A`, the inner `T.A` is rewritten to `T`, +// resulting in `((T).A).A`, which is then rewritten to +// `(T).A`, which is then rewritten to `T`. +fn F(T:! Allowed, x: ((T.A).A).A); ``` -These recursive constraints can be named: +```carbon +interface MoveYsRight; +constraint ForwardDeclaredConstraint(X:! MoveYsRight); +interface MoveYsRight { + let X:! MoveYsRight; + // Means `Y:! MoveYsRight where .X = X.Y` + let Y:! ForwardDeclaredConstraint(X); +} +constraint ForwardDeclaredConstraint(X:! MoveYsRight) { + extends MoveYsRight where .X = X.Y; +} +// ✅ The final type of `x` is `T.X.Y.Y`. It is computed as follows: +// The type of `T` is `MoveYsRight`. +// The type of `T.Y` is determined as follows: +// - Qualified name lookup finds `MoveYsRight.Y`. +// - The declared type is `ForwardDeclaredConstraint(Self.X)`. +// - That is a named constraint, for which we perform substitution. +// Substituting `X = Self.X` gives the type +// `MoveYsRight where .X = Self.X.Y`. +// - Substituting `Self = T` gives the type +// `MoveYsRight where .X = T.X.Y`. +// The type of `T.Y.Y` is determined as follows: +// - Qualified name lookup finds `MoveYsRight.Y`. +// - The declared type is `ForwardDeclaredConstraint(Self.X)`. +// - That is a named constraint, for which we perform substitution. +// Substituting `X = Self.X` gives the type +// `MoveYsRight where .X = Self.X.Y`. +// - Substituting `Self = T.Y` with +// rewrite `.X = T.X.Y` gives the type +// `MoveYsRight where .X = T.Y.X.Y`, but +// `T.Y.X` is replaced by `T.X.Y`, giving +// `MoveYsRight where .X = T.X.Y.Y`. +// The type of `T.Y.Y.X` is determined as follows: +// - Qualified name lookup finds `MoveYsRight.X`. +// - The type of `T.Y.Y` says to rewrite that to `T.X.Y.Y`. +// - The result is `T.X.Y.Y`, of type `MoveYsRight`. +fn F4(T:! MoveYsRight, x: T.Y.Y.X); +``` + +###### Termination + +Each of the above steps performs at most one rewrite, and doesn't introduce any +new recursive type-checking steps, so should not introduce any new forms of +non-termination. Rewrite constraints thereby give us a deterministic, +terminating type canonicalization mechanism for associated constants: in `A.B`, +if the type of `A` specifies that `.B = C`, then `A.B` is replaced by `C`. +Equality of types constrained in this way is transitive. + +However, some existing forms of non-termination may remain, such as template +instantiation triggering another template instantiation. Such cases will need to +be detected and handled in some way, such as by a depth limit, but doing so +doesn't compromise the soundness of the type system. + +#### Same-type constraints + +A same-type constraint describes that two type expressions are known to evaluate +to the same value. Unlike a [rewrite constraint](#rewrite-constraints), however, +the two type expressions are treated as distinct types when type-checking a +symbolic expression that refers to them. + +Same-type constraints are brought into scope, looked up, and resolved exactly as +if there were a `SameAs(U:! type)` interface and a `T == U` impl corresponded to +`T is SameAs(U)`, except that `==` is commutative. As such, it's not possible to +ask for a list of types that are the same as a given type, nor to ask whether +there exists a type that is the same as a given type and has some property. But +it is possible to ask whether two types are (non-transitively) known to be the +same. + +In order for same-type constraints to be useful, they must allow the two types +to be treated as actually being the same in some context. This can be +accomplished by the use of `==` constraints in an `impl`, such as in the +built-in implementation of `ImplicitAs`: -``` -let RealAbs:! auto = HasAbs where .MagnitudeType == .Self; -constraint RealAbs { - extend HasAbs where .MagnitudeType == Self; +```carbon +final impl forall [T:! type, U:! type where .Self == T] T as ImplicitAs(U) { + fn Convert[self: Self](other: U) -> U { ... } +} +``` + +> **Alternative considered:** It superficially seems like it would be convenient +> if such implementations were made available implicitly –- for example, by +> writing `impl forall [T:! type] T as ImplicitAs(T)` -– but in more complex +> examples that turns out to be problematic. Consider: +> +> ```carbon +> interface CommonTypeWith(U:! type) { +> let Result:! type; +> } +> final impl forall [T:! type] T as CommonTypeWith(T) where .Result = T {} +> +> fn F[T:! Potato, U:! Hashable where .Self == T](x: T, y: U) -> auto { +> // What is T.CommonTypeWith(U).Result? Is it T or U? +> return (if cond then x else y).Hash(); +> } +> ``` +> +> With this alternative, `impl` validation for `T as CommonTypeWith(U)` fails: +> we cannot pick a common type when given two distinct type expressions, even if +> we know they evaluate to the same type, because we would not know which API +> the result should have. + +##### Implementation of same-type `ImplicitAs` + +It is possible to implement the above `impl` of `ImplicitAs` directly in Carbon, +without a compiler builtin, by taking advantage of the built-in conversion +between `C where .A = X` and `C where .A == X`: + +```carbon +interface EqualConverter { + let T:! type; + fn Convert(t: T) -> Self; } -let ContainerIsSlice:! auto = - Container where .SliceType == .Self; -constraint ContainerIsSlice { - extend Container where .SliceType == Self; +fn EqualConvert[T:! type](t: T, U:! EqualConverter where .T = T) -> U { + return U.Convert(t); +} +impl forall [U:! type] U as EqualConverter where .T = U { + fn Convert(u: U) -> U { return u; } +} + +impl forall [T:! type, U:! type where .Self == T] T as ImplicitAs(U) { + fn Convert[self: Self]() -> U { return EqualConvert(self, U); } } ``` -Note that using the `constraint` approach we can name these constraints using -`Self` instead of `.Self`, since they refer to the same type. +The transition from `(T as ImplicitAs(U)).Convert`, where we know that `U == T`, +to `EqualConverter.Convert`, where we know that `.T = U`, allows a same-type +constraint to be used to perform a rewrite. -The `.Self` construct follows these rules: +##### Manual type equality -- `X :!` introduces `.Self:! type`, where references to `.Self` are resolved - to `X`. This allows you to use `.Self` as an interface parameter as in - `X:! I(.Self)`. -- `A where` introduces `.Self:! A` and `.Foo` for each member `Foo` of `A` -- It's an error to reference `.Self` if it refers to more than one different - thing or isn't a type. -- You get the innermost, most-specific type for `.Self` if it is introduced - twice in a scope. By the previous rule, it is only legal if they all refer - to the same generic parameter. +A same-type constraint establishes +[type expressions](terminology.md#type-expression) are equal, and allows +implicit conversions between them. However, determining whether two type +expressions are _transitively_ equal is in general undecidable, as +[has been shown in Swift](https://forums.swift.org/t/swift-type-checking-is-undecidable/39024). -So in `X:! A where ...`, `.Self` is introduced twice, after the `:!` and the -`where`. This is allowed since both times it means `X`. After the `:!`, `.Self` -has the type `type`, which gets refined to `A` after the `where`. In contrast, -it is an error if `.Self` could mean two different things, as in: +Carbon does not combine these equalities between type expressions. This means +that if two type expressions are only transitively equal, the user will need to +include a sequence of casts or use an +[`observe` declaration](#observe-declarations) to convert between them. + +Given this interface `Transitive` that has associated facets that are +constrained to all be equal, with interfaces `P`, `Q`, and `R`: + +```carbon +interface P { fn InP[self: Self](); } +interface Q { fn InQ[self: Self](); } +interface R { fn InR[self: Self](); } + +interface Transitive { + let A:! P; + let B:! Q where .Self == A; + let C:! R where .Self == B; + fn GetA[self: Self]() -> A; + fn TakesC[self: Self](c: C); +} ``` -// ❌ Illegal: `.Self` could mean `T` or `T.A`. -fn F[T:! InterfaceA where .A impls - (InterfaceB where .B == .Self)](x: T); + +A cast to `B` is needed to call `TakesC` with a value of type `A`, so each step +only relies on one equality: + +```carbon +fn F[T:! Transitive](t: T) { + // ✅ Allowed + t.TakesC(t.GetA() as T.B); + + // ✅ Allowed + let b: T.B = t.GetA(); + t.TakesC(b); + + // ❌ Not allowed: t.TakesC(t.GetA()); +} ``` -#### Parameterized type implements interface +The compiler may have several different `where` clauses to consider, +particularly when an interface has associated facets that recursively satisfy +the same interface. For example, given this interface `Commute`: + +```carbon +interface Commute { + let X:! Commute; + // **FIXME: Not allowed (at least not by Explorer) + // since `Commute` is incomplete here.** + let Y:! Commute where .X == X.Y; + + fn GetX[self: Self]() -> X; + fn GetY[self: Self]() -> Y; + fn TakesXXY[self: Self](xxy: X.X.Y); +} -There are times when a function will pass a generic type parameter of the -function as an argument to a parameterized type, as in the previous case, and in -addition the function needs the result to implement a specific interface. +// **FIXME: Maybe the following?** +interface Commute; +constraint Helper(T:! Commute); +interface Commute { + let X:! Commute; + let Y:! Helper(X); + + fn GetX[self: Self]() -> X; + fn GetY[self: Self]() -> Y; + // **FIXME: Don't think it is legal to write `X.X.Y` here.** + fn TakesXXY[self: Self](xxy: X.X.Y); +} + +constraint Helper(T:! Commute) { + extend Commute where .X == T.Y; +} ``` -// Some parameterized type. -class Vector(T:! type) { ... } -// Parameterized type implements interface only for some arguments. -impl Vector(String) as Printable { ... } +and a function `H` taking a value with some type implementing this interface, +then the following would be legal statements in `H`: -// Constraint: `T` such that `Vector(T)` implements `Printable` -fn PrintThree - [T:! type where Vector(.Self) impls Printable] - (a: T, b: T, c: T) { - var v: Vector(T) = (a, b, c); - Print(v); +```carbon +fn H[C: Commute](c: C) { + // ✅ Legal: argument has type `C.X.X.Y` + c.TakesXXY(c.GetX().GetX().GetY()); + + // ✅ Legal: argument has type `C.X.Y.X` which is equal + // to `C.X.X.Y` following only one `where` clause. + c.TakesXXY(c.GetX().GetY().GetX()); + + // ✅ Legal: cast is legal since it matches a `where` + // clause, and produces an argument that has type + // `C.X.Y.X`. + c.TakesXXY(c.GetY().GetX().GetX() as C.X.Y.X); } ``` -**Comparison with other languages:** This use case was part of the -[Rust rationale for adding support for `where` clauses](https://rust-lang.github.io/rfcs/0135-where.html#motivation). +That last call would not be legal without the cast, though. -#### Another type implements parameterized interface +**Comparison with other languages:** Other languages such as Swift and Rust +instead perform automatic type equality. In practice this means that their +compiler can reject some legal programs based on heuristics simply to avoid +running for an unbounded length of time. -In this case, we need some other type to implement an interface parameterized by -a generic type parameter. The syntax for this case follows the previous case, -except now the `.Self` parameter is on the interface to the right of the -`impls`. For example, we might need a type parameter `T` to support explicit -conversion from an integer type like `i32`: +The benefits of the manual approach include: + +- fast compilation, since the compiler does not need to explore a potentially + large set of combinations of equality restrictions, supporting + [Carbon's goal of fast and scalable development](/docs/project/goals.md#fast-and-scalable-development); +- expressive and predictable semantics, since there are no limitations on how + complex a set of constraints can be supported; and +- simplicity. + +The main downsides are: +- manual work for the source code author to prove to the compiler that types + are equal; and +- verbosity. + +We expect that rich error messages and IDE tooling will be able to suggest +changes to the source code when a single equality constraint is not sufficient +to show two type expressions are equal, but a more extensive automated search +can find a sequence that prove they are equal. + +##### Observe declarations + +Same-type constraints are non-transitive, just like `ImplicitAs`. The developer +can use an `observe` declaration to bring a new same-type constraint into scope: + +```carbon +observe A == B == C; ``` -interface As(T:! type) { - fn Convert[self: Self]() -> T; + +notionally does much the same thing as + +```carbon +impl A as SameAs(C) { ... } +``` + +where the `impl` makes use of `A is SameAs(B)` and `B is SameAs(C)`. + +In general, an `observe` declaration lists a sequence of +[type expressions](terminology.md#type-expression) that are equal by some +same-type `where` constraints. These `observe` declarations may be included in +an `interface` definition or a function body, as in: + +```carbon +// **FIXME: Not clear how to fix this example.** +interface Commute { + let X:! Commute; + let Y:! Commute where .X == X.Y; + ... + observe X.X.Y == X.Y.X == Y.X.X; } -fn Double[T:! Mul where i32 impls As(.Self)](x: T) -> T { - return x * (2 as T); +fn H[C: Commute](c: C) { + observe C.X.Y.Y == C.Y.X.Y == C.Y.Y.X; + ... } ``` -### Constraints must use a designator +Every type expression after the first must be equal to some earlier type +expression in the sequence by a single `where` equality constraint. In this +example, -We don't allow a `where` constraint unless it applies a restriction to the -current type. This means referring to some -[designator](#set-an-associated-constant-to-a-specific-value), like -`.MemberName`, or [`.Self`](#recursive-constraints). Examples: +```carbon +// **FIXME: Not clear how to fix this example.** +interface Commute { + let X:! Commute; + let Y:! Commute where .X == X.Y; + ... + // ✅ Legal: + observe X.X.Y.Y == X.Y.X.Y == Y.X.X.Y == X.Y.Y.X; +} +``` -- `Container where .ElementType = i32` -- `type where Vector(.Self) impls Sortable` -- `Addable where i32 impls AddableWith(.Result)` +the expression `X.Y.Y.X` is one equality away from `X.Y.X.Y` and so it is +allowed. This is even though `X.Y.X.Y` isn't the type expression immediately +prior to `X.Y.Y.X`. -Constraints that only refer to other types should be moved to the type that is -declared last. So: +After an `observe` declaration, all of the listed type expressions are +considered equal to each other using a single `where` equality. In this example, +the `observe` declaration in the `Transitive` interface definition provides the +link between associated facets `A` and `C` that allows function `F` to type +check. ```carbon -// ❌ Error: `where A == B` does not use `.Self` or a designator -fn F[A:! type, B:! type, C:! type where A == B](a: A, b: B, c: C); +interface P { fn InP[self: Self](); } +interface Q { fn InQ[self: Self](); } +interface R { fn InR[self: Self](); } + +interface Transitive { + let A:! P; + let B:! Q where .Self == A; + let C:! R where .Self == B; + + fn GetA[self: Self]() -> A; + fn TakesC[self: Self](c: C); + + // Without this `observe` declaration, the + // calls in `F` below would not be allowed. + observe A == B == C; +} + +fn F[T:! Transitive](t: T) { + var a: T.A = t.GetA(); + + // ✅ Allowed: `T.A` values implicitly convert to + // `T.C` using `observe` in interface definition. + t.TakesC(a); + + // ✅ Allowed: `T.C` extends and implements `R`. + (a as T.C).InR(); +} ``` -must be replaced by: +Only the current type is searched for interface implementations, so the call to +`InR()` would be illegal without the cast. However, an +[`observe`...`==`...`impls` declaration](#observing-equal-to-a-type-implementing-an-interface) +can be used to identify interfaces that must be implemented through some equal +type. This does not [extending](terminology.md#extending-an-impl) the API of the +type, that is solely determined by the definition of the type. Continuing the +previous example: ```carbon -// ✅ Allowed -fn F[A:! type, B:! type where A == .Self, C:! type](a: A, b: B, c: C); -``` +fn TakesPQR[U:! P & Q & R](u: U); -This includes `where` clauses used in an `impl` declaration: +fn G[T:! Transitive](t: T) { + var a: T.A = t.GetA(); -``` -// ❌ Error: `where T impls B` does not use `.Self` or a designator -impl forall [T:! type] T as A where T impls B {} -// ✅ Allowed -impl forall [T:! type where .Self impls B] T as A {} -// ✅ Allowed -impl forall [T:! B] T as A {} + // ✅ Allowed: `T.A` implements `P` and + // includes its API, as if it extends `P`. + a.InP(); + + // ❌ Illegal: only the current type is + // searched for interface implementations. + a.(Q.InQ()); + + // ✅ Allowed: values of type `T.A` may be cast + // to `T.B`, which extends and implements `Q`. + (a as T.B).InQ(); + + // ✅ Allowed: `T.A` == `T.B` that implements `Q`. + observe T.A == T.B impls Q; + a.(Q.InQ()); + + // ❌ Illegal: `T.A` still does not extend `Q`. + a.InQ(); + + // ✅ Allowed: `T.A` implements `P`, + // `T.A` == `T.B` that implements `Q` (observe above), + // and `T.A` == `T.C` that implements `R`. + observe T.A == T.C impls R; + TakesPQR(a); +} ``` -This clarifies the meaning of the `where` clause and reduces the number of -redundant ways to express a restriction, following the -[one-way principle](/docs/project/principles/one_way.md). +Since adding an `observe`...`impls` declaration only adds non-extending +implementations of interfaces to symbolic facets, they may be added without +breaking existing code. -**Alternative considered:** This rule was added in proposal -[#2376](https://github.com/carbon-language/carbon-lang/pull/2376), which -[considered whether this rule should be added](/proposals/p2376.md#alternatives-considered). +#### Implements constraints -### Implied constraints +An _implements constraint_ is written `where T impls C`, and expresses that the +facet `T` must implement the requirements of facet type `C`. This is more +flexible than using +[`&` to add a constraint](#combining-interfaces-by-anding-facet-types) since it +can be applied to [associated facet](#associated-facets) members as well. + +In the following example, normally the `ElementType` of a `Container` can be any +type. The `SortContainer` function, however, takes a pointer to a type +satisfying `Container` with the additional constraint that its `ElementType` +must satisfy the `Ordered` interface, using an `impls` constraint: -Imagine we have a generic function that accepts an arbitrary `HashMap`: +```carbon +interface Container { + let ElementType:! type; + ... +} +fn SortContainer + [ContainerType:! Container where .ElementType impls Ordered] + (container_to_sort: ContainerType*); ``` -fn LookUp[KeyType:! type](hm: HashMap(KeyType, i32)*, - k: KeyType) -> i32; -fn PrintValueOrDefault[KeyType:! Printable, +In contrast to a [rewrite constraint](#rewrite-constraints) or a +[same-type constraint](#same-type-constraints), this does not say what type +`ElementType` exactly is, just that it must satisfy requirements of some facet +type. + +> **Note:** `Container` defines `ElementType` as having type `type`, but +> `ContainerType.ElementType` has type `Ordered`. This is because +> `ContainerType` has type `Container where .ElementType impls Ordered`, not +> `Container`. This means we need to be a bit careful when talking about the +> type of `ContainerType` when there is a `where` clause modifying it. + +An implements constraint can be applied to [`.Self`](#recursive-constraints), as +in `I where .Self impls C`. This has the same requirements as `I & C`, but that +`where` clause does not affect the API. This means that a +[symbolic facet binding](#symbolic-facet-bindings) with that facet type, so `T` +in `T:! I where .Self impls C`, is represented by an +[archetype](terminology.md#archetype) that implements both `I` and `C`, but only +[extends](terminology.md#extending-an-impl) `I`. + +##### Implied constraints + +Imagine we have a checked-generic function that accepts an arbitrary +[`HashMap` parameterized type](#parameterized-types): + +```carbon +fn LookUp[KeyT:! type](hm: HashMap(KeyT, i32)*, + k: KeyT) -> i32; + +fn PrintValueOrDefault[KeyT:! Printable, ValueT:! Printable & HasDefault] - (map: HashMap(KeyType, ValueT), key: KeyT); + (map: HashMap(KeyT, ValueT), key: KeyT); ``` -The `KeyType` in these declarations does not visibly satisfy the requirements of +The `KeyT` in these declarations does not visibly satisfy the requirements of `HashMap`, which requires the type implement `Hashable` and other interfaces: -``` +```carbon class HashMap( - KeyType:! Hashable & EqualityComparable & Movable, + KeyT:! Hashable & Eq & Movable, ...) { ... } ``` -In this case, `KeyType` gets `Hashable` and so on as _implied constraints_. +In this case, `KeyT` gets `Hashable` and so on as _implied constraints_. Effectively that means that these functions are automatically rewritten to add a -`where` constraint on `KeyType` attached to the `HashMap` type: +`where .Self impls` constraint on `KeyT`: -``` -fn LookUp[KeyType:! type] - (hm: HashMap(KeyType, i32)* - where KeyType impls Hashable & EqualityComparable & Movable, - k: KeyType) -> i32; +```carbon +fn LookUp[ + KeyT:! type + where .Self impls Hashable & Eq & Movable] + (hm: HashMap(KeyT, i32)*, k: KeyT) -> i32; -fn PrintValueOrDefault[KeyType:! Printable, - ValueT:! Printable & HasDefault] - (map: HashMap(KeyType, ValueT) - where KeyType impls Hashable & EqualityComparable & Movable, - key: KeyT); +fn PrintValueOrDefault[ + KeyT:! Printable + where .Self impls Hashable & Eq & Movable, + ValueT:! Printable & HasDefault] + (map: HashMap(KeyT, ValueT), key: KeyT); ``` In this case, Carbon will accept the definition and infer the needed constraints -on the generic type parameter. This is both more concise for the author of the +on the symbolic facet parameter. This is both more concise for the author of the code and follows the ["don't repeat yourself" principle](https://en.wikipedia.org/wiki/Don%27t_repeat_yourself). This redundancy is undesirable since it means if the needed constraints for @@ -3017,15 +3758,15 @@ will have already satisfied these constraints. This implied constraint is equivalent to the explicit constraint that each parameter and return type [is legal](#must-be-legal-type-argument-constraints). -**Note:** These implied constraints affect the _requirements_ of a generic type -parameter, but not its _member names_. This way you can always look at the -declaration to see how name resolution works, without having to look up the -definitions of everything it is used as an argument to. +> **Note:** These implied constraints affect the _requirements_ of a symbolic +> facet parameter, but not its _member names_. This way you can always look at +> the declaration to see how name resolution works, without having to look up +> the definitions of everything it is used as an argument to. **Limitation:** To limit readability concerns and ambiguity, this feature is limited to a single signature. Consider this interface declaration: -``` +```carbon interface GraphNode { let Edge:! type; fn EdgesFrom[self: Self]() -> HashSet(Edge); @@ -3039,7 +3780,7 @@ say that the `EdgesFrom` would only be conditionally available when `Edge` does satisfy the constraints on `HashSet` arguments. Instead, Carbon will reject this definition, requiring the user to include all the constraints required for the other declarations in the interface in the declaration of the `Edge` associated -type. Similarly, a parameter to a class must be declared with all the +facet. Similarly, a parameter to a class must be declared with all the constraints needed to declare the members of the class that depend on that parameter. @@ -3051,306 +3792,407 @@ and support some form of this feature as part of their type inference (and [the Rust community is considering expanding support](http://smallcultfollowing.com/babysteps//blog/2022/04/12/implied-bounds-and-perfect-derive/#expanded-implied-bounds)). -#### Must be legal type argument constraints - -Now consider the case that the generic type parameter is going to be used as an -argument to a parameterized type in a function body, not in the signature. If -the parameterized type was explicitly mentioned in the signature, the implied -constraint feature would ensure all of its requirements were met. The developer -can create a trivial -[parameterized type implements interface](#parameterized-type-implements-interface) -`where` constraint to just say the type is a legal with this argument, by saying -that the parameterized type implements `type`, which all types do. +#### Combining constraints -For example, a function that adds its parameters to a `HashSet` to deduplicate -them, needs them to be `Hashable` and so on. To say "`T` is a type where -`HashSet(T)` is legal," we can write: +Constraints can be combined by separating constraint clauses with the `and` +keyword. This example expresses a constraint that two associated facets are +equal and satisfy an interface: -``` -fn NumDistinct[T:! type where HashSet(.Self) impls type] - (a: T, b: T, c: T) -> i32 { - var set: HashSet(T); - set.Add(a); - set.Add(b); - set.Add(c); - return set.Size(); -} +```carbon +fn EqualContainers + [CT1:! Container, + CT2:! Container where .ElementType impls HasEquality + and .ElementType = CT1.ElementType] + (c1: CT1*, c2: CT2*) -> bool; ``` -This has the same advantages over repeating the constraints on `HashSet` -arguments in the type of `T` as the general implied constraints above. +**Comparison with other languages:** Swift and Rust use commas `,` to separate +constraint clauses, but that only works because they place the `where` in a +different position in a declaration. In Carbon, the `where` is attached to a +type in a parameter list that is already using commas to separate parameters. -### Referencing names in the interface being defined +### Satisfying both facet types -The constraint in a `where` clause is required to only reference earlier names -from this scope, as in this example: +If the two facet bindings being constrained to be equal, using either a +[rewrite constraint](#rewrite-constraints) or a +[same-type constraint](#same-type-constraints), have been declared with +different facet types, then the actual type value they are set to will have to +satisfy the requirements of both facet types. For example, if +`SortedContainer.ElementType` is declared to have a `Ordered` requirement, then +in these declarations: -``` -interface Graph { - let E: Edge; - let V: Vert where .E == E and .Self == E.V; -} +```carbon +// With `=` rewrite constraint: +fn Contains_Rewrite + [SC:! SortedContainer, + CT:! Container where .ElementType = SC.ElementType] + (haystack: SC, needles: CT) -> bool; + +// With `==` same-type constraint: +fn Contains_SameType + [SC:! SortedContainer, + CT:! Container where .ElementType == SC.ElementType] + (haystack: SC, needles: CT) -> bool; ``` -### Manual type equality +the `where` constraints in both cases mean `CT.ElementType` must satisfy +`Ordered` as well. However, the behavior inside the body of these two inside the +body of the two functions is different. -Imagine we have some function with generic parameters: +In `Contains_Rewrite`, `CT.ElementType` is rewritten to `SC.ElementType` and +uses the facet type of `SC.ElementType`. +In `Contains_SameType`, the `where` clause does not affect the API of +`CT.ElementType`, and it would not even be considered to implement `Ordered` +unless there is some declaration like +`observe CT.ElementType == SC.ElementType impls Ordered`. Even then, the items +from the `needles` container won't directly have a `Compare` method member. + +The rule is that an same-type `where` constraint between two type variables does +not modify the set of member names of either type. This is in contrast to +rewrite constraints like `where .ElementType = String` with a `=`, then +`.ElementType` is actually set to `String` including the complete `String` API. + +Note that `==` constraints are symmetric, so the previous declaration of +`Contains_SameType` is equivalent to an alternative declaration where `CT` is +declared first and the `where` clause is attached to `SortedContainer`: + +```carbon +fn Contains_SameType_Equivalent + [CT:! Container, + SC:! SortedContainer where .ElementType == CT.ElementType] + (haystack: SC, needles: CT) -> bool; ``` -fn F[T:! SomeInterface](x: T) { - x.G(x.H()); -} + +### Constraints must use a designator + +We don't allow a `where` constraint unless it applies a restriction to the +current type. This means referring to some +[designator](#kinds-of-where-constraints), like `.MemberName`, or +[`.Self`](#recursive-constraints). Examples: + +- `Container where .ElementType = i32` +- `type where Vector(.Self) impls Sortable` +- `Addable where i32 impls AddableWith(.Result)` + +Constraints that only refer to other types should be moved to the type that is +declared last. So: + +```carbon +// ❌ Error: `where A == B` does not use `.Self` or a designator +fn F[A:! type, B:! type, C:! type where A == B](a: A, b: B, c: C); ``` -We want to know if the return type of method `T.H` is the same as the parameter -type of `T.G` in order to typecheck the function. However, determining whether -two type expressions are transitively equal is in general undecidable, as -[has been shown in Swift](https://forums.swift.org/t/swift-type-checking-is-undecidable/39024). +must be replaced by: -Carbon's approach is to only allow implicit conversions between two type -expressions that are constrained to be equal in a single where clause. This -means that if two type expressions are only transitively equal, the user will -need to include a sequence of casts or use an -[`observe` declaration](#observe-declarations) to convert between them. +```carbon +// ✅ Allowed +fn F[A:! type, B:! type where A == .Self, C:! type](a: A, b: B, c: C); +``` -Given this interface `Transitive` that has associated types that are constrained -to all be equal, with interfaces `P`, `Q`, and `R`: +This includes `where` clauses used in an `impl` declaration: +```carbon +// ❌ Error: `where T impls B` does not use `.Self` or a designator +impl forall [T:! type] T as A where T impls B {} +// ✅ Allowed +impl forall [T:! type where .Self impls B] T as A {} +// ✅ Allowed +impl forall [T:! B] T as A {} ``` -interface P { fn InP[self: Self](); } -interface Q { fn InQ[self: Self](); } -interface R { fn InR[self: Self](); } -interface Transitive { - let A:! P; - let B:! Q where .Self == A; - let C:! R where .Self == B; +This clarifies the meaning of the `where` clause and reduces the number of +redundant ways to express a restriction, following the +[one-way principle](/docs/project/principles/one_way.md). + +**Alternative considered:** This rule was added in proposal +[#2376](https://github.com/carbon-language/carbon-lang/pull/2376), which +[considered whether this rule should be added](/proposals/p2376.md#alternatives-considered). + +### Referencing names in the interface being defined + +The constraint in a `where` clause is required to only reference earlier names +from this scope, as in this example: + +```carbon +// ❌ Illegal: `E` references `V` declared later. +interface Graph { + let E: Edge where .V = V; + let V: Vert where .E = E; +} - fn GetA[self: Self]() -> A; - fn TakesC[self: Self](c: C); +// ✅ Allowed: Only references to earlier names. +interface Graph { + let E: Edge; + let V: Vert where .E = E and .Self == E.V; } ``` -A cast to `B` is needed to call `TakesC` with a value of type `A`, so each step -only relies on one equality: - -``` -fn F[T:! Transitive](t: T) { - // ✅ Allowed - t.TakesC(t.GetA() as T.B); +### Constraint examples and use cases - // ✅ Allowed - let b: T.B = t.GetA(); - t.TakesC(b); +- **Set [associated constant](#associated-constants) to a constant:** For + example in `NSpacePoint where .N = 2`, the associated constant `N` of + `NSpacePoint` must be `2`. This syntax is also used to specify the values of + associated constants when implementing an interface for a type, as in + `impl MyPoint as NSpacePoint where .N = 2 {`...`}`. - // ❌ Not allowed: t.TakesC(t.GetA()); -} -``` +- **Set an [associated facet](#associated-facets) to a specific value:** + Associated facets are treated like any other associated constant. So + `Stack where .ElementType = i32` is a facet type that restricts to types + that implement the `Stack` interface with integer elements, as in: -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#extending-an-impl). However, the -compiler will require a cast to `B` or `C` to see that the type implements `R`. + ```carbon + fn SumIntStack[T:! Stack where .ElementType = i32] + (s: T*) -> i32 { + var sum: i32 = 0; + while (!s->IsEmpty()) { + // s->Pop() returns a value of type + // `T.ElementType` which is `i32`: + sum += s->Pop(); + } + return sum; + } + ``` -``` -fn TakesPQR[U:! P & Q & R](u: U); + Note that this is a case that can use an `==` same-type constraint instead + of an `=` rewrite constraint. -fn G[T:! Transitive](t: T) { - var a: T.A = t.GetA(); +- **One [associated constant](#associated-constants) must equal another:** For + example with this definition of the interface `PointCloud`: - // ✅ Allowed: `T.A` implements `P`. - a.InP(); + ```carbon + interface PointCloud { + let Dim:! i32; + let PointT:! NSpacePoint where .N = Dim; + } + ``` - // ✅ Allowed: `T.A` implements `Q` externally. - a.(Q.InQ)(); + an implementation of `PointCloud` for a type `T` will have + `T.PointT.N == T.Dim`. - // ❌ Not allowed: a.InQ(); +- **Equal facet bindings:** - // ✅ Allowed: values of type `T.A` may be cast - // to `T.B`, which implements `Q` internally. - (a as T.B).InQ(); + For example, we could make the `ElementType` of an `Iterator` interface + equal to the `ElementType` of a `Container` interface as follows: - // ✅ Allowed: `T.B` implements `R` externally. - (a as T.B).(R.InR)(); + ```carbon + interface Iterator { + let ElementType:! type; + ... + } + interface Container { + let ElementType:! type; + let IteratorType:! Iterator where .ElementType = ElementType; + ... + } + ``` - // ❌ Not allowed: TakesPQR(a); + In a function signature, this may be done by referencing an earlier + parameter: - // ✅ Allowed: `T.B` implements `P`, `Q`, and - // `R`, though the implementations of `P` - // and `R` are external. - TakesPQR(a as T.B); -} -``` + ```carbon + fn Map[CT:! Container, + FT:! Function where .InputType = CT.ElementType] + (c: CT, f: FT) -> Vector(FT.OutputType); + ``` -The compiler may have several different `where` clauses to consider, -particularly when an interface has associated types that recursively satisfy the -same interface. For example, given this interface `Commute`: + In that example, `FT.InputType` is constrained to equal `CT.InputType`. + Given an interface with two associated facets -``` -interface Commute { - let X:! Commute; - let Y:! Commute where .X == X.Y; + ```carbon + interface PairInterface { + let Left:! type; + let Right:! type; + } + ``` - fn GetX[self: Self]() -> X; - fn GetY[self: Self]() -> Y; - fn TakesXXY[self: Self](xxy: X.X.Y); -} -``` + we can constrain them to be equal using + `PairInterface where .Left = .Right`. -and a function `H` taking a value with some type implementing this interface, -then the following would be legal statements in `H`: + Note that this is a case that can use an `==` same-type constraint instead + of an `=` rewrite constraint. -``` -fn H[C: Commute](c: C) { - // ✅ Legal: argument has type `C.X.X.Y` - c.TakesXXY(c.GetX().GetX().GetY()); +- **[Associated facet](#associated-facets) implements interface:** Given these + definitions (omitting `ElementType` for brevity): - // ✅ Legal: argument has type `C.X.Y.X` which is equal - // to `C.X.X.Y` following only one `where` clause. - c.TakesXXY(c.GetX().GetY().GetX()); + ```carbon + interface IteratorInterface { ... } + interface ContainerInterface { + let IteratorType:! IteratorInterface; + // ... + } + interface RandomAccessIterator { + extend IteratorInterface; + // ... + } + ``` - // ✅ Legal: cast is legal since it matches a `where` - // clause, and produces an argument that has type - // `C.X.Y.X`. - c.TakesXXY(c.GetY().GetX().GetX() as C.X.Y.X); -} -``` + We can then define a function that only accepts types that implement + `ContainerInterface` where its `IteratorType` associated facet implements + `RandomAccessIterator`: -That last call would not be legal without the cast, though. + ```carbon + fn F[ContainerType:! ContainerInterface + where .IteratorType impls RandomAccessIterator] + (c: ContainerType); + ``` -**Comparison with other languages:** Other languages such as Swift and Rust -instead perform automatic type equality. In practice this means that their -compiler can reject some legal programs based on heuristics simply to avoid -running for an unbounded length of time. +#### Parameterized type implements interface -The benefits of the manual approach include: +There are times when a function will pass a +[symbolic facet parameter](#symbolic-facet-bindings) of the function as an +argument to a [parameterized type](#parameterized-types), and the function needs +the result to implement a specific interface. -- fast compilation, since the compiler does not need to explore a potentially - large set of combinations of equality restrictions, supporting - [Carbon's goal of fast and scalable development](/docs/project/goals.md#fast-and-scalable-development); -- expressive and predictable semantics, since there are no limitations on how - complex a set of constraints can be supported; and -- simplicity. +```carbon +// A parameterized type +class Vector(T:! type) { ... } -The main downsides are: +// The parameterized type `Vector` implements interface +// `Printable` only for some arguments. +impl Vector(String) as Printable { ... } -- manual work for the source code author to prove to the compiler that types - are equal; and -- verbosity. +// Constraint: `T` such that `Vector(T)` implements `Printable` +fn PrintThree + [T:! type where Vector(.Self) impls Printable] + (a: T, b: T, c: T) { + var v: Vector(T) = (a, b, c); + Print(v); +} +``` -We expect that rich error messages and IDE tooling will be able to suggest -changes to the source code when a single equality constraint is not sufficient -to show two type expressions are equal, but a more extensive automated search -can find a sequence that prove they are equal. +**Comparison with other languages:** This use case was part of the +[Rust rationale for adding support for `where` clauses](https://rust-lang.github.io/rfcs/0135-where.html#motivation). -#### `observe` declarations +#### Another type implements parameterized interface -An `observe` declaration lists a sequence of type expressions that are equal by -some same-type `where` constraints. These `observe` declarations may be included -in an `interface` definition or a function body, as in: +In this case, we need some other type to implement an interface parameterized by +a [symbolic facet parameter](#symbolic-facet-bindings). The syntax for this case +follows the previous case, except now the `.Self` parameter is on the interface +to the right of the `impls`. For example, we might need a type parameter `T` to +support explicit conversion from an `i32`: -``` -interface Commute { - let X:! Commute; - let Y:! Commute where .X == X.Y; - ... - observe X.X.Y == X.Y.X == Y.X.X; +```carbon +interface As(T:! type) { + fn Convert[self: Self]() -> T; } -fn H[C: Commute](c: C) { - observe C.X.Y.Y == C.Y.X.Y == C.Y.Y.X; - ... +fn Double[T:! Mul where i32 impls As(.Self)](x: T) -> T { + return x * ((2 as i32) as T); } ``` -Every type expression after the first must be equal to some earlier type -expression in the sequence by a single `where` equality constraint. In this -example, +#### Must be legal type argument constraints -``` -interface Commute { - let X:! Commute; - let Y:! Commute where .X == X.Y; - ... - // ✅ Legal: - observe X.X.Y.Y == X.Y.X.Y == Y.X.X.Y == X.Y.Y.X; +Now consider the case that the symbolic facet parameter is going to be used as +an argument to a [parameterized type](#parameterized-types) in a function body, +but not in the signature. If the parameterized type was explicitly mentioned in +the signature, the [implied constraint](#implied-constraints) feature would +ensure all of its requirements were met. To say a parameterized type is allowed +to be passed a specific argument, just write that it `impls type`, which all +types do. This is a trivial case of a +[parameterized type implements interface](#parameterized-type-implements-interface) +`where` constraint. + +For example, a function that adds its parameters to a `HashSet` to deduplicate +them, needs them to be `Hashable` and so on. To say "`T` is a type where +`HashSet(T)` is legal," we can write: + +```carbon +fn NumDistinct[T:! type where HashSet(.Self) impls type] + (a: T, b: T, c: T) -> i32 { + var set: HashSet(T); + set.Add(a); + set.Add(b); + set.Add(c); + return set.Size(); } ``` -the expression `X.Y.Y.X` is one equality away from `X.Y.X.Y` and so it is -allowed. This is even though `X.Y.X.Y` isn't the type expression immediately -prior to `X.Y.Y.X`. +This has the same advantages over repeating the constraints on `HashSet` +arguments in the type of `T` as other +[implied constraints](#implied-constraints). -After an `observe` declaration, all of the listed type expressions are -considered equal to each other using a single `where` equality. In this example, -the `observe` declaration in the `Transitive` interface definition provides the -link between associated types `A` and `C` that allows function `F` to type -check. +### Named constraint constants -``` -interface P { fn InP[self: Self](); } -interface Q { fn InQ[self: Self](); } -interface R { fn InR[self: Self](); } +A facet type with a `where` constraint, such as `C where `, can be +named two different ways: -interface Transitive { - let A:! P; - let B:! Q where .Self == A; - let C:! R where .Self == B; +- Using `let template` as in: - fn GetA[self: Self]() -> A; - fn TakesC[self: Self](c: C); + ```carbon + let template NameOfConstraint:! auto = C where ; + ``` - // Without this `observe` declaration, the - // calls in `F` below would not be allowed. - observe A == B == C; -} + or, since the type of a facet type is `type`: -fn TakesPQR[U:! P & Q & R](u: U); + ```carbon + let template NameOfConstraint:! type = C where ; + ``` -fn F[T:! Transitive](t: T) { - var a: T.A = t.GetA(); +- Using a [named constraint](#named-constraints) with the `constraint` keyword + introducer: - // ✅ Allowed: `T.A` == `T.C` - t.TakesC(a); - a.(R.InR()); + ```carbon + constraint NameOfConstraint { + extend C where ; + } + ``` - // ✅ Allowed: `T.A` implements `P`, - // `T.A` == `T.B` that implements `Q`, and - // `T.A` == `T.C` that implements `R`. - TakesPQR(a); -} -``` +Whichever approach is used, the result is `NameOfConstraint` is a compile-time +constant that is equivalent to `C where `. -Since adding an `observe` declaration only adds external implementations of -interfaces to generic types, they may be added without breaking existing code. +## Other constraints as facet types -## Other constraints as type-of-types +There are some constraints that Carbon naturally represents as named facet +types. These can either be used directly to constrain a facet binding, or in a +`where ... impls ...` [implements constraint](#implements-constraints) to +constrain an associated facet. -There are some constraints that we will naturally represent as named -type-of-types. These can either be used directly to constrain a generic type -parameter, or in a `where ... impls ...` clause to constrain an associated type. +The compiler determines which types implement these interfaces, developers are +not permitted to explicitly implement these interfaces for their own types. -The compiler determines which types implement these interfaces, developers can -not explicitly implement these interfaces for their own types. +These facet types extend the requirements that facet types are allowed to +include beyond [interfaces implemented](#facet-types) and +[`where` clauses](#where-constraints). **Open question:** Are these names part of the prelude or in a standard library? ### Is a derived class -Given a type `T`, `Extends(T)` is a type-of-type whose values are types that are -derived from `T`. That is, `Extends(T)` is the set of all types `U` that are -subtypes of `T`. +Given a type `T`, `Extends(T)` is a facet type whose values are facets that are +(transitively) [derived from](/docs/design/classes.md#inheritance) `T`. That is, +`U:! Extends(T)` means `U` has an `extend base: T;` declaration, or there is a +chain of `extend base` declarations connecting `T` to `U`. + +```carbon +base class BaseType { ... } -``` fn F[T:! Extends(BaseType)](p: T*); -fn UpCast[T:! type](p: T*, U:! type where T impls Extends(.Self)) -> U*; -fn DownCast[T:! type](p: T*, U:! Extends(T)) -> U*; -``` +fn UpCast[U:! type] + (p: U*, V:! type where U impls Extends(.Self)) -> V*; +fn DownCast[X:! type](p: X*, Y:! Extends(X)) -> Y*; + +class DerivedType { + extend base: BaseType; +} +var d: DerivedType = {}; +// `T` is set to `DerivedType` +// `DerivedType impls Extends(BaseType)` +F(&d); -**Open question:** Alternatively, we could define a new `extends` operator: +// `U` is set to `DerivedType` +let p: BaseType* = UpCast(&d, BaseType); +// `X` is set to `BaseType` +// `Y` is set to facet `DerivedType as Extends(BaseType)`. +Assert(DownCast(p, DerivedType) == &d); ``` + +**Open question:** Alternatively, we could define a new `extends` operator for +use in `where` clauses: + +```carbon fn F[T:! type where .Self extends BaseType](p: T*); fn UpCast[T:! type](p: T*, U:! type where T extends .Self) -> U*; fn DownCast[T:! type](p: T*, U:! type where .Self extends T) -> U*; @@ -3361,25 +4203,23 @@ fn DownCast[T:! type](p: T*, U:! type where .Self extends T) -> U*; ### Type compatible with another type -Given a type `U`, define the type-of-type `CompatibleWith(U)` as follows: - -> `CompatibleWith(U)` is a type whose values are types `T` such that `T` and `U` -> are [compatible](terminology.md#compatible-types). That is values of types `T` -> and `U` can be cast back and forth without any change in representation (for -> example `T` is an [adapter](#adapting-types) for `U`). +Given a type `U`, define the facet type `CompatibleWith(U)` as follows: -To support this, we extend the requirements that type-of-types are allowed to -have to include a "data representation requirement" option. +> `CompatibleWith(U)` is a facet type whose values are facets `T` such that +> `T as type` and `U as type` are +> [compatible types](terminology.md#compatible-types). That is values of `T` and +> `U` as types can be cast back and forth without any change in representation +> (for example `T` is an [adapter](#adapting-types) for `U`). `CompatibleWith` determines an equivalence relationship between types. Specifically, given two types `T1` and `T2`, they are equivalent if -`T1 impls CompatibleWith(T2)`. That is, if `T1` has the type -`CompatibleWith(T2)`. +`T1 impls CompatibleWith(T2)`, which is true if and only if +`T2 impls CompatibleWith(T1)`. -**Note:** Just like interface parameters, we require the user to supply `U`, -they may not be deduced. Specifically, this code would be illegal: +**Note:** Just like interface parameters, we require the user to supply `U`, it +may not be deduced. Specifically, this code would be illegal: -``` +```carbon fn Illegal[U:! type, T:! CompatibleWith(U)](x: T*) ... ``` @@ -3387,7 +4227,7 @@ In general there would be multiple choices for `U` given a specific `T` here, and no good way of picking one. However, similar code is allowed if there is another way of determining `U`: -``` +```carbon fn Allowed[U:! type, T:! CompatibleWith(U)](x: U*, y: T*) ... ``` @@ -3396,37 +4236,37 @@ fn Allowed[U:! type, T:! CompatibleWith(U)](x: U*, y: T*) ... In some cases, we need to restrict to types that implement certain interfaces the same way as the type `U`. -> The values of type `CompatibleWith(U, TT)` are types satisfying -> `CompatibleWith(U)` that have the same implementation of `TT` as `U`. +> The values of facet type `CompatibleWith(U, C)` are facets satisfying +> `CompatibleWith(U)` that have the same implementation of `C` as `U`. For example, if we have a type `HashSet(T)`: -``` +```carbon class HashSet(T:! Hashable) { ... } ``` Then `HashSet(T)` may be cast to `HashSet(U)` if `T impls CompatibleWith(U, Hashable)`. The one-parameter interpretation of -`CompatibleWith(U)` is recovered by letting the default for the second `TT` -parameter be `type`. +`CompatibleWith(U)` is recovered by letting the default for the second parameter +(`C`) be `type`. #### Example: Multiple implementations of the same interface This allows us to represent functions that accept multiple implementations of the same interface for a type. -``` -enum CompareResult { Less, Equal, Greater } -interface Comparable { +```carbon +choice CompareResult { Less, Equal, Greater } +interface Ordered { fn Compare[self: Self](rhs: Self) -> CompareResult; } fn CombinedLess[T:! type](a: T, b: T, - U:! CompatibleWith(T) & Comparable, - V:! CompatibleWith(T) & Comparable) -> bool { + U:! CompatibleWith(T) & Ordered, + V:! CompatibleWith(T) & Ordered) -> bool { match ((a as U).Compare(b as U)) { - case CompareResult.Less => { return True; } - case CompareResult.Greater => { return False; } - case CompareResult.Equal => { + case .Less => { return True; } + case .Greater => { return False; } + case .Equal => { return (a as V).Compare(b as V) == CompareResult.Less; } } @@ -3435,52 +4275,54 @@ fn CombinedLess[T:! type](a: T, b: T, Used as: -``` +```carbon class Song { ... } -class SongByArtist { adapt Song; impl as Comparable { ... } } -class SongByTitle { adapt Song; impl as Comparable { ... } } -var s1: Song = ...; -var s2: Song = ...; +class SongByArtist { adapt Song; impl as Ordered { ... } } +class SongByTitle { adapt Song; impl as Ordered { ... } } +let s1: Song = ...; +let s2: Song = ...; assert(CombinedLess(s1, s2, SongByArtist, SongByTitle) == True); ``` -We might generalize this to a list of implementations: - -``` -fn CombinedCompare[T:! type] - (a: T, b: T, CompareList:! List(CompatibleWith(T) & Comparable)) - -> CompareResult { - for (let U:! auto in CompareList) { - var result: CompareResult = (a as U).Compare(b); - if (result != CompareResult.Equal) { - return result; - } - } - return CompareResult.Equal; -} - -assert(CombinedCompare(Song(...), Song(...), (SongByArtist, SongByTitle)) == - CompareResult.Less); -``` - -**Open question:** How are compile-time lists of types declared and iterated -through? They will also be needed for -[variadic argument support](#variadic-arguments). +> **Open question:** We might generalize this to a list of implementations using +> variadics: +> +> ```carbon +> fn CombinedCompare[T:! type] +> (a: T, b: T, ... each CompareT:! CompatibleWith(T) & Ordered) +> -> CompareResult { +> ... block { +> let result: CompareResult = +> (a as each CompareT).Compare(b as each CompareT); +> if (result != CompareResult.Equal) { +> return result; +> } +> } +> return CompareResult.Equal; +> } +> +> assert(CombinedCompare(s1, s2, SongByArtist, SongByTitle) +> == CompareResult.Less); +> ``` +> +> However, [variadic support](#variadic-arguments) is still future work. #### Example: Creating an impl out of other implementations -And then to package this functionality as an implementation of `Comparable`, we -combine `CompatibleWith` with [type adaptation](#adapting-types): +And then to package this functionality as an implementation of `Ordered`, we +combine `CompatibleWith` with [type adaptation](#adapting-types) and +[variadics](#variadic-arguments): -``` +```carbon class ThenCompare( T:! type, - CompareList:! List(CompatibleWith(T) & Comparable)) { + ... each CompareT:! CompatibleWith(T) & Ordered) { adapt T; - extend impl as Comparable { + extend impl as Ordered { fn Compare[self: Self](rhs: Self) -> CompareResult { - for (let U:! auto in CompareList) { - var result: CompareResult = (self as U).Compare(rhs as U); + ... block { + let result: CompareResult = + (self as each CompareT).Compare(rhs as each CompareT); if (result != CompareResult.Equal) { return result; } @@ -3490,23 +4332,23 @@ class ThenCompare( } } -let SongByArtistThenTitle: auto = - ThenCompare(Song, (SongByArtist, SongByTitle)); +let template SongByArtistThenTitle:! auto = + ThenCompare(Song, SongByArtist, SongByTitle); var s1: Song = ...; var s2: SongByArtistThenTitle = - Song(...) as SongByArtistThenTitle; + ({ ... } as Song) as SongByArtistThenTitle; assert((s1 as SongByArtistThenTitle).Compare(s2) == CompareResult.Less); ``` -### Sized types and type-of-types +### Sized types and facet types What is the size of a type? - It could be fully known and fixed at compile time -- this is true of primitive types (`i32`, `f64`, and so on), most [classes](/docs/design/classes.md), and most other concrete types. -- It could be known generically. This means that it will be known at codegen +- It could be known symbolically. This means that it will be known at codegen time, but not at type-checking time. - It could be dynamic. For example, it could be a [dynamic type](#runtime-type-fields), a slice, variable-sized type (such as @@ -3517,11 +4359,11 @@ What is the size of a type? essentially equivalent to having dynamic size. A type is called _sized_ if it is in the first two categories, and _unsized_ -otherwise. Note: something with size 0 is still considered "sized". The -type-of-type `Sized` is defined as follows: +otherwise. Note: something with size 0 is still considered "sized". The facet +type `Sized` is defined as follows: > `Sized` is a type whose values are types `T` that are "sized" -- that is the -> size of `T` is known, though possibly only generically. +> size of `T` is known, though possibly only symbolically Knowing a type is sized is a precondition to declaring variables of that type, taking values of that type as parameters, returning values of that type, and @@ -3529,12 +4371,9 @@ defining arrays of that type. Users will not typically need to express the `Sized` constraint explicitly, though, since it will usually be a dependency of some other constraint the type will need such as `Movable` or `Concrete`. -**Note:** The compiler will determine which types are "sized", this is not -something types will implement explicitly like ordinary interfaces. - Example: -``` +```carbon // In the Carbon standard library interface DefaultConstructible { // Types must be sized to be default constructible. @@ -3557,7 +4396,7 @@ fn F[T:! type](x: T*) { // T is unsized. var z: T; } -// T is sized, but its size is only known generically. +// T is sized, but its size is only known symbolically. fn G[T: DefaultConstructible](x: T*) { // ✅ Allowed: T is default constructible, which means sized. var y: T = T.Default(); @@ -3568,46 +4407,15 @@ var z: Name = Name.Default();; G(&z); ``` -**Open question:** Even if the size is fixed, it won't be known at the time of -compiling the generic function if we are using the dynamic strategy. Should we -automatically -[box]() -local variables when using the dynamic strategy? Or should we only allow -`MaybeBox` values to be instantiated locally? Or should this just be a case -where the compiler won't necessarily use the dynamic strategy? - -**Open question:** Should the `Sized` type-of-type expose an associated constant +**Open question:** Should the `Sized` facet type expose an associated constant with the size? So you could say `T.ByteSize` in the above example to get a -generic int value with the size of `T`. Similarly you might say `T.ByteStride` -to get the number of bytes used for each element of an array of `T`. - -### `TypeId` - -There are some capabilities every type can provide. For example, every type -should be able to return its name or identify whether it is equal to another -type. It is rare, however, for code to need to access these capabilities, so we -relegate these capabilities to an interface called `TypeId` that all types -automatically implement. This way generic code can indicate that it needs those -capabilities by including `TypeId` in the list of requirements. In the case -where no type capabilities are needed, for example the code is only manipulating -pointers to the type, you would write `T:! type` and get the efficiency of -`void*` but without giving up type safety. - -``` -fn SortByAddress[T:! type](v: Vector(T*)*) { ... } -``` - -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#extending-an-impl) for types to avoid -name pollution (`.TypeName`, `.TypeHash`, etc.) unless the function specifically -requests those capabilities? +symbolic integer value with the size of `T`. Similarly you might say +`T.ByteStride` to get the number of bytes used for each element of an array of +`T`. ### Destructor constraints -There are four type-of-types related to +There are four facet types related to [the destructors of types](/docs/design/classes.md#destructors): - `Concrete` types may be local or member variables. @@ -3617,7 +4425,7 @@ There are four type-of-types related to using the `UnsafeDelete` method on the correct `Allocator`, but it may be unsafe. The concerning case is deleting a pointer to a derived class through a pointer to its base class without a virtual destructor. -- `TrivialDestructor` types have empty destructors. This type-of-type may be +- `TrivialDestructor` types have empty destructors. This facet type may be used with [specialization](#lookup-resolution-and-specialization) to unlock specific optimizations. @@ -3632,34 +4440,86 @@ The facet types `Concrete`, `Deletable`, and `TrivialDestructor` all extend checked-generic function that both instantiates and deletes values of a type `T` would require `T` implement `Concrete & Deletable`. -Types are forbidden from explicitly implementing these type-of-types directly. +Types are forbidden from explicitly implementing these facet types directly. Instead they use [`destructor` declarations in their class definition](/docs/design/classes.md#destructors) -and the compiler uses them to determine which of these type-of-types are +and the compiler uses them to determine which of these facet types are implemented. -## Generic `let` +## Compile-time `let` A `let` statement inside a function body may be used to get the change in type -behavior of calling a generic function without having to introduce a function -call. +behavior of calling a checked-generic function without having to introduce a +function call. + +```carbon +fn SymbolicLet(...) { + ... + let T:! C = U; + X; + Y; + Z; +} +``` + +This introduces a symbolic constant `T` with type `C` and value `U`. This +implicitly includes an [`observe T == U;` declaration](#observe-declarations), +when `T` and `U` are facets, which allows values to implicitly convert from the +concrete type `U` to the erased type `T`, as in: + +```carbon +let x: i32 = 7; +let T:! Add = i32; +// ✅ Allowed to convert `i32` values to `T`. +let y: T = x; +``` +> **TODO:** The implied `observe` declaration is from question-for-leads issue +> [#996](https://github.com/carbon-language/carbon-lang/issues/996) and should +> be approved in a proposal. + +This makes the `SymbolicLet` function roughly equivalent to: + +```carbon +fn SymbolicLet(...) { + ... + fn Closure(T:! C where .Self == U) { + X; + Y; + Z; + } + Closure(U); +} ``` -fn F(...) { + +The `where .Self == U` modifier captures the `observe` declaration introduced by +the `let` (at the cost of changing the type of `T`). + +A symbolic `let` can be used to switch to the API of `C` when `U` does not +extend `C`, as an alternative to +[using an adapter](#use-case-accessing-interface-names), or to simplify inlining +of a generic function while preserving semantics. + +To get a template binding instead of symbolic binding, add the `template` +keyword before the binding pattern, as in: + +```carbon +fn TemplateLet(...) { ... - let T:! C = U; + let template T:! C = U; X; Y; Z; } ``` -gets rewritten to: +which introduces a template constant `T` with type `C` and value `U`. This is +roughly equivalent to: -``` -fn F(...) { +```carbon +fn TemplateLet(...) { ... - fn Closure(T:! C where .Self == U) { + fn Closure(template T:! C) { X; Y; Z; @@ -3668,37 +4528,52 @@ fn F(...) { } ``` -The `where .Self == U` modifier allows values to implicitly convert between type -`T`, the erased type, and type `U`, the concrete type. Note that implicit -conversion is -[only performed across a single `where` equality](#manual-type-equality). This -can be used to switch to the API of `C` when `U` does not extend `C`, as an -alternative to [using an adapter](#use-case-accessing-interface-names), or to -simplify inlining of a generic function while preserving semantics. +In this case, the `where .Self == U` modifier is superfluous. + +> **References:** +> +> - Proposal +> [#950: Generics details 6: remove facets #950](https://github.com/carbon-language/carbon-lang/pull/950) +> - Question-for-leads issue +> [#996: Generic `let` with `auto`?](https://github.com/carbon-language/carbon-lang/issues/996) ## Parameterized impl declarations -There are cases where an impl definition should apply to more than a single type -and interface combination. The solution is to parameterize the impl definition, -so it applies to a family of types, interfaces, or both. This includes: +There are cases where an `impl` definition should apply to more than a single +type and interface combination. The solution is to parameterize the `impl` +definition, so it applies to a family of types, interfaces, or both. This +includes: -- Declare an impl for a parameterized type, which may be external or declared - out-of-line. -- "Conditional conformance" where a parameterized type implements some +- Defining an `impl` that applies to multiple arguments to a + [parameterized type](#parameterized-types). +- _Conditional conformance_ where a parameterized type implements some interface if the parameter to the type satisfies some criteria, like implementing the same interface. -- "Blanket" impl declarations where an interface is implemented for all types - that implement another interface, or some other criteria beyond being a - specific type. -- "Wildcard" impl declarations where a family of interfaces are implemented +- _Blanket_ `impl` declarations where an interface is implemented for all + types that implement another interface, or some other criteria beyond being + a specific type. +- _Wildcard_ `impl` declarations where a family of interfaces are implemented for single type. +The syntax for an out-of-line parameterized `impl` declaration is: + + + + + +> `impl forall [`__`]` __ `as` +> _ [_ `where` _ ]_ `;` + + + +This may also be called a _generic `impl` declaration_. + ### Impl for a parameterized type -Interfaces may be implemented for a parameterized type. This can be done -lexically in the class' scope: +Interfaces may be implemented for a [parameterized type](#parameterized-types). +This can be done lexically in the class' scope: -``` +```carbon class Vector(T:! type) { impl as Iterable where .ElementType = T { ... @@ -3709,7 +4584,7 @@ class Vector(T:! type) { This is equivalent to naming the implementing type between `impl` and `as`, though this form is not allowed after `extend`: -``` +```carbon class Vector(T:! type) { impl Vector(T) as Iterable where .ElementType = T { ... @@ -3720,7 +4595,7 @@ class Vector(T:! type) { An out-of-line `impl` declaration must declare all parameters in a `forall` clause: -``` +```carbon impl forall [T:! type] Vector(T) as Iterable where .ElementType = T { ... @@ -3728,23 +4603,23 @@ impl forall [T:! type] Vector(T) as Iterable ``` The parameter for the type can be used as an argument to the interface being -implemented: +implemented, with or without `extend`: -``` -class HashMap(Key:! Hashable, Value:! type) { - extend impl as Has(Key) { ... } - extend impl as Contains(HashSet(Key)) { ... } +```carbon +class HashMap(KeyT:! Hashable, ValueT:! type) { + extend impl as Has(KeyT) { ... } + impl as Contains(HashSet(KeyT)) { ... } } ``` -or externally out-of-line: +or out-of-line the same `forall` parameter can be passed to both: -``` -class HashMap(Key:! Hashable, Value:! type) { ... } -impl forall [Key:! Hashable, Value:! type] - HashMap(Key, Value) as Has(Key) { ... } -impl forall [Key:! Hashable, Value:! type] - HashMap(Key, Value) as Contains(HashSet(Key)) { ... } +```carbon +class HashMap(KeyT:! Hashable, ValueT:! type) { ... } +impl forall [KeyT:! Hashable, ValueT:! type] + HashMap(KeyT, ValueT) as Has(KeyT) { ... } +impl forall [KeyT:! Hashable, ValueT:! type] + HashMap(KeyT, ValueT) as Contains(HashSet(KeyT)) { ... } ``` ### Conditional conformance @@ -3765,7 +4640,7 @@ interface when its element type satisfies the same interface: This may be done by specifying a more specific implementing type to the left of the `as` in the declaration: -``` +```carbon interface Printable { fn Print[self: Self](); } @@ -3785,9 +4660,9 @@ impl forall [T:! Printable] Vector(T) as Printable { ``` Note that no `forall` clause or type may be specified when declaring an `impl` -with the `extend` keyword: +with the [`extend`](#extend-impl) keyword: -``` +```carbon class Array(T:! type, template N:! i64) { // ❌ Illegal: nothing allowed before `as` after `extend impl`: extend impl forall [P:! Printable] Array(P, N) as Printable { ... } @@ -3800,7 +4675,7 @@ class Array(T:! type, template N:! i64) { Instead, the class can declare aliases to members of the interface. Those aliases will only be usable when the type implements the interface. -``` +```carbon class Array(T:! type, template N:! i64) { alias Print = Printable.Print; } @@ -3822,29 +4697,31 @@ var no_print: Array(Unprintable, 2) = ...; no_print.Print(); ``` -It is still legal to declare or define an external impl lexically inside the -class scope, as in: +It is legal to declare or define a conditional impl lexically inside the class +scope without `extend`, as in: -``` +```carbon class Array(T:! type, template N:! i64) { - // ✅ Allowed: external impl defined in class scope may use `forall` - // and may specify a type. + // ✅ Allowed: non-extending impl defined in class scope may + // use `forall` and may specify a type. impl forall [P:! Printable] Array(P, N) as Printable { ... } } ``` Inside the scope of this `impl` definition, both `P` and `T` refer to the same -type, but `P` has the type-of-type of `Printable` and so has a `Print` member. -The relationship between `T` and `P` is as if there was a `where P == T` clause. +type, but `P` has the facet type of `Printable` and so has a `Print` member. The +relationship between `T` and `P` is as if there was a +[`where P == T` clause](#same-type-constraints). -**TODO:** Need to resolve whether the `T` name can be reused, or if we require -that you need to use new names, like `P`, when creating new type variables. +**Open question:** Need to resolve whether the `T` name can be reused, or if we +require that you need to use new names, like `P`, when creating new type +variables. **Example:** Consider a type with two parameters, like `Pair(T, U)`. In this example, the interface `Foo(T)` is only implemented when the two types are equal. -``` +```carbon interface Foo(T:! type) { ... } class Pair(T:! type, U:! type) { ... } impl forall [T:! type] Pair(T, T) as Foo(T) { ... } @@ -3853,7 +4730,7 @@ impl forall [T:! type] Pair(T, T) as Foo(T) { ... } As before, you may also define the `impl` inline, but it may not be combined with the `extend` keyword: -``` +```carbon class Pair(T:! type, U:! type) { impl Pair(T, T) as Foo(T) { ... } } @@ -3862,7 +4739,7 @@ class Pair(T:! type, U:! type) { **Clarification:** The same interface may be implemented multiple times as long as there is no overlap in the conditions: -``` +```carbon class X(T:! type) { // ✅ Allowed: `X(T).F` consistently means `X(T).(Foo.F)` // even though that may have different definitions for @@ -3886,28 +4763,6 @@ can only mean one thing, regardless of `T`. but bans cases where there could be ambiguity from overlap. [Rust also supports conditional conformance](https://doc.rust-lang.org/rust-by-example/generics/where.html). -#### Conditional methods - -A method could be defined conditionally for a type by using a more specific type -in place of `Self` in the method declaration. For example, this is how to define -a vector type that only has a `Sort` method if its elements implement the -`Comparable` interface: - -``` -class Vector(T:! type) { - // `Vector(T)` has a `Sort()` method if `T` impls `Comparable`. - fn Sort[C:! Comparable, addr self: Vector(C)*](); -} -``` - -**Comparison with other languages:** In -[Rust](https://doc.rust-lang.org/book/ch10-02-traits.html#using-trait-bounds-to-conditionally-implement-methods) -this feature is part of conditional conformance. Swift supports conditional -methods using -[conditional extensions](https://docs.swift.org/swift-book/LanguageGuide/Generics.html#ID553) -or -[contextual where clauses](https://docs.swift.org/swift-book/LanguageGuide/Generics.html#ID628). - ### Blanket impl declarations A _blanket impl declaration_ is an `impl` declaration that could apply to more @@ -3917,13 +4772,13 @@ than one root type, so the `impl` declaration will use a type variable for the - Any type implementing `Ordered` should get an implementation of `PartiallyOrdered`. - ``` + ```carbon impl forall [T:! Ordered] T as PartiallyOrdered { ... } ``` - `T` implements `CommonType(T)` for all `T` - ``` + ```carbon impl forall [T:! type] T as CommonType(T) where .Result = T { } ``` @@ -3954,7 +4809,7 @@ of interfaces are implemented for a single `Self` type. For example, the `ImplicitAs(i32)`. The implementation would first convert `T` to `i32` and then add the `i32` to the `BigInt` value. -``` +```carbon class BigInt { impl forall [T:! ImplicitAs(i32)] as AddTo(T) { ... } } @@ -3971,7 +4826,7 @@ The different kinds of parameters to an `impl` declarations may be combined. For example, if `T` implements `As(U)`, then this implements `As(Optional(U))` for `Optional(T)`: -``` +```carbon impl forall [U:! type, T:! As(U)] Optional(T) as As(Optional(U)) { ... } ``` @@ -3980,22 +4835,22 @@ This has a wildcard parameter `U`, and a condition on parameter `T`. ### Lookup resolution and specialization -As much as possible, we want rules for where an impl is allowed to be defined -and for selecting which impl to use that achieve these three goals: +As much as possible, we want rules for where an `impl` is allowed to be defined +and for selecting which `impl` definition to use that achieve these three goals: - Implementations have coherence, as [defined in terminology](terminology.md#coherence). This is [a goal for Carbon](goals.md#coherence). More detail can be found in [this appendix with the rationale and alternatives considered](appendix-coherence.md). - Libraries will work together as long as they pass their separate checks. -- A generic function can assume that some impl will be successfully selected - if it can see an impl that applies, even though another more specific impl - may be selected. +- A checked-generic function can assume that some `impl` definition will be + successfully selected if it can see an `impl` declaration that applies, even + though another more specific `impl` definition may be selected. -For this to work, we need a rule that picks a single `impl` in the case where -there are multiple `impl` definitions that match a particular type and interface -combination. This is called _specialization_ when the rule is that most specific -implementation is chosen, for some definition of specific. +For this to work, we need a rule that picks a single `impl` definition in the +case where there are multiple `impl` definitions that match a particular type +and interface combination. This is called _specialization_ when the rule is that +most specific implementation is chosen, for some definition of "specific." #### Type structure of an impl declaration @@ -4003,21 +4858,21 @@ Given an impl declaration, find the type structure by deleting deduced parameters and replacing type parameters by a `?`. The type structure of this declaration: -``` +```carbon impl forall [T:! ..., U:! ...] Foo(T, i32) as Bar(String, U) { ... } ``` is: -``` +```carbon impl Foo(?, i32) as Bar(String, ?) ``` To get a uniform representation across different `impl` definitions, before type parameters are replaced the declarations are normalized as follows: -- For impl declarations lexically inline in a class definition, the type is - added between the `impl` and `as` keywords if the type is left out. +- For `impl` declarations that are lexically inline in a class definition, the + type is added between the `impl` and `as` keywords if the type is left out. - Pointer types `T*` are replaced with `Ptr(T)`. - The `extend` keyword is removed, if present. - The `forall` clause introducing type parameters is removed, if present. @@ -4033,11 +4888,12 @@ library depends on. #### Orphan rule -To achieve coherence, we need to ensure that any given impl can only be defined -in a library that must be imported for it to apply. Specifically, given a -specific type and specific interface, `impl` declarations that can match can -only be in libraries that must have been imported to name that type or -interface. This is achieved with the _orphan rule_. +To achieve [coherence](terminology.md#coherence), we need to ensure that any +given impl can only be defined in a library that must be imported for it to +apply. Specifically, given a specific type and specific interface, `impl` +declarations that can match can only be in libraries that must have been +imported to name that type or interface. This is achieved with the _orphan +rule_. **Orphan rule:** Some name from the type structure of an `impl` declaration must be defined in the same library as the `impl`, that is some name must be _local_. @@ -4058,9 +4914,9 @@ few goals: is actually used, avoiding [One Definition Rule (ODR)](https://en.wikipedia.org/wiki/One_Definition_Rule) problems. -- Every attempt to use an `impl` will see the exact same `impl`, making the - interpretation and semantics of code consistent no matter its context, in - accordance with the +- Every attempt to use an `impl` will see the exact same `impl` definition, + making the interpretation and semantics of code consistent no matter its + context, in accordance with the [low context-sensitivity principle](/docs/project/principles/low_context_sensitivity.md). - Allowing the `impl` to be defined with either the interface or the type partially addresses the @@ -4094,7 +4950,7 @@ implementation of that type for that interface. Given two different type structures of impl declarations matching a query, for example: -``` +```carbon impl Foo(?, i32) as Bar(String, ?) impl Foo(?, ?) as Bar(String, f32) ``` @@ -4112,66 +4968,80 @@ difference. Since at most one library can contain `impl` definitions with a given type structure, all `impl` definitions with a given type structure must be in the -same library. Furthermore by the [impl declaration access rules](#access), they -will be defined in the API file for the library if they could match any query -from outside the library. If there is more than one impl with that type +same library. Furthermore by the [`impl` declaration access rules](#access), +they will be defined in the API file for the library if they could match any +query from outside the library. If there is more than one `impl` with that type structure, they must be [defined](#implementing-interfaces) or [declared](#declaring-implementations) together in a prioritization block. Once -a type structure is selected for a query, the first impl in the prioritization -block that matches is selected. - -**Open question:** How are prioritization blocks written? A block starts with a -keyword like `match_first` or `impl_priority` and then a sequence of impl -declarations inside matching curly braces `{` ... `}`. - -``` -match_first { - // If T is Foo prioritized ahead of T is Bar - impl forall [T:! Foo] T as Bar { ... } - impl forall [T:! Baz] T as Bar { ... } -} -``` - -**Open question:** How do we pick between two different prioritization blocks -when they contain a mixture of type structures? There are three options: - -- Prioritization blocks implicitly define all non-empty intersections of - contained `impl` declarations, which are then selected by their type - structure. -- The compiler first picks the impl with the type pattern most favored for the - query, and then picks the definition of the highest priority matching impl - in the same prioritization block. -- All the `impl` declarations in a prioritization block are required to have - the same type structure, at a cost in expressivity. - -To see the difference between the first two options, consider two libraries with -type structures as follows: - -- Library B has `impl (A, ?, ?, D) as I` and `impl (?, B, ?, D) as I` in the - same prioritization block. -- Library C has `impl (A, ?, C, ?) as I`. - -For the query `(A, B, C, D) as I`, using the intersection rule, library B is -considered to have the intersection impl with type structure -`impl (A, B, ?, D) as I` which is the most specific. If we instead just -considered the rules mentioned explicitly, then `impl (A, ?, C, ?) as I` from -library C is the most specific. The advantage of the implicit intersection rule -is that if library B is changed to add an impl with type structure -`impl (A, B, ?, D) as I`, it won't shift which library is serving that query. +a type structure is selected for a query, the first `impl` declaration in the +prioritization block that matches is selected. + +> **Open question:** How are prioritization blocks written? A block starts with +> a keyword like `match_first` or `impl_priority` and then a sequence of impl +> declarations inside matching curly braces `{` ... `}`. +> +> ```carbon +> match_first { +> // If T is Foo prioritized ahead of T is Bar +> impl forall [T:! Foo] T as Bar { ... } +> impl forall [T:! Baz] T as Bar { ... } +> } +> ``` + +To increase expressivity, Carbon allows prioritization blocks to contain a mix +of type structures, which is resolved using this rule: + +> The compiler first picks the `impl` declaration with the type structure most +> favored for the query, and then picks the highest priority (earliest) matching +> `impl` declaration in the same prioritization block. + +> **Alternatives considered:** We considered two other options: +> +> - "Intersection rule:" Prioritization blocks implicitly define all non-empty +> intersections of contained `impl` declarations, which are then selected by +> their type structure. +> - "Same type structure rule:" All the `impl` declarations in a +> prioritization block are required to have the same type structure, at a +> cost in expressivity. This option was not chosen since it wouldn't support +> the different type structures created by the +> [`like` operator](#like-operator-for-implicit-conversions). +> +> To see the difference from the first option, consider two libraries with type +> structures as follows: +> +> - Library B has `impl (A, ?, ?, D) as I` and `impl (?, B, ?, D) as I` in the +> same prioritization block. +> - Library C has `impl (A, ?, C, ?) as I`. +> +> For the query `(A, B, C, D) as I`, using the intersection rule, library B is +> considered to have the intersection impl with type structure +> `impl (A, B, ?, D) as I` which is the most specific. If we instead just +> considered the rules mentioned explicitly, then `impl (A, ?, C, ?) as I` from +> library C is the most specific. The advantage of the implicit intersection +> rule is that if library B is changed to add an impl with type structure +> `impl (A, B, ?, D) as I`, it won't shift which library is serving that query. +> Ultimately we decided that it was too surprising to prioritize based on the +> implicit intersection of `impl` declarations, rather than something explicitly +> written in the code. +> +> We chose between these alternatives in +> [the open discussion on 2023-07-18](https://docs.google.com/document/d/1gnJBTfY81fZYvI_QXjwKk1uQHYBNHGqRLI2BS_cYYNQ/edit?resourcekey=0-ql1Q1WvTcDvhycf8LbA9DQ#heading=h.7jxges9ojgy3). +> **TODO:** This decision needs to be approved in a proposal. #### Acyclic rule A cycle is when a query, such as "does type `T` implement interface `I`?", -considers an impl that might match, and whether that impl matches is ultimately -dependent on whether that query is true. These are cycles in the graph of (type, -interface) pairs where there is an edge from pair A to pair B if whether type A -implements interface A determines whether type B implements interface B. +considers an `impl` declaration that might match, and whether that `impl` +declaration matches is ultimately dependent on whether that query is true. These +are cycles in the graph of (type, interface) pairs where there is an edge from +pair A to pair B if whether type A implements interface A determines whether +type B implements interface B. The test for whether something forms a cycle needs to be precise enough, and not erase too much information when considering this graph, that these `impl` declarations are not considered to form cycles with themselves: -``` +```carbon impl forall [T:! Printable] Optional(T) as Printable; impl forall [T:! type, U:! ComparableTo(T)] U as ComparableTo(Optional(T)); ``` @@ -4179,7 +5049,7 @@ impl forall [T:! type, U:! ComparableTo(T)] U as ComparableTo(Optional(T)); **Example:** If `T` implements `ComparableWith(U)`, then `U` should implement `ComparableWith(T)`. -``` +```carbon impl forall [U:! type, T:! ComparableWith(U)] U as ComparableWith(T); ``` @@ -4191,7 +5061,7 @@ types implement the same interface. selecting `impl` declarations that are inconsistent with each other. Consider an interface with two blanket `impl` declarations: -``` +```carbon class Y {} class N {} interface True {} @@ -4210,18 +5080,18 @@ declarations are selected. - An implementation of `Z(i16)` for `i8` could come from the first blanket impl with `T == i8` and `U == i16` if `i16 impls Z(i8)` and - `i16.(Z(i8).Cond) == Y`. This condition is satisfied if `i16` implements + `(i16 as Z(i8)).Cond == Y`. This condition is satisfied if `i16` implements `Z(i8)` using the second blanket impl. In this case, - `i8.(Z(i16).Cond) == N`. + `(i8 as Z(i16)).Cond == N`. - Equally well `Z(i8)` could be implemented for `i16` using the first blanket impl and `Z(i16)` for `i8` using the second. In this case, - `i8.(Z(i16).Cond) == Y`. + `(i8 as Z(i16)).Cond == Y`. There is no reason to to prefer one of these outcomes over the other. **Example:** Further, cycles can create contradictions in the type system: -``` +```carbon class A {} class B {} class C {} @@ -4236,18 +5106,20 @@ match_first { } ``` -What is `i8.(D(i16).Cond)`? The answer is determined by which blanket impl is +What is `(i8 as D(i16)).Cond`? The answer is determined by which blanket impl is selected to implement `D(i16)` for `i8`: -- If the third blanket impl is selected, then `i8.(D(i16).Cond) == A`. This - implies that `i16.(D(i8).Cond) == B` using the second blanket impl. If that - is true, though, then our first impl choice was incorrect, since the first - blanket impl applies and is higher priority. So `i8.(D(i16).Cond) == C`. But - that means that `i16 as D(i8)` can't use the second blanket impl. -- For the second blanket impl to be selected, so `i8.(D(i16).Cond) == B`, - `i16.(D(i8).Cond)` would have to be `A`. This happens when `i16` implements - `D(i8)` using the third blanket impl. However, `i8.(D(i16).Cond) == B` means - that there is a higher priority implementation of `D(i8).Cond` for `i16`. +- If the third blanket impl is selected, then `(i8 as D(i16)).Cond == A`. This + implies that `(i16 as D(i8)).Cond == B` using the second blanket impl. If + that is true, though, then our first impl choice was incorrect, since the + first blanket impl applies and is higher priority. So + `(i8 as D(i16)).Cond == C`. But that means that `i16 as D(i8)` can't use the + second blanket impl. +- For the second blanket impl to be selected, so `(i8 as D(i16)).Cond == B`, + `(i16 as D(i8)).Cond` would have to be `A`. This happens when `i16` + implements `D(i8)` using the third blanket impl. However, + `(i8 as D(i16)).Cond == B` means that there is a higher priority + implementation of `D(i8).Cond` for `i16`. In either case, we arrive at a contradiction. @@ -4281,36 +5153,142 @@ forever. `Optional(A) impls B`, if `Optional(Optional(A)) impls B`, and so on. This could be the result of a single impl: -``` +```carbon impl forall [A:! type where Optional(.Self) impls B] A as B { ... } ``` This problem can also result from a chain of `impl` declarations, as in `A impls B` if `A* impls C`, if `Optional(A) impls B`, and so on. -Rust solves this problem by imposing a recursion limit, much like C++ compilers -use to terminate template recursion. This goes against -[Carbon's goal of predictability in generics](goals.md#predictability), but at -this time there are no known alternatives. Unfortunately, the approach Carbon -uses to avoid undecidability for type equality, -[providing an explicit proof in the source](#manual-type-equality), can't be -used here. The code triggering the query asking whether some type implements an -interface will typically be checked-generic code with no specific knowledge -about the types involved, and won't be in a position to provide a manual proof -that the implementation should exist. - -**Open question:** Is there some restriction on `impl` declarations that would -allow our desired use cases, but allow the compiler to detect non-terminating -cases? Perhaps there is some sort of complexity measure Carbon can require -doesn't increase when recursing? +Determining whether a particular set of `impl` declarations terminates is +[equivalent to the halting problem](https://sdleffler.github.io/RustTypeSystemTuringComplete/) +(content warning: contains many instances of an obscene word as part of a +programming language name), and so is undecidable in general. Carbon adopts an +approximation that guarantees termination, but may mistakenly report an error +when the query would terminate if left to run long enough. The hope is that this +criteria is accurate on code that occurs in practice. + +Rule: the types in the `impl` query must never get strictly more complicated +when considering the same `impl` declaration again. The way we measure the +complexity of a set of types is by counting how many of each base type appears. +A base type is the name of a type without its parameters. For example, the base +types in this query `Pair(Optional(i32), bool) impls AddWith(Optional(i32))` +are: + +- `Pair` +- `Optional` twice +- `i32` twice +- `bool` +- `AddWith` + +A query is strictly more complicated if at least one count increases, and no +count decreases. So `Optional(Optional(i32))` is strictly more complicated than +`Optional(i32)` but not strictly more complicated than `Optional(bool)`. + +This rule, when combined with [the acyclic rule](#acyclic-rule) that a query +can't repeat exactly, +[guarantees termination](/proposals/p2687.md#proof-of-termination). + +Consider the example from before, + +```carbon +impl forall [A:! type where Optional(.Self) impls B] A as B; +``` + +This `impl` declaration matches the query `i32 impls B` as long as +`Optional(i32) impls B`. That is a strictly more complicated query, though, +since it contains all the base types of the starting query (`i32` and `B`), plus +one more (`Optional`). As a result, an error can be given after one step, rather +than after hitting a large recursion limit. And that error can state explicitly +what went wrong: we went from a query with no `Optional` to one with one, +without anything else decreasing. + +Note this only triggers a failure when the same `impl` declaration is considered +with the strictly more complicated query. For example, if the declaration is not +considered since there is a more specialized `impl` declaration that is +preferred by the [type-structure overlap rule](#overlap-rule), as in: + +``` +impl forall [A:! type where Optional(.Self) impls B] A as B; +impl Optional(bool) as B; +// OK, because we never consider the first `impl` +// declaration when looking for `Optional(bool) impls I`. +let U:! B = bool; +// Error: cycle with `i32 impls B` depending on +// `Optional(i32) impls B`, using the same `impl` +// declaration, as before. +let V:! B = i32; +``` + +> **Comparison with other languages:** Rust solves this problem by imposing a +> recursion limit, much like C++ compilers use to terminate template recursion. +> This goes against +> [Carbon's goal of predictability in generics](goals.md#predictability), +> because of the concern that increasing the number of steps needed to resolve +> an `impl` query could cause far away code to hit the recursion limit. +> +> Carbon's approach is robust in the face of refactoring: +> +> - It does not depend on the specifics of how an `impl` declaration is +> parameterized, only on the query. +> - It does not depend on the length of the chain of queries. +> - It does not depend on a measure of type-expression complexity, like depth. +> +> Carbon's approach also results in identifying the minimal steps in the loop, +> which makes error messages as short and understandable as possible. + +> **Alternatives considered:** +> +> - [Recursion limit](/proposals/p2687.md#problem) +> - [Measure complexity using type tree depth](/proposals/p2687.md#measure-complexity-using-type-tree-depth) +> - [Consider each type parameter in an `impl` declaration separately](/proposals/p2687.md#consider-each-type-parameter-in-an-impl-declaration-separately) +> - [Consider types in the interface being implemented as distinct](/proposals/p2687.md#consider-types-in-the-interface-being-implemented-as-distinct) +> - [Require some count to decrease](/proposals/p2687.md#require-some-count-to-decrease) +> - [Require non-type values to stay the same](/proposals/p2687.md#require-non-type-values-to-stay-the-same) + +> **References:** This algorithm is from proposal +> [#2687: Termination algorithm for impl selection](https://github.com/carbon-language/carbon-lang/pull/2687), +> replacing the recursion limit originally proposed in +> [#920: Generic parameterized impls (details 5)](https://github.com/carbon-language/carbon-lang/pull/920) +> before we came up with this algorithm. + +##### Non-facet arguments + +For non-facet arguments we have to expand beyond base types to consider other +kinds of keys. These other keys are in a separate namespace from base types. + +- Values with an integral type use the name of the type as the key and the + absolute value as a count. This means integer arguments are considered more + complicated if they increase in absolute value. For example, if the values + `2` and `-3` are used as arguments to parameters with type `i32`, then the + `i32` key will have count `5`. +- Every option of a choice type is its own key, counting how many times a + value using that option occurs. Any parameters to the option are recorded as + separate keys. For example, the `Optional(i32)` value of `.Some(7)` is + recorded as keys `.Some` (with a count of `1`) and `i32` (with a count of + `7`). +- Yet another namespace of keys is used to track counts of variadic arguments, + under the base type. This is to defend against having a variadic type `V` + that takes any number of `i32` arguments, with an infinite set of distinct + instantiations: `V(0)`, `V(0, 0)`, `V(0, 0, 0)`, ... + - A `tuple` key in this namespace is used to track the total number of + components of tuple values. The values of those elements will be tracked + using their own keys. + +Non-facet argument values not covered by these cases are deleted from the query +entirely for purposes of the termination algorithm. This requires that two +queries that only differ by non-facet arguments are considered identical and +therefore are rejected by the acyclic rule. Otherwise, we could construct an +infinite family of non-facet argument values that could be used to avoid +termination. ### `final` impl declarations There are cases where knowing that a parameterized impl won't be specialized is particularly valuable. This could let the compiler know the return type of a -generic function call, such as using an operator: +call to a generic function, such as using an operator: -``` +```carbon // Interface defining the behavior of the prefix-* operator interface Deref { let Result:! type; @@ -4342,7 +5320,7 @@ anything about the return type of `Deref.Op` calls. This means `F` would in practice have to add a constraint, which is both verbose and exposes what should be implementation details: -``` +```carbon fn F[T:! type where Optional(T).(Deref.Result) == .Self and Ptr(T).(Deref.Result) == .Self](x: T) { // uses Ptr(T) and Optional(T) in implementation @@ -4352,7 +5330,7 @@ fn F[T:! type where Optional(T).(Deref.Result) == .Self To mark an impl as not able to be specialized, prefix it with the keyword `final`: -``` +```carbon class Ptr(T:! type) { ... // Note: added `final` @@ -4400,7 +5378,7 @@ If the Carbon compiler sees a matching `final` impl, it can assume it won't be specialized so it can use the assignments of the associated constants in that impl definition. -``` +```carbon fn F[T:! type](x: T) { var p: Ptr(T) = ...; // *p has type `T` @@ -4409,21 +5387,21 @@ fn F[T:! type](x: T) { } ``` -**Alternatives considered:** - -- [Allow interfaces with member functions to compare equal](/proposals/p2868.md#allow-interfaces-with-member-functions-to-compare-equal) -- Mark associated constants as `final` instead of an `impl` declaration, in - proposals - [#983](/proposals/p0983.md#final-associated-constants-instead-of-final-impls) - and - [#2868](/proposals/p2868.md#mark-associated-constants-as-final-instead-of-an-impl-declaration) -- [Prioritize a `final impl` over a more specific `impl` on the overlap](/proposals/p2868.md#prioritize-a-final-impl-over-a-more-specific-impl-on-the-overlap) +> **Alternatives considered:** +> +> - [Allow interfaces with member functions to compare equal](/proposals/p2868.md#allow-interfaces-with-member-functions-to-compare-equal) +> - Mark associated constants as `final` instead of an `impl` declaration, in +> proposals +> [#983](/proposals/p0983.md#final-associated-constants-instead-of-final-impls) +> and +> [#2868](/proposals/p2868.md#mark-associated-constants-as-final-instead-of-an-impl-declaration) +> - [Prioritize a `final impl` over a more specific `impl` on the overlap](/proposals/p2868.md#prioritize-a-final-impl-over-a-more-specific-impl-on-the-overlap) #### Libraries that can contain a `final` impl -To prevent the possibility of two unrelated libraries defining conflicting impl -declarations, Carbon restricts which libraries may declare an impl as `final` to -only: +To prevent the possibility of two unrelated libraries defining conflicting +`impl` declarations, Carbon restricts which libraries may declare an impl as +`final` to only: - the library declaring the impl's interface and - the library declaring the root of the `Self` type. @@ -4462,9 +5440,9 @@ process, so Carbon can benefit from the work they have done. However, getting specialization to work for Rust is complicated by the need to maintain compatibility with existing Rust code. This motivates a number of Rust rules where Carbon can be simpler. As a result there are both similarities and -differences between the Carbon and Rust plans: +differences between the Carbon design and Rust plans: -- A Rust impl defaults to not being able to be specialized, with a `default` +- A Rust `impl` defaults to not being able to be specialized, with a `default` keyword used to opt-in to allowing specialization, reflecting the existing code base developed without specialization. Carbon `impl` declarations default to allowing specialization, with restrictions on which may be @@ -4488,9 +5466,9 @@ differences between the Carbon and Rust plans: [Little Orphan Impls: The ordered rule](http://smallcultfollowing.com/babysteps/blog/2015/01/14/little-orphan-impls/#the-ordered-rule), but the specifics are different. - Carbon is not planning to support any inheritance of implementation between - impl definitions. This is more important to Rust since Rust does not support - class inheritance for implementation reuse. Rust has considered multiple - approaches here, see + `impl` definitions. This is more important to Rust since Rust does not + support class inheritance for implementation reuse. Rust has considered + multiple approaches here, see [Aaron Turon: "Specialize to Reuse"](http://aturon.github.io/tech/2015/09/18/reuse/) and [Supporting blanket impls in specialization](http://smallcultfollowing.com/babysteps/blog/2016/10/24/supporting-blanket-impls-in-specialization/). @@ -4536,10 +5514,7 @@ interface in its parameter list. There is a the use cases when this would come up. An expression forming a constraint, such as `C & D`, is incomplete if any of the -interfaces or constraints used in the expression are incomplete. A constraint -expression using a [`where` clause](#where-constraints), like `C where ...`, is -invalid if `C` is incomplete, since there is no way to look up member names of -`C` that appear after `where`. +interfaces or constraints used in the expression are incomplete. An interface or named constraint may be forward declared subject to these rules: @@ -4547,17 +5522,17 @@ An interface or named constraint may be forward declared subject to these rules: - Only the first declaration may have an access-control keyword. - An incomplete interface or named constraint may be used as constraints in declarations of types, functions, interfaces, or named constraints. This - includes an `impl as` or `extend` declaration inside an interface or named + includes an `require` or `extend` declaration inside an interface or named constraint, but excludes specifying the values for associated constants because that would involve name lookup into the incomplete constraint. - An attempt to define the body of a generic function using an incomplete - interface or named constraint is illegal. + interface or named constraint in its signature is illegal. - An attempt to call a generic function using an incomplete interface or named constraint in its signature is illegal. - Any name lookup into an incomplete interface or named constraint is an error. For example, it is illegal to attempt to access a member of an interface using `MyInterface.MemberName` or constrain a member using a - `where` clause. + [`where` clause](#where-constraints). If `C` is the name of an incomplete interface or named constraint, then it can be used in the following contexts: @@ -4566,8 +5541,8 @@ be used in the following contexts: - ✅ `C & D` - There may be conflicts between `C` and `D` making this invalid that will only be discovered once they are both complete. -- ✅ `interface `...` { impl` ... `as C; }` or `constraint `...` { impl` ... - `as C; }` +- ✅ `interface `...` { require` ... `impls C; }` or + `constraint `...` { require` ... `impls C; }` - Nothing implied by implementing `C` will be visible until `C` is complete. - ✅ `T:! C` ... `T impls C` @@ -4590,24 +5565,24 @@ An incomplete `C` cannot be used in the following contexts: - Need to see the definition of `C` to see if it implies `A`. - ❌ `impl` ... `as C {` ... `}` -**Future work:** It is currently undecided whether an interface needs to be -complete to be extended, as in: - -``` -interface I { extend C; } -``` - -There are three different approaches being considered: - -- If we detect name collisions between the members of the interface `I` and - `C` when the interface `I` is defined, then we need `C` to be complete. -- If we instead only generate errors on ambiguous use of members with the same - name, as we do with `A & B`, then we don't need to require `C` to be - complete. -- Another option, being discussed in - [#2355](https://github.com/carbon-language/carbon-lang/issues/2355), is that - names in interface `I` shadow the names in any interface being extended, - then `C` would not be required to be complete. +> **Future work:** It is currently undecided whether an interface needs to be +> complete to be extended, as in: +> +> ```carbon +> interface I { extend C; } +> ``` +> +> There are three different approaches being considered: +> +> - If we detect name collisions between the members of the interface `I` and +> `C` when the interface `I` is defined, then we need `C` to be complete. +> - If we instead only generate errors on ambiguous use of members with the +> same name, as we do with `A & B`, then we don't need to require `C` to be +> complete. +> - Another option, being discussed in +> [#2355](https://github.com/carbon-language/carbon-lang/issues/2355), is +> that names in interface `I` shadow the names in any interface being +> extended, then `C` would not be required to be complete. ### Declaring implementations @@ -4617,46 +5592,43 @@ The declaration of an interface implementation consists of: - the keyword introducer `impl`, - an optional `forall` followed by a deduced parameter list in square brackets `[`...`]`, -- a type, including an optional parameter pattern, +- a type, including an optional [argument list](#parameterized-types), - the keyword `as`, and - a [facet type](#facet-types), including an optional - [parameter pattern](#parameterized-interfaces) and + [argument list](#parameterized-interfaces) and [`where` clause](#where-constraints) assigning [associated constants](#associated-constants) including [associated facets](#associated-facets). -**Note:** The `extend` keyword, when present, is not part of the declaration. It -precedes the `impl` declaration in class scope. +**Note:** The `extend` keyword, when present, is not part of the `impl` +declaration. It precedes the `impl` declaration in class scope. -An implementation of an interface for a type may be forward declared subject to +An implementation of an interface for a type may be forward declared, subject to these rules: - The definition must be in the same library as the declaration. They must either be in the same file, or the declaration can be in the API file and the definition in an impl file. **Future work:** Carbon may require - [parameterized impl definitions](#parameterized-impl-declarations) to be in - the API file, to support separate compilation. + [parameterized `impl` definitions](#parameterized-impl-declarations) to be + in the API file, to support separate compilation. - If there is both a forward declaration and a definition, only the first declaration must specify the assignment of associated constants with a `where` clause. Later declarations may omit the `where` clause by writing `where _` instead. -- You may forward declare an implementation of a defined interface but not an - incomplete interface. This allows the assignment of associated constants in - the `impl` declaration to be verified. An impl forward declaration may be - for any declared type, whether it is incomplete or defined. Note that this - does not apply to `impl as` declarations in an interface or named constraint - definition, as those are considered interface requirements not forward - declarations. -- Every extending implementation must be declared (or defined) inside the - scope of the class definition. It may also be declared before the class - definition or defined afterwards. Note that the class itself is incomplete - in the scope of the class definition, but member function bodies defined - inline are processed +- You can't forward declare an implementation of an incomplete interface. This + allows the assignment of associated constants in the `impl` declaration to + be verified with the declaration. An `impl` forward declaration may be for + any declared type, whether it is incomplete or defined. +- Every [extending implementation](#extend-impl) must be declared (or defined) + inside the scope of the class definition. It may also be declared before the + class definition or defined afterwards. Note that the class itself is + incomplete in the scope of the class definition, but member function bodies + defined inline are processed [as if they appeared immediately after the end of the outermost enclosing class](/docs/project/principles/information_accumulation.md#exceptions). -- For [coherence](goals.md#coherence), we require that any `impl` declaration - that matches an impl lookup query in the same file, must be declared before - the query. This can be done with a definition or a forward declaration. This - matches the +- For [coherence](terminology.md#coherence), we require that any `impl` + declaration that matches an impl lookup query in the same file, must be + declared before the query. This can be done with a definition or a forward + declaration. This matches the [information accumulation principle](/docs/project/principles/information_accumulation.md). ### Matching and agreeing @@ -4684,9 +5656,10 @@ expressions match along with - If the type part is omitted, it is rewritten to `Self` in the context of the declaration. - `Self` is rewritten to its meaning in the scope it is used. In a class - scope, this should match the type name and optional parameter expression - after `class`. So in `class MyClass { ... }`, `Self` is rewritten to - `MyClass`. In `class Vector(T:! Movable) { ... }`, `Self` is rewritten to + scope, this should match the type name and + [optional parameter expression](#parameterized-types) after `class`. So in + `class MyClass { ... }`, `Self` is rewritten to `MyClass`. In + `class Vector(T:! Movable) { ... }`, `Self` is rewritten to `forall [T:! Movable] Vector(T)`. - Types match if they have the same name after name and alias resolution and the same parameters, or are the same type parameter. @@ -4705,7 +5678,7 @@ For implementations to agree: ### Declaration examples -``` +```carbon // Forward declaration of interfaces interface Interface1; interface Interface2; @@ -4803,7 +5776,7 @@ constrained to implement `Node`. Furthermore, the `NodeType` of an `EdgeType` is the original type, and the other way around. This is accomplished by naming and then forward declaring the constraints that can't be stated directly: -``` +```carbon // Forward declare interfaces used in // parameter lists of constraints. interface Edge; @@ -4841,7 +5814,7 @@ To work around [the restriction about not being able to name an interface in its parameter list](#declaring-interfaces-and-named-constraints), instead include that requirement in the body of the interface. -``` +```carbon // Want to require that `T` satisfies `CommonType(Self)`, // but that can't be done in the parameter list. interface CommonType(T:! type) { @@ -4856,7 +5829,7 @@ constraints on members of `CommonType` are allowed, and that this `require T impls` declaration [must involve `Self`](#interface-requiring-other-interfaces-revisited). -``` +```carbon interface CommonType(T:! type) { let Result:! type; // ❌ Illegal: `CommonType` is incomplete @@ -4868,7 +5841,7 @@ Instead, a forward-declared named constraint can be used in place of the constraint that can only be defined later. This is [the same strategy used to work around cyclic references](#example-of-declaring-interfaces-with-cyclic-references). -``` +```carbon private constraint CommonTypeResult(T:! type, R:! type); interface CommonType(T:! type) { @@ -4896,7 +5869,7 @@ and prefixed with the `final` keyword. An interface may provide a default implementation of methods in terms of other methods in the interface. -``` +```carbon interface Vector { fn Add[self: Self](b: Self) -> Self; fn Scale[self: Self](v: f64) -> Self; @@ -4910,7 +5883,7 @@ interface Vector { A default function or method may also be defined out of line, later in the same file as the interface definition: -``` +```carbon interface Vector { fn Add[self: Self](b: Self) -> Self; fn Scale[self: Self](v: f64) -> Self; @@ -4936,7 +5909,7 @@ has one required method but dozens of "provided methods" with defaults. Defaults may also be provided for associated constants, such as associated facets, and interface parameters, using the `= ` syntax. -``` +```carbon interface Add(Right:! type = Self) { default let Result:! type = Self; fn DoAdd[self: Self](right: Right) -> Result; @@ -4952,7 +5925,7 @@ Note that `Self` is a legal default value for an associated facet or facet parameter. In this case the value of those names is not determined until `Self` is, so `Add()` is equivalent to the constraint: -``` +```carbon // Equivalent to Add() constraint AddDefault { extend Add(Self); @@ -4965,7 +5938,7 @@ parameters are left as their default values. More generally, default expressions may reference other associated constants or `Self` as parameters to type constructors. For example: -``` +```carbon interface Iterator { let Element:! type; default let Pointer:! type = Element*; @@ -4975,7 +5948,7 @@ interface Iterator { Carbon does **not** support providing a default implementation of a required interface. -``` +```carbon interface TotalOrder { fn TotalLess[self: Self](right: Self) -> bool; // ❌ Illegal: May not provide definition @@ -4991,7 +5964,11 @@ interface TotalOrder { The workaround for this restriction is to use a [blanket impl declaration](#blanket-impl-declarations) instead: -``` +**FIXME: Is it sensible to have both a `require` and a blanket implementation? +Does the blanket implementation satisfy the requirement so you only need to +implement `TotalOrder`?** + +```carbon interface TotalOrder { fn TotalLess[self: Self](right: Self) -> bool; require Self impls PartialOrder; @@ -5020,7 +5997,7 @@ As an alternative to providing a definition of an interface member as a default, members marked with the `final` keyword will not allow that definition to be overridden in `impl` definitions. -``` +```carbon interface TotalOrder { fn TotalLess[self: Self](right: Self) -> bool; final fn TotalGreater[self: Self](right: Self) -> bool { @@ -5041,14 +6018,14 @@ interface Add(T:! type = Self) { // `AddWith` *always* equals `T` final let AddWith:! type = T; // Has a *default* of `Self` - let Result:! type = Self; + default let Result:! type = Self; fn DoAdd[self: Self](right: AddWith) -> Result; } ``` Final members may also be defined out-of-line: -``` +```carbon interface TotalOrder { fn TotalLess[self: Self](right: Self) -> bool; final fn TotalGreater[self: Self](right: Self) -> bool; @@ -5076,7 +6053,7 @@ Recall that an [interface can require another interface be implemented for the type](#interface-requiring-other-interfaces), as in: -``` +```carbon interface Iterable { require Self impls Equatable; // ... @@ -5089,7 +6066,7 @@ done with [conditional conformance](#conditional-conformance), we allow another type to be specified between `require` and `impls` to say some type other than `Self` must implement an interface. For example, -``` +```carbon interface IntLike { require i32 impls As(Self); // ... @@ -5099,7 +6076,7 @@ interface IntLike { says that if `Self` implements `IntLike`, then `i32` must implement `As(Self)`. Similarly, -``` +```carbon interface CommonTypeWith(T:! type) { require T impls CommonTypeWith(Self); // ... @@ -5110,8 +6087,9 @@ says that if `Self` implements `CommonTypeWith(T)`, then `T` must implement `CommonTypeWith(Self)`. An `require`...`impls` constraint in an `interface`, or `constraint`, definition -must still use `Self` in some way. It can be an argument to either the type or -interface. For example: +must still use `Self` in some way. It can be an argument to either the +[type](#parameterized-types) or [interface](#parameterized-interfaces). For +example: - ✅ Allowed: `require Self impls Equatable` - ✅ Allowed: `require Vector(Self) impls Equatable` @@ -5124,9 +6102,9 @@ interface. For example: This restriction allows the Carbon compiler to know where to look for facts about a type. If `require i32 impls Equatable` could appear in any `interface` definition, that implies having to search all of them when considering what -interfaces `i32` implements. This creates a coherence problem, since then the -set of facts true for a type would depend on which interfaces have been -imported. +interfaces `i32` implements. This would create a +[coherence](terminology.md#coherence) problem, since then the set of facts true +for a type would depend on which interfaces have been imported. When implementing an interface with an `require`...`impls` requirement, that requirement must be satisfied by an implementation in an imported library, an @@ -5136,7 +6114,7 @@ requirement will be implemented. This is like a [forward declaration of an impl](#declaring-implementations) except that the definition can be broader instead of being required to match exactly. -``` +```carbon // `Iterable` requires `Equatable`, so there must be some // impl of `Equatable` for `Vector(i32)` in this file. impl Vector(i32) as Iterable { ... } @@ -5149,14 +6127,14 @@ fn ProcessVector(v: Vector(i32)) { } // Satisfies the requirement that `Vector(i32)` must -// implement `Equatable` since `i32` impls `Equatable`. +// implement `Equatable` since `i32 impls Equatable`. impl forall [T:! Equatable] Vector(T) as Equatable { ... } ``` In some cases, the interface's requirement can be trivially satisfied by the implementation itself, as in: -``` +```carbon impl forall [T:! type] T as CommonTypeWith(T) { ... } ``` @@ -5164,7 +6142,7 @@ Here is an example where the requirement of interface `Iterable` that the type implements interface `Equatable` is satisfied by a constraint in the `impl` declaration: -``` +```carbon class Foo(T:! type) {} // This is allowed because we know that an `impl Foo(T) as Equatable` // will exist for all types `T` for which this impl is used, even @@ -5176,7 +6154,7 @@ impl forall [T:! type where Foo(T) impls Equatable] This might be used to provide an implementation of `Equatable` for types that already satisfy the requirement of implementing `Iterable`: -``` +```carbon class Bar {} impl Foo(Bar) as Equatable {} // Gives `Foo(Bar) impls Iterable` using the blanket impl of @@ -5189,7 +6167,7 @@ An interface implementation requirement with a `where` clause is harder to satisfy. Consider an interface `B` that has a requirement that interface `A` is also implemented. -``` +```carbon interface A(T:! type) { let Result:! type; } @@ -5212,9 +6190,10 @@ to have a different assignment. An [`observe` declaration](#observe-declarations) can be used to show that two types are equal so code can pass type checking without explicitly writing casts, -without requiring the compiler to do a unbounded search that may not terminate. -An `observe` declaration can also be used to show that a type implements an -interface, in cases where the compiler will not work this out for itself. +and without requiring the compiler to do a unbounded search that may not +terminate. An `observe` declaration can also be used to show that a type +implements an interface, in cases where the compiler will not work this out for +itself. ### Observing interface requirements @@ -5222,13 +6201,13 @@ One situation where this occurs is when there is a chain of [interfaces requiring other interfaces](#interface-requiring-other-interfaces-revisited). During the `impl` validation done during type checking, Carbon will only consider the interfaces that are direct requirements of the interfaces the type -is known to implement. An `observe...impls` declaration can be used to add an +is known to implement. An `observe`...`impls` declaration can be used to add an interface that is a direct requirement to the set of interfaces whose direct requirements will be considered for that type. This allows a developer to provide a proof that there is a sequence of requirements that demonstrate that a type implements an interface, as in this example: -``` +```carbon interface A { } interface B { require Self impls A; } interface C { require Self impls B; } @@ -5243,35 +6222,35 @@ fn RequiresD[T:! D](x: T) { // ❌ Illegal: No direct connection between `D` and `A`. // RequiresA(x); - // `T` impls `D` and `D` directly requires `C` to be + // `T impls D` and `D` directly requires `C` to be // implemented. observe T impls C; - // `T` impls `C` and `C` directly requires `B` to be + // `T impls C` and `C` directly requires `B` to be // implemented. observe T impls B; - // ✅ Allowed: `T` impls `B` and `B` directly requires + // ✅ Allowed: `T impls B` and `B` directly requires // `A` to be implemented. RequiresA(x); } ``` Note that `observe` statements do not affect which impl is selected during code -generation. For coherence, the impl used for a (type, interface) pair must -always be the same, independent of context. The +generation. For [coherence](terminology.md#coherence), the impl used for a +(type, interface) pair must always be the same, independent of context. The [termination rule](#termination-rule) governs when compilation may fail when the -compiler can't determine the impl to select. +compiler can't determine the `impl` definition to select. ### Observing blanket impl declarations -An `observe...impls` declaration can also be used to observe that a type +An `observe`...`impls` declaration can also be used to observe that a type implements an interface because there is a [blanket impl declaration](#blanket-impl-declarations) in terms of requirements a type is already known to satisfy. Without an `observe` declaration, Carbon will only use blanket impl declarations that are directly satisfied. -``` +```carbon interface A { } interface B { } interface C { } @@ -5311,27 +6290,57 @@ In the case of an error, a quality Carbon implementation will do a deeper search for chains of requirements and blanket impl declarations and suggest `observe` declarations that would make the code compile if any solution is found. +### Observing equal to a type implementing an interface + +The [`observe`...`==` form](#observe-declarations) can be combined with the +`observe`...`impls` form to show that a type implements an interface because it +is equal to another type that is known to implement that interface. + +```carbon +interface I { + fn F(); +} + +fn G(T:! I, U:! type where .Self == T) { + // ❌ Illegal: No implementation of `I` for `U`. + U.(I.F)(); + + // ✅ Allowed: Implementation of `I` for `U` + // through `T`. + observe U == T impls I; + U.(I.F)(); + + // ❌ Illegal: `U` does not extend `I`. + U.F(); +} +``` + +Multiple `==` clauses are allowed in an `observe` declaration, so you may write +`observe A == B == C impls I;`. + ## Operator overloading Operations are overloaded for a type by implementing an interface specific to -that interface for that type. For example, types implement the `Negatable` -interface to overload the unary `-` operator: +that interface for that type. For example, types implement +[the `Negate` interface](/docs/design/expressions/arithmetic.md#extensibility) +to overload the unary `-` operator: -``` +```carbon // Unary `-`. -interface Negatable { - let Result:! type = Self; - fn Negate[self: Self]() -> Result; +interface Negate { + default let Result:! type = Self; + fn Op[self: Self]() -> Result; } ``` Expressions using operators are rewritten into calls to these interface methods. -For example, `-x` would be rewritten to `x.(Negatable.Negate)()`. +For example, `-x` would be rewritten to `x.(Negate.Op)()`. The interfaces and rewrites used for a given operator may be found in the [expressions design](/docs/design/expressions/README.md). [Question-for-leads issue #1058](https://github.com/carbon-language/carbon-lang/issues/1058) -defines the naming scheme for these interfaces. +defines the naming scheme for these interfaces, which was implemented in +[proposal #1178](https://github.com/carbon-language/carbon-lang/pull/1178). ### Binary operators @@ -5341,7 +6350,7 @@ example, to say a type may be converted to another type using an `as` expression, implement the [`As` interface](/docs/design/expressions/as_expressions.md#extensibility): -``` +```carbon interface As(Dest:! type) { fn Convert[self: Self]() -> Dest; } @@ -5352,26 +6361,26 @@ parameterization of the interface means it can be implemented multiple times to support multiple operand types. Unlike `as`, for most binary operators the interface's argument will be the -_type_ of the right-hand operand instead of its _value_. Consider an interface -for a binary operator like `*`: +_type_ of the right-hand operand instead of its _value_. Consider +[the interface for a binary operator like `*`](/docs/design/expressions/arithmetic.md#extensibility): -``` +```carbon // Binary `*`. -interface MultipliableWith(U:! type) { - let Result:! type = Self; - fn Multiply[self: Self](other: U) -> Result; +interface MulWith(U:! type) { + default let Result:! type = Self; + fn Op[self: Self](other: U) -> Result; } ``` A use of binary `*` in source code will be rewritten to use this interface: -``` +```carbon var left: Meters = ...; var right: f64 = ...; var result: auto = left * right; // Equivalent to: -var equivalent: left.(MultipliableWith(f64).Result) - = left.(MultipliableWith(f64).Multiply)(right); +var equivalent: left.(MulWith(f64).Result) + = left.(MulWith(f64).Op)(right); ``` Note that if the types of the two operands are different, then swapping the @@ -5380,23 +6389,28 @@ It is up to the developer to make those consistent when that is appropriate. The standard library will provide [adapters](#adapting-types) for defining the second implementation from the first, as in: -``` -interface ComparableWith(RHS:! type) { - fn Compare[self: Self](right: RHS) -> CompareResult; +```carbon +interface OrderedWith(U:! type) { + fn Compare[self: Self](u: U) -> Ordering; + // ... } -class ReverseComparison - (T:! type, U:! ComparableWith(RHS)) { +class ReverseComparison(T:! type, U:! OrderedWith(T)) { adapt T; - extend impl as ComparableWith(U) { - fn Compare[self: Self](right: RHS) -> CompareResult { - return ReverseCompareResult(right.Compare(self)); + extend impl as OrderedWith(U) { + fn Compare[self: Self](u: U) -> Ordering { + match (u.Compare(self)) { + case .Less => return .Greater; + case .Equivalent => return .Equivalent; + case .Greater => return .Less; + case .Incomparable => return .Incomparable; + } } } } -impl SongByTitle as ComparableWith(SongTitle); -impl SongTitle as ComparableWith(SongByTitle) +impl SongByTitle as OrderedWith(SongTitle) { ... } +impl SongTitle as OrderedWith(SongByTitle) = ReverseComparison(SongTitle, SongByTitle); ``` @@ -5404,59 +6418,59 @@ In some cases the reverse operation may not be defined. For example, a library might support subtracting a vector from a point, but not the other way around. Further note that even if the reverse implementation exists, -[the impl prioritization rule](#prioritization-rule) might not pick it. For +[the `impl` prioritization rule](#prioritization-rule) might not pick it. For example, if we have two types that support comparison with anything implementing an interface that the other implements: -``` +```carbon interface IntLike { fn AsInt[self: Self]() -> i64; } class EvenInt { ... } impl EvenInt as IntLike; -impl EvenInt as ComparableWith(EvenInt); +impl EvenInt as OrderedWith(EvenInt); // Allow `EvenInt` to be compared with anything that // implements `IntLike`, in either order. -impl forall [T:! IntLike] EvenInt as ComparableWith(T); -impl forall [T:! IntLike] T as ComparableWith(EvenInt); +impl forall [T:! IntLike] EvenInt as OrderedWith(T); +impl forall [T:! IntLike] T as OrderedWith(EvenInt); class PositiveInt { ... } impl PositiveInt as IntLike; -impl PositiveInt as ComparableWith(PositiveInt); +impl PositiveInt as OrderedWith(PositiveInt); // Allow `PositiveInt` to be compared with anything that // implements `IntLike`, in either order. -impl forall [T:! IntLike] PositiveInt as ComparableWith(T); -impl forall [T:! IntLike] T as ComparableWith(PositiveInt); +impl forall [T:! IntLike] PositiveInt as OrderedWith(T); +impl forall [T:! IntLike] T as OrderedWith(PositiveInt); ``` -Then it will favor selecting the implementation based on the type of the -left-hand operand: +Then the compiler will favor selecting the implementation based on the type of +the left-hand operand: -``` +```carbon var even: EvenInt = ...; var positive: PositiveInt = ...; -// Uses `EvenInt as ComparableWith(T)` impl +// Uses `EvenInt as OrderedWith(T)` impl if (even < positive) { ... } -// Uses `PositiveInt as ComparableWith(T)` impl +// Uses `PositiveInt as OrderedWith(T)` impl if (positive > even) { ... } ``` ### `like` operator for implicit conversions -Because the type of the operands is directly used to select the implementation -to use, there are no automatic implicit conversions, unlike with function or -method calls. Given both a method and an interface implementation for -multiplying by a value of type `f64`: +Because the type of the operands is directly used to select the operator +interface implementation, there are no automatic implicit conversions, unlike +with function or method calls. Given both a method and an interface +implementation for multiplying by a value of type `f64`: -``` +```carbon class Meters { fn Scale[self: Self](s: f64) -> Self; } // "Implementation One" -impl Meters as MultipliableWith(f64) +impl Meters as MulWith(f64) where .Result = Meters { - fn Multiply[self: Self](other: f64) -> Result { + fn Op[self: Self](other: f64) -> Result { return self.Scale(other); } } @@ -5466,14 +6480,14 @@ the method will work with any argument that can be implicitly converted to `f64` but the operator overload will only work with values that have the specific type of `f64`: -``` +```carbon var height: Meters = ...; var scale: f32 = 1.25; // ✅ Allowed: `scale` implicitly converted // from `f32` to `f64`. var allowed: Meters = height.Scale(scale); // ❌ Illegal: `Meters` doesn't implement -// `MultipliableWith(f32)`. +// `MulWith(f32)`. var illegal: Meters = height * scale; ``` @@ -5481,17 +6495,17 @@ The workaround is to define a parameterized implementation that performs the conversion. The implementation is for types that implement the [`ImplicitAs` interface](/docs/design/expressions/implicit_conversions.md#extensibility). -``` +```carbon // "Implementation Two" impl forall [T:! ImplicitAs(f64)] - Meters as MultipliableWith(T) where .Result = Meters { - fn Multiply[self: Self](other: T) -> Result { + Meters as MulWith(T) where .Result = Meters { + fn Op[self: Self](other: T) -> Result { // Carbon will implicitly convert `other` from type // `T` to `f64` to perform this call. - return self.(Meters.(MultipliableWith(f64).Multiply))(other); + return self.((Meters as MulWith(f64)).Op)(other); } } -// ✅ Allowed: uses `Meters as MultipliableWith(T)` impl +// ✅ Allowed: uses `Meters as MulWith(T)` impl // with `T == f32` since `f32 impls ImplicitAs(f64)`. var now_allowed: Meters = height * scale; ``` @@ -5504,12 +6518,12 @@ defining operator overloads, Carbon has the `like` operator. This operator can only be used in the type or facet type part of an `impl` declaration, as part of a forward declaration or definition, in a place of a type. -``` +```carbon // Notice `f64` has been replaced by `like f64` // compared to "implementation one" above. -impl Meters as MultipliableWith(like f64) +impl Meters as MulWith(like f64) where .Result = Meters { - fn Multiply[self: Self](other: f64) -> Result { + fn Op[self: Self](other: f64) -> Result { return self.Scale(other); } } @@ -5521,19 +6535,30 @@ equivalent to "implementation one". The second implementation replaces the `like f64` with a parameter that ranges over types that can be implicitly converted to `f64`, equivalent to "implementation two". +> **Note:** We have decided to change the following in +> [a discussion on 2023-07-13](https://docs.google.com/document/d/1gnJBTfY81fZYvI_QXjwKk1uQHYBNHGqRLI2BS_cYYNQ/edit?resourcekey=0-ql1Q1WvTcDvhycf8LbA9DQ#heading=h.rs7m0kytcl4t). +> The new approach is to have one parameterized implementation replacing all of +> the `like` expressions on the left of the `as`, and another replacing all of +> the `like` expressions on the right of the `as`. However, in +> [a discussion on 2023-07-20](https://docs.google.com/document/d/1gnJBTfY81fZYvI_QXjwKk1uQHYBNHGqRLI2BS_cYYNQ/edit?resourcekey=0-ql1Q1WvTcDvhycf8LbA9DQ#heading=h.msdqbemd6axi), +> we decided that this change would not affect how we handle nested `like` +> expressions: `like Vector(like i32)` is still `like Vector(i32)` plus +> `Vector(like i32)`. These changes have not yet gone through the proposal +> process. + In general, each `like` adds one additional parameterized implementation. There is always the impl defined with all of the `like` expressions replaced by their arguments with the definition supplied in the source code. In addition, for each `like` expression, there is an automatic `impl` definition with it replaced by a new parameter. These additional automatic implementations will delegate to the -main impl, which will trigger implicit conversions according to +main `impl` definition, which will trigger implicit conversions according to [Carbon's ordinary implicit conversion rules](/docs/design/expressions/implicit_conversions.md). In this example, there are two uses of `like`, producing three implementations -``` -impl like Meters as MultipliableWith(like f64) +```carbon +impl like Meters as MulWith(like f64) where .Result = Meters { - fn Multiply[self: Self](other: f64) -> Result { + fn Op[self: Self](other: f64) -> Result { return self.Scale(other); } } @@ -5541,63 +6566,61 @@ impl like Meters as MultipliableWith(like f64) is equivalent to "implementation one", "implementation two", and: -``` +```carbon impl forall [T:! ImplicitAs(Meters)] - T as MultipliableWith(f64) where .Result = Meters { - fn Multiply[self: Self](other: f64) -> Result { - // Will implicitly convert `self` to `Meters` in order to - // match the signature of this `Multiply` method. - return self.(Meters.(MultipliableWith(f64).Multiply))(other); + T as MulWith(f64) where .Result = Meters { + fn Op[self: Self](other: f64) -> Result { + // Will implicitly convert `self` to `Meters` in + // order to match the signature of this `Op` method. + return self.((Meters as MulWith(f64)).Op)(other); } } ``` -`like` may be used in forward declarations in a way analogous to impl +`like` may be used in `impl` forward declarations in a way analogous to `impl` definitions. -``` -impl like Meters as MultipliableWith(like f64) +```carbon +impl like Meters as MulWith(like f64) where .Result = Meters; } ``` is equivalent to: -``` +```carbon // All `like`s removed. Same as the declaration part of // "implementation one", without the body of the definition. -impl Meters as MultipliableWith(f64) - where .Result = Meters; +impl Meters as MulWith(f64) where .Result = Meters; // First `like` replaced with a wildcard. impl forall [T:! ImplicitAs(Meters)] - T as MultipliableWith(f64) where .Result = Meters; + T as MulWith(f64) where .Result = Meters; // Second `like` replaced with a wildcard. Same as the // declaration part of "implementation two", without the // body of the definition. impl forall [T:! ImplicitAs(f64)] - Meters as MultipliableWith(T) where .Result = Meters; + Meters as MulWith(T) where .Result = Meters; ``` -In addition, the generated impl definition for a `like` is implicitly injected -at the end of the (unique) source file in which the impl is first declared. That -is, it is injected in the API file if the impl is declared in an API file, and -in the sole impl file declaring the impl otherwise. This means an `impl` -declaration using `like` in an API file also makes the parameterized definition +In addition, the generated `impl` definition for a `like` is implicitly injected +at the end of the (unique) source file in which the `impl` is defined. That is, +it is injected in the API file if the `impl` definition is in an API file, and +in the sole impl file with the `impl` definition otherwise. If one `impl` declaration uses `like`, other declarations must use `like` in the same way to match. The `like` operator may be nested, as in: -``` +```carbon impl like Vector(like String) as Printable; ``` Which will generate implementations with declarations: -``` +```carbon impl Vector(String) as Printable; impl forall [T:! ImplicitAs(Vector(String))] T as Printable; impl forall [T:! ImplicitAs(String)] Vector(T) as Printable; @@ -5611,7 +6634,7 @@ example, there existing an implicit conversion from `T` to `String` does not imply that there is one from `Vector(T)` to `Vector(String)`, so the following use of `like` is illegal: -``` +```carbon // ❌ Illegal: Can't convert a value with type // `Vector(T:! ImplicitAs(String))` // to `Vector(String)` for `self` @@ -5626,7 +6649,7 @@ The argument to `like` must either not mention any type parameters, or those parameters must be able to be determined due to being repeated outside of the `like` expression. -``` +```carbon // ✅ Allowed: no parameters impl like Meters as Printable; @@ -5636,24 +6659,24 @@ impl forall [T:! IntLike] like T as Printable; // ❌ Illegal: `T` being used in a `where` clause // is insufficient. impl forall [T:! IntLike] like T - as MultipliableWith(i64) where .Result = T; + as MulWith(i64) where .Result = T; // ❌ Illegal: `like` can't be used in a `where` // clause. -impl Meters as MultipliableWith(f64) +impl Meters as MulWith(f64) where .Result = like Meters; // ✅ Allowed: `T` can be determined by another // part of the query. impl forall [T:! IntLike] like T - as MultipliableWith(T) where .Result = T; + as MulWith(T) where .Result = T; impl forall [T:! IntLike] T - as MultipliableWith(like T) where .Result = T; + as MulWith(like T) where .Result = T; // ✅ Allowed: Only one `like` used at a time, so this // is equivalent to the above two examples. impl forall [T:! IntLike] like T - as MultipliableWith(like T) where .Result = T; + as MulWith(like T) where .Result = T; ``` ## Parameterized types @@ -5661,35 +6684,35 @@ impl forall [T:! IntLike] like T Generic types may be defined by giving them compile-time parameters. Those parameters may be used to specify types in the declarations of its members, such as data fields, member functions, and even interfaces being implemented. For -example, a container type might be parameterized by the type of its elements: +example, a container type might be parameterized by a facet describing the type +of its elements: -**FIXME: member functions may have additional parameters.** - -``` +```carbon class HashMap( - KeyType:! Hashable & EqualityComparable & Movable, - ValueType:! Movable) { - // `Self` is `HashMap(KeyType, ValueType)`. + KeyT:! Hashable & Eq & Movable, + ValueT:! Movable) { + // `Self` is `HashMap(KeyT, ValueT)`. - // Parameters may be used in function signatures. - fn Insert[addr self: Self*](k: KeyType, v: ValueType); + // Class parameters may be used in function signatures. + fn Insert[addr self: Self*](k: KeyT, v: ValueT); - // Parameters may be used in field types. - private var buckets: Vector((KeyType, ValueType)); + // Class parameters may be used in field types. + private var buckets: DynArray((KeyT, ValueT)); - // Parameters may be used in interfaces implemented. - extend impl as Container where .ElementType = (KeyType, ValueType); - extend impl as ComparableWith(HashMap(KeyType, ValueType)); + // Class parameters may be used in interfaces implemented. + extend impl as Container where .ElementType = (KeyT, ValueT); + impl as OrderedWith(HashMap(KeyT, ValueT)); } ``` -Note that, unlike functions, every parameter to a type must be compile-time, -either symbolic using `:!` or template using `template...:!`, not dynamic, with -a plain `:`. +Note that, unlike functions, every parameter to a type must be a compile-time +binding, either symbolic using `:!` or template using `template`...`:!`, not +runtime, with a plain `:`. -Two types are the same if they have the same name and the same arguments. -Carbon's [manual type equality](#manual-type-equality) approach means that the -compiler may not always be able to tell when two +Two types are the same if they have the same name and the same arguments, after +applying aliases and [rewrite constraints](#rewrite-constraints). Carbon's +[manual type equality](#manual-type-equality) approach means that the compiler +may not always be able to tell when two [type expressions](terminology.md#type-expression) are equal without help from the user, in the form of [`observe` declarations](#observe-declarations). This means Carbon will not in general be able to determine when types are unequal. @@ -5697,20 +6720,67 @@ means Carbon will not in general be able to determine when types are unequal. Unlike an [interface's parameters](#parameterized-interfaces), a type's parameters may be [deduced](terminology.md#deduced-parameter), as in: -``` -fn ContainsKey[KeyType:! Movable, ValueType:! Movable] - (haystack: HashMap(KeyType, ValueType), needle: KeyType) +```carbon +fn ContainsKey[KeyT:! Movable, ValueT:! Movable] + (haystack: HashMap(KeyT, ValueT), needle: KeyT) -> bool { ... } fn MyMapContains(s: String) { var map: HashMap(String, i32) = (("foo", 3), ("bar", 5)); - // ✅ Deduces `KeyType` = `String` from the types of both arguments. - // Deduces `ValueType` = `i32` from the type of the first argument. + // ✅ Deduces `KeyT` = `String as Movable` from the types of both arguments. + // Deduces `ValueT` = `i32 as Movable` from the type of the first argument. return ContainsKey(map, s); } ``` Note that restrictions on the type's parameters from the type's declaration can -be [implied constraints](#implied-constraints) on the function's parameters. +be [implied constraints](#implied-constraints) on the function's parameters. In +the above example, the `KeyT` parameter to `ContainsKey` gets `Hashable & Eq` +implied constraints from the declaration of the corresponding parameter to +`HashMap`. + +> **Future work:** We may want to support optional deduced parameters in square +> brackets `[`...`]` before the explicit parameters in round parens `(`...`)`. + +> **References:** This feature is from +> [proposal #1146: Generic details 12: parameterized types](https://github.com/carbon-language/carbon-lang/pull/1146). + +### Generic methods + +A generic type may have methods with additional compile-time parameters. For +example, this `Set(T)` type may be compared to anything implementing the +`Container` interface as long as the element types match: + +```carbon +class Set(T:! Ordered) { + fn Less[U:! Container with .ElementType = T, self: Self](u: U) -> bool; + // ... +} +``` + +The `Less` method is parameterized both by the `T` parameter to the `Set` type +and its own `U` parameter deduced from the type of its first argument. + +### Conditional methods + +A method could be defined conditionally for a generic type by using a more +specific type in place of `Self` in the method declaration. For example, this is +how to define a dynamically sized array type that only has a `Sort` method if +its elements implement the `Ordered` interface: + +```carbon +class DynArray(T:! type) { + // `DynArray(T)` has a `Sort()` method if `T impls Ordered`. + fn Sort[C:! Ordered, addr self: DynArray(C)*](); +} +``` + +**Comparison with other languages:** In +[Rust](https://doc.rust-lang.org/book/ch10-02-traits.html#using-trait-bounds-to-conditionally-implement-methods) +this feature is part of conditional conformance. Swift supports conditional +methods using +[conditional extensions](https://docs.swift.org/swift-book/LanguageGuide/Generics.html#ID553) +or +[contextual where clauses](https://docs.swift.org/swift-book/LanguageGuide/Generics.html#ID628). ### Specialization @@ -5732,7 +6802,7 @@ single byte. Clients of the optional library may want to add additional specializations for their own types. We make an interface that represents "the storage of `Optional(T)` for type `T`," written here as `OptionalStorage`: -``` +```carbon interface OptionalStorage { let Storage:! type; fn MakeNone() -> Storage; @@ -5745,7 +6815,7 @@ interface OptionalStorage { The default implementation of this interface is provided by a [blanket implementation](#blanket-impl-declarations): -``` +```carbon // Default blanket implementation impl forall [T:! Movable] T as OptionalStorage where .Storage = (bool, T) { @@ -5757,7 +6827,7 @@ This implementation can then be [specialized](#lookup-resolution-and-specialization) for more specific type patterns: -``` +```carbon // Specialization for pointers, using nullptr == None final impl forall [T:! type] T* as OptionalStorage where .Storage = Array(Byte, sizeof(T*)) { @@ -5774,7 +6844,7 @@ Further, libraries can implement `OptionalStorage` for their own types, assuming the interface is not marked `private`. Then the implementation of `Optional(T)` can delegate to `OptionalStorage` for anything that can vary with `T`: -``` +```carbon class Optional(T:! Movable) { fn None() -> Self { return {.storage = T.(OptionalStorage.MakeNone)()}; @@ -5794,7 +6864,7 @@ implementation of `OptionalStorage` exists for `T`. Carbon does not require callers of `Optional`, even checked-generic callers, to specify that the argument type implements `OptionalStorage`: -``` +```carbon // ✅ Allowed: `T` just needs to be `Movable` to form `Optional(T)`. // A `T:! OptionalStorage` constraint is not required. fn First[T:! Movable & Eq](v: Vector(T)) -> Optional(T); @@ -5808,7 +6878,7 @@ In this example, a `let` is used to avoid repeating `OptionalStorage` in the definition of `Optional`, since it has no name conflicts with the members of `Movable`: -``` +```carbon class Optional(T:! Movable) { private let U:! Movable & OptionalStorage = T; fn None() -> Self { @@ -5822,6 +6892,9 @@ class Optional(T:! Movable) { } ``` +> **Alternative considered:** Direct support for specialization of types was +> considered in [proposal #1146](/proposals/p1146.md#alternatives-considered). + ## Future work ### Dynamic types @@ -5910,23 +6983,18 @@ See details in [the goals document](goals.md#bridge-for-c-customization-points). Some facility for allowing a function to take a variable number of arguments, with the [definition checked](terminology.md#complete-definition-checking) -independent of calls. +independent of calls. Open +[proposal #2240](https://github.com/carbon-language/carbon-lang/pull/2240) is +adding this feature. -### Range constraints on symbolic integers +### Value constraints for template parameters -We currently only support `where` clauses on facet types. We may want to also -support constraints on symbolic integers. The constraint with the most expected -value is the ability to do comparisons like `<`, or `>=`. For example, you might -constrain the `N` member of [`NSpacePoint`](#associated-constants) using an -expression like `PointT:! NSpacePoint where 2 <= .N and .N <= 3`. - -The concern here is supporting this at compile time with more benefit than -complexity. For example, we probably don't want to support integer-range based -types at runtime, and there are also concerns about reasoning about comparisons -between multiple symbolic integer parameters. For example, if `J < K` and -`K <= L`, can we call a function that requires `J < L`? There is also a -secondary syntactic concern about how to write this kind of constraint on a -parameter, as opposed to an associated facet, as in `N:! u32 where ___ >= 2`. +We have planned support for predicates that constrain the value of non-facet +template parameters. For example, we might support a predicate that constrains +an integer to live inside a specified range. See +[question-for-leads issue #2153: Checked generics calling templates](https://github.com/carbon-language/carbon-lang/issues/2153) +and +[future work in proposal #2200: Template generics](/proposals/p2200.md#predicates-constraints-on-values). ## References @@ -5947,12 +7015,14 @@ parameter, as opposed to an associated facet, as in `N:! u32 where ___ >= 2`. - [#1327: Generics: `impl forall`](https://github.com/carbon-language/carbon-lang/pull/1327) - [#2107: Clarify rules around `Self` and `.Self`](https://github.com/carbon-language/carbon-lang/pull/2107) - [#2138: Checked and template generic terminology](https://github.com/carbon-language/carbon-lang/pull/2138) +- [Issue #2153: Checked generics calling templates](https://github.com/carbon-language/carbon-lang/issues/2153) - [#2173: Associated constant assignment versus equality](https://github.com/carbon-language/carbon-lang/pull/2173) - [#2200: Template generics](https://github.com/carbon-language/carbon-lang/pull/2200) - [#2347: What can be done with an incomplete interface](https://github.com/carbon-language/carbon-lang/pull/2347) - [#2360: Types are values of type `type`](https://github.com/carbon-language/carbon-lang/pull/2360) - [#2376: Constraints must use `Self`](https://github.com/carbon-language/carbon-lang/pull/2376) - [#2483: Replace keyword `is` with `impls`](https://github.com/carbon-language/carbon-lang/pull/2483) +- [#2687: Termination algorithm for impl selection](https://github.com/carbon-language/carbon-lang/pull/2687) - [#2760: Consistent `class` and `interface` syntax](https://github.com/carbon-language/carbon-lang/pull/2760) - [#2964: Expression phase terminology](https://github.com/carbon-language/carbon-lang/pull/2964) - [#3162: Reduce ambiguity in terminology](https://github.com/carbon-language/carbon-lang/pull/3162) From 4b13d2cccda95bd40f139b2ae341ab39d2f719ba Mon Sep 17 00:00:00 2001 From: Josh L Date: Fri, 22 Sep 2023 21:43:52 +0000 Subject: [PATCH 02/19] Checkpoint progress. --- docs/design/generics/details.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 74f86e71e852f..6058a0af8d308 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -5580,7 +5580,7 @@ An incomplete `C` cannot be used in the following contexts: > same name, as we do with `A & B`, then we don't need to require `C` to be > complete. > - Another option, being discussed in -> [#2355](https://github.com/carbon-language/carbon-lang/issues/2355), is +> [#2745](https://github.com/carbon-language/carbon-lang/issues/2745), is > that names in interface `I` shadow the names in any interface being > extended, then `C` would not be required to be complete. From 6671c69c355d13d2d58fbe33876be17f09679c37 Mon Sep 17 00:00:00 2001 From: Josh L Date: Sat, 23 Sep 2023 16:08:50 +0000 Subject: [PATCH 03/19] Add reference to #2880 --- docs/design/generics/details.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 6058a0af8d308..ae3c39201ef3f 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -5220,6 +5220,18 @@ let U:! B = bool; let V:! B = i32; ``` + + + + +> **Note:** +> [Issue #2880](https://github.com/carbon-language/carbon-lang/issues/2880) is a +> tracking bug for known issues with this "strictly more complex" rule for +> `impl` termination. We are using that issue to track any code that arises in +> practice that would terminate but is rejected by this rule. + + + > **Comparison with other languages:** Rust solves this problem by imposing a > recursion limit, much like C++ compilers use to terminate template recursion. > This goes against From c59f56ed6d0d96b0a82002ad168e259211c52baf Mon Sep 17 00:00:00 2001 From: Josh L Date: Sat, 23 Sep 2023 16:19:23 +0000 Subject: [PATCH 04/19] Checkpoint progress. --- docs/design/generics/details.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index ae3c39201ef3f..0922ca957c4fa 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -6556,7 +6556,8 @@ converted to `f64`, equivalent to "implementation two". > we decided that this change would not affect how we handle nested `like` > expressions: `like Vector(like i32)` is still `like Vector(i32)` plus > `Vector(like i32)`. These changes have not yet gone through the proposal -> process. +> process, and we may decide to reject nested `like` until we have a +> demonstrated need. In general, each `like` adds one additional parameterized implementation. There is always the impl defined with all of the `like` expressions replaced by their From 98fafbdac4005e6e8787bee51232992f376daafa Mon Sep 17 00:00:00 2001 From: josh11b Date: Tue, 26 Sep 2023 13:10:31 -0700 Subject: [PATCH 05/19] Apply suggestions from code review Co-authored-by: Richard Smith --- docs/design/generics/details.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 0922ca957c4fa..8b890353c51b6 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -1206,7 +1206,7 @@ type. For example, in C++, requires all containers to also satisfy the requirements of `DefaultConstructible`, `CopyConstructible`, `Eq`, and `Swappable`. This is already a capability for [facet types in general](#facet-types). For consistency -we will use the same semantics and `require Self impls` syntax as we do for +we use the same semantics and `require Self impls` syntax as we do for [named constraints](#named-constraints): ```carbon @@ -2481,7 +2481,7 @@ The result of applying a `where` operator to a facet type is another facet type. Note that this expands the kinds of requirements that facet types can have from just interface requirements to also include the various kinds of constraints discussed later in this section. In addition, it can introduce relationships -between different type variables, such as that a member of one is equal to the +between different type variables, such as that a member of one is equal to a member of another. The `where` operator is not associative, so a type expression using multiple must use round parens `(`...`)` to specify grouping. @@ -2536,9 +2536,9 @@ An implements constraint is written `where T impls C`, where `T` is a facet and `C` is a facet type. The constraint is that `T` satisfies the requirements of `C`. -**References:** The definition of rewrite and same-type constraints were +**References:** The definition of rewrite and same-type constraints were in [proposal #2173](https://github.com/carbon-language/carbon-lang/pull/2173). -Implements constraints switched using the `impls` keyword in +Implements constraints switched to using the `impls` keyword in [proposal #2483](https://github.com/carbon-language/carbon-lang/pull/2483). **Alternatives considered:** @@ -2571,7 +2571,7 @@ interface HasAbs { For types representing subsets of the real numbers, such as `i32` or `f32`, the `MagnitudeType` will match `Self`, the type implementing an interface. For types representing complex numbers, the types will be different. For example, the -`Abs()` applied to a `Complex64` value would produce a `f32` result. The goal is +`Abs()` function applied to a `Complex64` value would produce a `f32` result. The goal is to write a constraint to restrict to the first case. In a second example, when you take the slice of a type implementing `Container` @@ -2635,10 +2635,10 @@ constraint ContainerIsSlice { The `.Self` construct follows these rules: -- `X :!` introduces `.Self:! type`, where references to `.Self` are resolved. +- `X :!` introduces `.Self:! type`, where references to `.Self` are resolved to `X`. This allows you to use `.Self` as an interface parameter as in `X:! I(.Self)`. -- `A where` introduces `.Self:! A` and `.Foo` _designator_ for each member +- `A where` introduces `.Self:! A` and a `.Foo` _designator_ for each member `Foo` of `A`. - It's an error to reference `.Self` if it refers to more than one different thing or isn't a facet. From 3524ec678ae11eb94b119b9556d1fc855bec89a7 Mon Sep 17 00:00:00 2001 From: Josh L Date: Tue, 26 Sep 2023 20:50:00 +0000 Subject: [PATCH 06/19] Changes prompted by review feedback --- docs/design/generics/details.md | 94 +++++++++++++++++++++------------ 1 file changed, 59 insertions(+), 35 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 8b890353c51b6..ccd55c171da9b 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -54,8 +54,8 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception - [Rewrite constraints](#rewrite-constraints) - [Combining constraints with `&`](#combining-constraints-with-) - [Combining constraints with `and`](#combining-constraints-with-and) - - [Combining constraints with `extends`](#combining-constraints-with-extends) - - [Combining constraints with `impl as` and `impls`](#combining-constraints-with-impl-as-and-impls) + - [Combining constraints with `extend`](#combining-constraints-with-extend) + - [Combining constraints with `require` and `impls`](#combining-constraints-with-require-and-impls) - [Rewrite constraint resolution](#rewrite-constraint-resolution) - [Precise rules and termination](#precise-rules-and-termination) - [Qualified name lookup](#qualified-name-lookup) @@ -1200,8 +1200,8 @@ the discussion. ## Interface requiring other interfaces -Some interfaces will depend on other interfaces being implemented for the same -type. For example, in C++, +Some interfaces depend on other interfaces being implemented for the same type. +For example, in C++, [the `Container` concept](https://en.cppreference.com/w/cpp/named_req/Container#Other_requirements) requires all containers to also satisfy the requirements of `DefaultConstructible`, `CopyConstructible`, `Eq`, and `Swappable`. This is @@ -1259,9 +1259,9 @@ def DoHashAndEquals[T:! Hashable](x: T) { ### Interface extension -When implementing an interface, we should allow implementing the aliased names -as well. In the case of `Hashable` above, this includes all the members of -`Equatable`, obviating the need to implement `Equatable` itself: +When implementing an interface, we allow implementing the aliased names as well. +In the case of `Hashable` above, this includes all the members of `Equatable`, +obviating the need to implement `Equatable` itself: ```carbon class Song { @@ -2551,7 +2551,7 @@ Implements constraints switched to using the `impls` keyword in - [Different syntax for same-type constraint](/proposals/p2173.md#different-syntax-for-same-type-constraint) - [Required ordering for rewrites](/proposals/p2173.md#required-ordering-for-rewrites) - [Multi-constraint `where` clauses](/proposals/p2173.md#multi-constraint-where-clauses) -- [Rewrite constraints in `impl as` constraints](/proposals/p2173.md#rewrite-constraints-in-impl-as-constraints) +- [Rewrite constraints in `require` constraints](/proposals/p2173.md#rewrite-constraints-in-impl-as-constraints) #### Recursive constraints @@ -2571,8 +2571,8 @@ interface HasAbs { For types representing subsets of the real numbers, such as `i32` or `f32`, the `MagnitudeType` will match `Self`, the type implementing an interface. For types representing complex numbers, the types will be different. For example, the -`Abs()` function applied to a `Complex64` value would produce a `f32` result. The goal is -to write a constraint to restrict to the first case. +`Abs()` function applied to a `Complex64` value would produce a `f32` result. +The goal is to write a constraint to restrict to the first case. In a second example, when you take the slice of a type implementing `Container` you get a type implementing `Container` which may or may not be the same type as @@ -2602,6 +2602,7 @@ defined. ```carbon interface Container { let ElementType:! type; + let IteratorType:! Iterator where .ElementType = ElementType; let SliceType:! Container where .ElementType = ElementType and @@ -2617,19 +2618,26 @@ interface Container { Note that [naming](#named-constraint-constants) a recursive constraint using the [`constraint` introducer](#named-constraints) approach, we can name the implementing type using `Self` instead of `.Self`, since they refer to the same -type: +type. Note though they are different facets with different facet types: ```carbon constraint RealAbs { extend HasAbs where .MagnitudeType = Self; - // Equivalent to: + // Satisfied by the same types: extend HasAbs where .MagnitudeType = .Self; + + // While `Self as type` is the same as `.Self as type`, + // they are different as facets: `Self` has type + // `RealAbs` and `.Self` has type `HasAbs`. } constraint ContainerIsSlice { extend Container where .SliceType = Self; - // Equivalent to: + // Satisfied by the same types: extend Container where .SliceType = .Self; + + // `Self` has type `ContainerIsSlice` and + // `.Self` has type `Container`. } ``` @@ -2658,6 +2666,22 @@ fn F[T:! InterfaceA where .A impls (InterfaceB where .B = .Self)](x: T); ``` +These two meanings can be disambiguated by defining a +[`constraint`](#named-constraints): + +```carbon +constraint InterfaceBWithSelf { + extend InterfaceB where .B = Self; +} +constraint InterfaceBWith(U:! InterfaceA) { + extend InterfaceB where .B = U; +} +// `T.A impls InterfaceB where .B = T.A` +fn F[T:! InterfaceA where .A impls InterfaceBWithSelf](x: T); +// `T.A impls InterfaceB where .B = T` +fn F[T:! InterfaceA where .A impls InterfaceBWith(.Self)](x: T); +``` + #### Rewrite constraints In a rewrite constraint, the left-hand operand of `=` must be a `.` followed by @@ -2781,9 +2805,9 @@ fn F[A:! C where .T = M and .U = .T.Me]() {} fn F[A:! C where .U = .T.Me and .T = M]() {} ``` -##### Combining constraints with `extends` +##### Combining constraints with `extend` -Within an interface or named constraint, `extends` can be used to extend a +Within an interface or named constraint, `extend` can be used to extend a constraint that has rewrites. ```carbon @@ -2792,7 +2816,7 @@ interface A { let U:! type; } interface B { - extends A where .T = .U and .U = i32; + extend A where .T = .U and .U = i32; } var n: i32; @@ -2803,9 +2827,9 @@ var n: i32; fn F(T:! B) -> T.(A.T) { return n; } ``` -##### Combining constraints with `impl as` and `impls` +##### Combining constraints with `require` and `impls` -Within an interface or named constraint, the `impl T as C` syntax does not +Within an interface or named constraint, the `require T impls C` syntax does not permit `=` constraints to be specified directly. However, such constraints can be specified indirectly, for example if `C` is a named constraint that contains rewrites. Because these constraints don't change the type of `T`, rewrite @@ -2818,15 +2842,15 @@ interface A { let U:! type; } constraint C { - extends A where .T = .U and .U = i32; + extend A where .T = .U and .U = i32; } constraint D { - extends A where .T == .U and .U == i32; + extend A where .T == .U and .U == i32; } interface B { - // OK, equivalent to `impl as D;` or - // `impl as A where .T == .U and .U == i32;`. - impl as C; + // OK, equivalent to `require Self impls D;` or + // `require Self impls A where .T == .U and .U == i32;`. + require Self impls C; } var n: i32; @@ -2847,8 +2871,8 @@ an expression: - If an `=` constraint is specified directly in an operand of an `&` or `(`...`)`, then it is specified directly in that enclosing expression. -In an `impl as C` or `impl T as C` declaration in an interface or named -constraint, `C` is not allowed to directly specify any `=` constraints: +In an `require Self impls C` or `require T impls C` declaration in an interface +or named constraint, `C` is not allowed to directly specify any `=` constraints: ```carbon // Compile-time identity function. @@ -2856,18 +2880,18 @@ fn Identity[T:! type](x:! T) -> T { return x; } interface E { // ❌ Rewrite constraint specified directly. - impl as A where .T = .U and .U = i32; + require Self impls A where .T = .U and .U = i32; // ❌ Rewrite constraint specified directly. - impl as type & (A where .T = .U and .U = i32); + require Self impls type & (A where .T = .U and .U = i32); // ✅ Not specified directly, but does not result // in any rewrites being performed. - impl as Identity(A where .T = .U and .U = i32); + require Self impls Identity(A where .T = .U and .U = i32); } ``` -The same rules apply to `impls` constraints. Note that `.T == U` constraints are -also not allowed in this context, because the reference to `.T` is rewritten to -`.Self.T`, and `.Self` is ambiguous. +The same rules apply to `where`...`impls` constraints. Note that `.T == U` +constraints are also not allowed in this context, because the reference to `.T` +is rewritten to `.Self.T`, and `.Self` is ambiguous. ```carbon // ❌ Rewrite constraint specified directly in `impls`. @@ -2899,7 +2923,7 @@ constraints that apply to `T`. This happens: `T:! Constraint`. - When declaring that a type implements a constraint with an `impl` declaration, such as `impl T as Constraint`. Note that this does not include - `impl ... as` constraints appearing in `interface` or `constraint` + `require` ... `impls` constraints appearing in `interface` or `constraint` declarations. In each case, the following steps are performed to resolve the facet type's @@ -3226,7 +3250,7 @@ interface Container { let Element:! type; } interface SliceableContainer { - extends Container; + extend Container; let Slice:! Container where .Element = Self.(Container.Element); } // ❌ Qualified name lookup rewrites this facet type to @@ -3260,7 +3284,7 @@ interface AllowedBase { let A:! Allowed; } interface Allowed { - extends AllowedBase where .A = .Self; + extend AllowedBase where .A = .Self; } // ✅ The final type of `x` is `T`. It is computed as follows: // In `((T.A).A).A`, the inner `T.A` is rewritten to `T`, @@ -3278,7 +3302,7 @@ interface MoveYsRight { let Y:! ForwardDeclaredConstraint(X); } constraint ForwardDeclaredConstraint(X:! MoveYsRight) { - extends MoveYsRight where .X = X.Y; + extend MoveYsRight where .X = X.Y; } // ✅ The final type of `x` is `T.X.Y.Y`. It is computed as follows: // The type of `T` is `MoveYsRight`. From f60ad2738aad05db0585cfa00d96a614eea02e11 Mon Sep 17 00:00:00 2001 From: josh11b Date: Tue, 26 Sep 2023 14:34:31 -0700 Subject: [PATCH 07/19] Apply suggestions from code review Co-authored-by: Richard Smith --- docs/design/generics/details.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index ccd55c171da9b..eb6dfb05c1329 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -2857,7 +2857,7 @@ var n: i32; // ❌ No implicit conversion from `i32` to `T.(A.T)`. // Resolved constraint on `T` is -// `B where T.(A.T) == T.(A.U) and T.(A.U) = i32`. +// `B where T.(A.T) == T.(A.U) and T.(A.U) == i32`. // `T.(A.T)` is single-step equal to `T.(A.U)`, and // `T.(A.U)` is single-step equal to `i32`, but // `T.(A.T)` is not single-step equal to `i32`. @@ -2918,7 +2918,7 @@ When a facet type is used as the declared type of a facet `T`, the constraints that were specified within that facet type are _resolved_ to determine the constraints that apply to `T`. This happens: -- When the constraint is used explicitly, when declaring symbolic binding, +- When the constraint is used explicitly when declaring a symbolic binding, like a generic parameter or associated constant, of the form `T:! Constraint`. - When declaring that a type implements a constraint with an `impl` @@ -3645,7 +3645,7 @@ Only the current type is searched for interface implementations, so the call to `InR()` would be illegal without the cast. However, an [`observe`...`==`...`impls` declaration](#observing-equal-to-a-type-implementing-an-interface) can be used to identify interfaces that must be implemented through some equal -type. This does not [extending](terminology.md#extending-an-impl) the API of the +type. This does not [extend](terminology.md#extending-an-impl) the API of the type, that is solely determined by the definition of the type. Continuing the previous example: @@ -3712,7 +3712,7 @@ fn SortContainer In contrast to a [rewrite constraint](#rewrite-constraints) or a [same-type constraint](#same-type-constraints), this does not say what type -`ElementType` exactly is, just that it must satisfy requirements of some facet +`ElementType` exactly is, just that it must satisfy the requirements of some facet type. > **Note:** `Container` defines `ElementType` as having type `type`, but @@ -3872,7 +3872,7 @@ unless there is some declaration like `observe CT.ElementType == SC.ElementType impls Ordered`. Even then, the items from the `needles` container won't directly have a `Compare` method member. -The rule is that an same-type `where` constraint between two type variables does +The rule is that a same-type `where` constraint between two type variables does not modify the set of member names of either type. This is in contrast to rewrite constraints like `where .ElementType = String` with a `=`, then `.ElementType` is actually set to `String` including the complete `String` API. @@ -4595,7 +4595,7 @@ This may also be called a _generic `impl` declaration_. ### Impl for a parameterized type Interfaces may be implemented for a [parameterized type](#parameterized-types). -This can be done lexically in the class' scope: +This can be done lexically in the class's scope: ```carbon class Vector(T:! type) { @@ -6122,7 +6122,7 @@ interface CommonTypeWith(T:! type) { says that if `Self` implements `CommonTypeWith(T)`, then `T` must implement `CommonTypeWith(Self)`. -An `require`...`impls` constraint in an `interface`, or `constraint`, definition +A `require`...`impls` constraint in an `interface`, or `constraint`, definition must still use `Self` in some way. It can be an argument to either the [type](#parameterized-types) or [interface](#parameterized-interfaces). For example: From ba68926bf756519503c4da096f4f2259b76ba78f Mon Sep 17 00:00:00 2001 From: Josh L Date: Tue, 26 Sep 2023 21:35:02 +0000 Subject: [PATCH 08/19] Fix formatting --- docs/design/generics/details.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index eb6dfb05c1329..96f0ba516848f 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -3712,8 +3712,8 @@ fn SortContainer In contrast to a [rewrite constraint](#rewrite-constraints) or a [same-type constraint](#same-type-constraints), this does not say what type -`ElementType` exactly is, just that it must satisfy the requirements of some facet -type. +`ElementType` exactly is, just that it must satisfy the requirements of some +facet type. > **Note:** `Container` defines `ElementType` as having type `type`, but > `ContainerType.ElementType` has type `Ordered`. This is because From 695d08e107c22355a1ad839e24f609757da01cff Mon Sep 17 00:00:00 2001 From: Josh L Date: Wed, 27 Sep 2023 21:14:21 +0000 Subject: [PATCH 09/19] Implement suggestions from review --- docs/design/generics/details.md | 69 ++++++++++++++++++++++----------- 1 file changed, 47 insertions(+), 22 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 96f0ba516848f..8344015b04ca7 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -3355,11 +3355,18 @@ symbolic expression that refers to them. Same-type constraints are brought into scope, looked up, and resolved exactly as if there were a `SameAs(U:! type)` interface and a `T == U` impl corresponded to -`T is SameAs(U)`, except that `==` is commutative. As such, it's not possible to -ask for a list of types that are the same as a given type, nor to ask whether -there exists a type that is the same as a given type and has some property. But -it is possible to ask whether two types are (non-transitively) known to be the -same. +`T is SameAs(U)`, except that `==` is commutative. + +Further, same-type equalities apply to type components, so that `X(A, B, C)` is +`SameType(X(D, E, F))` if we know that `A == D`, `B == E`, and `C == F`. Stated +differently, if `F` is any pure type function, `T impls SameAs(U)` implies +`F(T) impls SameAs(F(U))`. For example, if we know that `T == i32` then we also +have `Vector(T)` is single-step equal to `Vector(i32)`. + +This relationship is not transitive, though, so it's not possible to ask for a +list of types that are the same as a given type, nor to ask whether there exists +a type that is the same as a given type and has some property. But it is +possible to ask whether two types are (non-transitively) known to be the same. In order for same-type constraints to be useful, they must allow the two types to be treated as actually being the same in some context. This can be @@ -3715,11 +3722,18 @@ In contrast to a [rewrite constraint](#rewrite-constraints) or a `ElementType` exactly is, just that it must satisfy the requirements of some facet type. -> **Note:** `Container` defines `ElementType` as having type `type`, but -> `ContainerType.ElementType` has type `Ordered`. This is because -> `ContainerType` has type `Container where .ElementType impls Ordered`, not -> `Container`. This means we need to be a bit careful when talking about the -> type of `ContainerType` when there is a `where` clause modifying it. +The specific case of a clause of the form +`where .AssociatedFacet impls AConstraint`, where the constraint is applied to a +direct associated facet member of the facet type being constrained (similar to +the restriction on [rewrite constraints](#rewrite-constraints)), gets special +treatment. In this case, the type of the associated facet is +[combined](#combining-interfaces-by-anding-facet-types) with the constraint. In +the above example, `Container` defines `ElementType` as having type `type`, but +`ContainerType.ElementType` has type `type & Ordered` (which is equivalent to +`Ordered`). This is because `ContainerType` has type +`Container where .ElementType impls Ordered`, not `Container`. This means we +need to be a bit careful when talking about the type of `ContainerType` when +there is a `where` clause modifying it. An implements constraint can be applied to [`.Self`](#recursive-constraints), as in `I where .Self impls C`. This has the same requirements as `I & C`, but that @@ -4070,19 +4084,30 @@ the result to implement a specific interface. ```carbon // A parameterized type -class Vector(T:! type) { ... } +class DynArray(T:! type) { ... } -// The parameterized type `Vector` implements interface +interface Printable { fn Print[self: Self](); } + +// The parameterized type `DynArray` implements interface // `Printable` only for some arguments. -impl Vector(String) as Printable { ... } +impl DynArray(String) as Printable { ... } -// Constraint: `T` such that `Vector(T)` implements `Printable` +// Constraint: `T` such that `DynArray(T)` implements `Printable` fn PrintThree - [T:! type where Vector(.Self) impls Printable] + [T:! type where DynArray(.Self) impls Printable] (a: T, b: T, c: T) { - var v: Vector(T) = (a, b, c); - Print(v); + // Create a `DynArray(T)` of size 3. + var v: auto = DynArray(T).Make(a, b, c); + // Known to be implemented due to the constraint on `T`. + v.(Printable.Print)(); } + +// ✅ Allowed: `DynArray(String)` implements `Printable`. +let s: String = "Ai "; +PrintThree(s, s, s); +// ❌ Forbidden: `DynArray(i32)` doesn't implement `Printable`. +let i: i32 = 3; +PrintThree(i, i, i); ``` **Comparison with other languages:** This use case was part of the @@ -6000,16 +6025,16 @@ interface TotalOrder { The workaround for this restriction is to use a [blanket impl declaration](#blanket-impl-declarations) instead: -**FIXME: Is it sensible to have both a `require` and a blanket implementation? -Does the blanket implementation satisfy the requirement so you only need to -implement `TotalOrder`?** - ```carbon interface TotalOrder { fn TotalLess[self: Self](right: Self) -> bool; - require Self impls PartialOrder; + // No `require` declaration, since implementers of + // `TotalOrder` don't need to also implement + // `PartialOrder`, since an implementation is provided. } +// Any type that implements `TotalOrder` also has at +// least this implementation of `PartialOrder`: impl forall [T:! TotalOrder] T as PartialOrder { fn PartialLess[self: Self](right: Self) -> bool { return self.TotalLess(right); From 9a6a483c11d1de5c493a1bf1a6a39fce396d2a69 Mon Sep 17 00:00:00 2001 From: Josh L Date: Thu, 28 Sep 2023 03:46:48 +0000 Subject: [PATCH 10/19] Checkpoint progress. --- docs/design/generics/details.md | 125 ++++++++++++++++++++------------ 1 file changed, 78 insertions(+), 47 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 8344015b04ca7..c09b17c7f6537 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -3477,55 +3477,65 @@ fn F[T:! Transitive](t: T) { The compiler may have several different `where` clauses to consider, particularly when an interface has associated facets that recursively satisfy -the same interface. For example, given this interface `Commute`: +the same interface, or mutual recursion between multiple interfaces. For +example, given these `Edge` and `Node` interfaces (similar to those defined in +[the section on interfaces with cyclic references](#example-of-declaring-interfaces-with-cyclic-references), +but using `==` same-type constraints): ```carbon -interface Commute { - let X:! Commute; - // **FIXME: Not allowed (at least not by Explorer) - // since `Commute` is incomplete here.** - let Y:! Commute where .X == X.Y; - - fn GetX[self: Self]() -> X; - fn GetY[self: Self]() -> Y; - fn TakesXXY[self: Self](xxy: X.X.Y); -} - -// **FIXME: Maybe the following?** -interface Commute; -constraint Helper(T:! Commute); +interface Edge; +interface Node; -interface Commute { - let X:! Commute; - let Y:! Helper(X); +private constraint EdgeFor(NodeT:! Node); +private constraint NodeFor(EdgeT:! Edge); - fn GetX[self: Self]() -> X; - fn GetY[self: Self]() -> Y; - // **FIXME: Don't think it is legal to write `X.X.Y` here.** - fn TakesXXY[self: Self](xxy: X.X.Y); +interface Edge { + let N:! NodeFor(Self); + fn GetN[self: Self]() -> N; + // FIXME: delete fn HasN[self: Self](n: N) -> bool; +} +interface Node { + let E:! EdgeFor(Self); + fn GetE[self: Self]() -> EdgeT; + fn AddE[addr self: Self*](e: EdgeT); + fn NearN[self: Self](n: N) -> bool; } -constraint Helper(T:! Commute) { - extend Commute where .X == T.Y; +constraint EdgeFor(NodeT:! Node) { + extend Edge where .N == NodeT; +} +constraint NodeFor(EdgeT:! Edge) { + extend Node where .E == EdgeT; } ``` -and a function `H` taking a value with some type implementing this interface, -then the following would be legal statements in `H`: +and a function `H` taking a value with some type implementing the `Node` +interface, then the following would be legal statements in `H`: ```carbon -fn H[C: Commute](c: C) { - // ✅ Legal: argument has type `C.X.X.Y` - c.TakesXXY(c.GetX().GetX().GetY()); +fn H[N:! Node](n: N) { + // ✅ Legal: argument has type `N.E`, matches parameter + n.AddE(n.GetE()); - // ✅ Legal: argument has type `C.X.Y.X` which is equal - // to `C.X.X.Y` following only one `where` clause. - c.TakesXXY(c.GetX().GetY().GetX()); + // ✅ Legal: + // - argument has type `N.E.N` + // - `N.E` has type `EdgeFor(Self)` where `Self` + // is `N`, which means `Edge where .N == N` + // - so we have the constraint `N.E.N == N` + // - which means the argument type `N.E.N` + // is equal to the parameter type `N` using a + // single `==` constraint. + n.NearN(n.GetE().GetN()); - // ✅ Legal: cast is legal since it matches a `where` - // clause, and produces an argument that has type - // `C.X.Y.X`. - c.TakesXXY(c.GetY().GetX().GetX() as C.X.Y.X); + // ✅ Legal: + // - type `N.E.N.E.N` may be cast to `N.E.N` + // using a single `where ==` clause, either + // `(N.E.N).E.N == (N).E.N` or + // `N.E.(N.E.N) == N.E.(N)` + // - argument of type `N.E.N` may be passed to + // function expecting `N`, using a single + // `where ==` clause, as in the previous call. + n.NearN(n.GetE().GetN().GetE().GetN() as N.E.N); } ``` @@ -5831,11 +5841,11 @@ impl MyClass as Interface6 where _ { } ### Example of declaring interfaces with cyclic references -In this example, `Node` has an `EdgeType` associated facet that is constrained -to implement `Edge`, and `Edge` has a `NodeType` associated facet that is -constrained to implement `Node`. Furthermore, the `NodeType` of an `EdgeType` is -the original type, and the other way around. This is accomplished by naming and -then forward declaring the constraints that can't be stated directly: +In this example, `Node` has an `EdgeT` associated facet that is constrained to +implement `Edge`, and `Edge` has a `NodeT` associated facet that is constrained +to implement `Node`. Furthermore, the `NodeT` of an `EdgeT` is the original +type, and the other way around. This is accomplished by naming and then forward +declaring the constraints that can't be stated directly: ```carbon // Forward declare interfaces used in @@ -5850,25 +5860,46 @@ private constraint NodeFor(E:! Edge); // Define interfaces using named constraints. interface Edge { - let NodeType:! NodeFor(Self); - fn Head[self: Self]() -> NodeType; + let NodeT:! NodeFor(Self); + fn Head[self: Self]() -> NodeT; } interface Node { - let EdgeType:! EdgeFor(Self); - fn Edges[self: Self]() -> Vector(EdgeType); + let EdgeT:! EdgeFor(Self); + fn Edges[self: Self]() -> DynArray(EdgeT); } // Now that the interfaces are defined, can // refer to members of the interface, so it is // now legal to define the named constraints. constraint EdgeFor(N:! Node) { - extend Edge where .NodeType == N; + extend Edge where .NodeT = N; } constraint NodeFor(E:! Edge) { - extend Node where .EdgeType == E; + extend Node where .EdgeT = E; } ``` +> **Future work:** This approach has limitations. For example the compiler only +> knows `EdgeT` is convertible to `type` in the body of the `interface Node` +> definition, which may not be enough to satisfy the requirements to be an +> argument to `DynArray`. If this proves to be a problem, we may decided to +> expand what can be done with incomplete interfaces and types to allow the +> above to be written without the additional private constraints: +> +> ```carbon +> interface Node; +> +> interface Edge { +> let NodeT:! Node where .EdgeT = Self; +> fn Head[self: Self]() -> NodeT; +> } +> +> interface Node { +> let EdgeT:! Movable & Edge where .NodeT = Self; +> fn Edges[self: Self]() -> DynArray(EdgeT); +> } +> ``` + ### Interfaces with parameters constrained by the same interface To work around From b34a5fa99e42242ee093e5131c6f55a99d9ffc03 Mon Sep 17 00:00:00 2001 From: Josh L Date: Thu, 28 Sep 2023 16:44:04 +0000 Subject: [PATCH 11/19] Apply suggestions from review --- docs/design/generics/details.md | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index c09b17c7f6537..3a3534a9d534d 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -2829,12 +2829,11 @@ fn F(T:! B) -> T.(A.T) { return n; } ##### Combining constraints with `require` and `impls` -Within an interface or named constraint, the `require T impls C` syntax does not -permit `=` constraints to be specified directly. However, such constraints can -be specified indirectly, for example if `C` is a named constraint that contains -rewrites. Because these constraints don't change the type of `T`, rewrite -constraints in this context will never result in a rewrite being performed, and -instead are equivalent to `==` constraints. +Within an interface or named constraint, the `require T impls C` and +`require Self impls C` syntaxes do not change the type of `T` or `Self`, +respectively, so any `=` constraints that they specify do not result in rewrites +being performed when the type `T` or `Self` is later used. Such `=` constraints +are equivalent to `==` constraints: ```carbon interface A { @@ -2864,15 +2863,17 @@ var n: i32; fn F(T:! B) -> T.(A.T) { return n; } ``` -A purely syntactic check is used to determine if an `=` is specified directly in -an expression: +Because `=` constraints are effectively treated as `==` constraints in an +`require Self impls C` or `require T impls C` declaration in an interface or +named constraint, it is an error to specify such a `=` constraint directly in +`C`. A purely syntactic check is used to determine if an `=` is specified +directly in an expression: - An `=` constraint is specified directly in its enclosing `where` expression. - If an `=` constraint is specified directly in an operand of an `&` or `(`...`)`, then it is specified directly in that enclosing expression. -In an `require Self impls C` or `require T impls C` declaration in an interface -or named constraint, `C` is not allowed to directly specify any `=` constraints: +For example: ```carbon // Compile-time identity function. From da4c92a00e067b5c1a6fc3abb0afa7ed172c7c23 Mon Sep 17 00:00:00 2001 From: Josh L Date: Thu, 28 Sep 2023 19:03:02 +0000 Subject: [PATCH 12/19] `extend private adapt` --- docs/design/generics/details.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 3a3534a9d534d..9b96d1c734fea 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -1990,7 +1990,9 @@ This is used to record in the type system that some data has passed validation checks, like `ValidDate` with the same data layout as `Date`. Or to record the units associated with a value, such as `Seconds` versus `Milliseconds` or `Feet` versus `Meters`. We should have some way of restricting the casts between a type -and an adapter to address this use case. +and an adapter to address this use case. One possibility would be to add the +keyword `private` before `adpat`, so you might write +`extend private adapt Date;`. ## Associated constants From e5999e4a3ffee32b82dd87c13601ad9058311c18 Mon Sep 17 00:00:00 2001 From: Josh L Date: Thu, 28 Sep 2023 20:00:55 +0000 Subject: [PATCH 13/19] Replace Commute example with Graph example --- docs/design/generics/details.md | 39 +++++++++++++++++---------------- 1 file changed, 20 insertions(+), 19 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 9b96d1c734fea..14791c385667c 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -3592,17 +3592,22 @@ same-type `where` constraints. These `observe` declarations may be included in an `interface` definition or a function body, as in: ```carbon -// **FIXME: Not clear how to fix this example.** -interface Commute { - let X:! Commute; - let Y:! Commute where .X == X.Y; - ... - observe X.X.Y == X.Y.X == Y.X.X; +interface Edge { + let N:! type; +} +interface Node { + let E:! type; +} +interface Graph { + let E:! Edge; + let N:! Node where .E == E and E.N == .Self; + observe E == N.E == E.N.E == N.E.N.E; + // ... } -fn H[C: Commute](c: C) { - observe C.X.Y.Y == C.Y.X.Y == C.Y.Y.X; - ... +fn H[G: Graph](g: G) { + observe G.N == G.E.N == G.N.E.N == G.E.N.E.N; + // ... } ``` @@ -3611,19 +3616,15 @@ expression in the sequence by a single `where` equality constraint. In this example, ```carbon -// **FIXME: Not clear how to fix this example.** -interface Commute { - let X:! Commute; - let Y:! Commute where .X == X.Y; - ... - // ✅ Legal: - observe X.X.Y.Y == X.Y.X.Y == Y.X.X.Y == X.Y.Y.X; +fn J[G: Graph](g: G) { + observe G.E.N == G.N.E.N == G.N == G.E.N.E.N; + // ... } ``` -the expression `X.Y.Y.X` is one equality away from `X.Y.X.Y` and so it is -allowed. This is even though `X.Y.X.Y` isn't the type expression immediately -prior to `X.Y.Y.X`. +the expression `G.E.N.E.N` is one equality away from `G.N.E.N` and so it is +allowed. This is even though `G.N.E.N` isn't the type expression immediately +prior to `G.E.N.E.N`. After an `observe` declaration, all of the listed type expressions are considered equal to each other using a single `where` equality. In this example, From 71f33d6f87f0c4e4c26b4218de6bb4a4d8b6818b Mon Sep 17 00:00:00 2001 From: Josh L Date: Thu, 28 Sep 2023 20:02:48 +0000 Subject: [PATCH 14/19] Checkpoint progress. --- docs/design/generics/details.md | 1 - 1 file changed, 1 deletion(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 14791c385667c..e3f17420985a6 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -3495,7 +3495,6 @@ private constraint NodeFor(EdgeT:! Edge); interface Edge { let N:! NodeFor(Self); fn GetN[self: Self]() -> N; - // FIXME: delete fn HasN[self: Self](n: N) -> bool; } interface Node { let E:! EdgeFor(Self); From eff1b40ed0116aefcec336bb02941e22a8f27d93 Mon Sep 17 00:00:00 2001 From: Josh L Date: Thu, 28 Sep 2023 22:00:39 +0000 Subject: [PATCH 15/19] Move rewrite constraint details to appendix --- docs/design/generics/README.md | 7 +- .../generics/appendix-rewrite-constraints.md | 627 ++++++++++++++++++ docs/design/generics/details.md | 608 +---------------- 3 files changed, 636 insertions(+), 606 deletions(-) create mode 100644 docs/design/generics/appendix-rewrite-constraints.md diff --git a/docs/design/generics/README.md b/docs/design/generics/README.md index 999bea92b4624..fb00480e3bd3f 100644 --- a/docs/design/generics/README.md +++ b/docs/design/generics/README.md @@ -17,8 +17,11 @@ feature of Carbon: - [Terminology](terminology.md) - A glossary establishing common terminology for describing the design - [Detailed design](details.md) - In-depth description + - [Appendix: Coherence](appendix-coherence.md) - Describes the rationale + for Carbon's choice to have coherent generics, and the alternatives. + - [Appendix: Rewrite constraints](appendix-rewrite-constraints.md) - + Describes the detailed rules governing rewrite constraints, and why + resolving them terminates. - [Appendix: Witness tables](appendix-witness.md) - Describes an implementation strategy for checked generics, and Carbon's rationale for only using it for dynamic dispatch. - - [Appendix: Coherence](appendix-coherence.md) - Describes the rationale - for Carbon's choice to have coherent generics, and the alternatives. diff --git a/docs/design/generics/appendix-rewrite-constraints.md b/docs/design/generics/appendix-rewrite-constraints.md new file mode 100644 index 0000000000000..ff0c13fa3c718 --- /dev/null +++ b/docs/design/generics/appendix-rewrite-constraints.md @@ -0,0 +1,627 @@ +# Carbon: Rewrite constraint details + + + +This document explains the rationale for choosing to make +[implementation coherence](terminology.md#coherence) +[a goal for Carbon](goals.md#coherence), and the alternatives considered. + + + +## Table of contents + +- [Rewrite constraints](#rewrite-constraints) +- [Combining constraints with `&`](#combining-constraints-with-) +- [Combining constraints with `and`](#combining-constraints-with-and) +- [Combining constraints with `extend`](#combining-constraints-with-extend) +- [Combining constraints with `require` and `impls`](#combining-constraints-with-require-and-impls) +- [Rewrite constraint resolution](#rewrite-constraint-resolution) +- [Precise rules and termination](#precise-rules-and-termination) + - [Qualified name lookup](#qualified-name-lookup) + - [Type substitution](#type-substitution) + - [Examples](#examples) + - [Termination](#termination) + + + +## Rewrite constraints + +Rewrite constraints are [`where` clauses](details.md#where-constraints) of the +form `.AssociatedConstant = Value`. Given `T:! A where .B = C`, references to +`T.(A.B)` are rewritten to `C`. This appendix describes the precise rules +governing them. + +## Combining constraints with `&` + +Suppose we have `X = C where .R = A` and `Y = C where .R = B`. What should +`C & X` produce? What should `X & Y` produce? + +- Combining two rewrite rules with different rewrite targets results in a + facet type where the associated constant is ambiguous. Given `T:! X & Y`, + the type expression `T.R` is ambiguous between a rewrite to `A` and a + rewrite to `B`. But given `T:! X & X`, `T.R` is unambiguously rewritten to + `A`. +- Combining a constraint with a rewrite rule with a constraint with no rewrite + rule preserves the rewrite rule, so `C & X` is the same as `X`. For example, + supposing that `interface Container` extends `interface Iterable`, and + `Iterable` has an associated constant `Element`, the constraint + `Container & (Iterable where .Element = i32)` is the same as the constraint + `(Container & Iterable) where .Element = i32` which is the same as the + constraint `Container where .Element = i32`. + +If the rewrite for an associated constant is ambiguous, the facet type is +rejected during [constraint resolution](#rewrite-constraint-resolution). + +> **Alternative considered:** We could perhaps say that `X & Y` results in a +> facet type where the type of `R` has the union of the interface of `A` and the +> interface of `B`, and that `C & X` similarly results in a facet type where the +> type of `R` has the union of the interface of `A` and the interface originally +> specified by `C`. + +## Combining constraints with `and` + +It's possible for one `=` constraint in a `where` to refer to another. When this +happens, the facet type `C where A and B` is interpreted as +`(C where A) where B`, so rewrites in `A` are applied immediately to names in +`B`, but rewrites in `B` are not applied to names in `A` until the facet type is +[resolved](#rewrite-constraint-resolution): + +```carbon +interface C { + let T:! type; + let U:! type; + let V:! type; +} +class M { + alias Me = Self; +} +// ✅ Same as `C where .T = M and .U = M.Me`, which is +// the same as `C where .T = M and .U = M`. +fn F[A:! C where .T = M and .U = .T.Me]() {} +// ❌ No member `Me` in `A.T:! type`. +fn F[A:! C where .U = .T.Me and .T = M]() {} +``` + +## Combining constraints with `extend` + +Within an interface or named constraint, `extend` can be used to extend a +constraint that has rewrites. + +```carbon +interface A { + let T:! type; + let U:! type; +} +interface B { + extend A where .T = .U and .U = i32; +} + +var n: i32; + +// ✅ Resolved constraint on `T` is +// `B where .(A.T) = i32 and .(A.U) = i32`. +// `T.(A.T)` is rewritten to `i32`. +fn F(T:! B) -> T.(A.T) { return n; } +``` + +## Combining constraints with `require` and `impls` + +Within an interface or named constraint, the `require T impls C` and +`require Self impls C` syntaxes do not change the type of `T` or `Self`, +respectively, so any `=` constraints that they specify do not result in rewrites +being performed when the type `T` or `Self` is later used. Such `=` constraints +are equivalent to `==` constraints: + +```carbon +interface A { + let T:! type; + let U:! type; +} +constraint C { + extend A where .T = .U and .U = i32; +} +constraint D { + extend A where .T == .U and .U == i32; +} +interface B { + // OK, equivalent to `require Self impls D;` or + // `require Self impls A where .T == .U and .U == i32;`. + require Self impls C; +} + +var n: i32; + +// ❌ No implicit conversion from `i32` to `T.(A.T)`. +// Resolved constraint on `T` is +// `B where T.(A.T) == T.(A.U) and T.(A.U) == i32`. +// `T.(A.T)` is single-step equal to `T.(A.U)`, and +// `T.(A.U)` is single-step equal to `i32`, but +// `T.(A.T)` is not single-step equal to `i32`. +fn F(T:! B) -> T.(A.T) { return n; } +``` + +Because `=` constraints are effectively treated as `==` constraints in an +`require Self impls C` or `require T impls C` declaration in an interface or +named constraint, it is an error to specify such a `=` constraint directly in +`C`. A purely syntactic check is used to determine if an `=` is specified +directly in an expression: + +- An `=` constraint is specified directly in its enclosing `where` expression. +- If an `=` constraint is specified directly in an operand of an `&` or + `(`...`)`, then it is specified directly in that enclosing expression. + +For example: + +```carbon +// Compile-time identity function. +fn Identity[T:! type](x:! T) -> T { return x; } + +interface E { + // ❌ Rewrite constraint specified directly. + require Self impls A where .T = .U and .U = i32; + // ❌ Rewrite constraint specified directly. + require Self impls type & (A where .T = .U and .U = i32); + // ✅ Not specified directly, but does not result + // in any rewrites being performed. + require Self impls Identity(A where .T = .U and .U = i32); +} +``` + +The same rules apply to `where`...`impls` constraints. Note that `.T == U` +constraints are also not allowed in this context, because the reference to `.T` +is rewritten to `.Self.T`, and `.Self` is ambiguous. + +```carbon +// ❌ Rewrite constraint specified directly in `impls`. +fn F[T:! A where .U impls (A where .T = i32)](); + +// ❌ Reference to `.T` in same-type constraint is ambiguous: +// does this mean the outer or inner `.Self.T`? +fn G[T:! A where .U impls (A where .T == i32)](); + +// ✅ Not specified directly, but does not result +// in any rewrites being performed. Return type +// is not rewritten to `i32`. +fn H[T:! type where .Self impls C]() -> T.(A.U); + +// ✅ Return type is rewritten to `i32`. +fn I[T:! C]() -> T.(A.U); +``` + +## Rewrite constraint resolution + +When a facet type is used as the declared type of a facet `T`, the constraints +that were specified within that facet type are _resolved_ to determine the +constraints that apply to `T`. This happens: + +- When the constraint is used explicitly when declaring a symbolic binding, + like a generic parameter or associated constant, of the form + `T:! Constraint`. +- When declaring that a type implements a constraint with an `impl` + declaration, such as `impl T as Constraint`. Note that this does not include + `require` ... `impls` constraints appearing in `interface` or `constraint` + declarations. + +In each case, the following steps are performed to resolve the facet type's +abstract constraints into a set of constraints on `T`: + +- If multiple rewrites are specified for the same associated constant, they + are required to be identical, and duplicates are discarded. +- Rewrites are performed on other rewrites in order to find a fixed point, + where no rewrite applies within any other rewrite. If no fixed point exists, + the generic parameter declaration or `impl` declaration is invalid. +- Rewrites are performed throughout the other constraints in the facet type -- + that is, in any `==` constraints and `impls` constraints -- and the type + `.Self` is replaced by `T` throughout the constraint. + +```carbon +// ✅ `.T` in `.U = .T` is rewritten to `i32` when initially +// forming the facet type. +// Nothing to do during constraint resolution. +fn InOrder[A:! C where .T = i32 and .U = .T]() {} +// ✅ Facet type has `.T = .U` before constraint resolution. +// That rewrite is resolved to `.T = i32`. +fn Reordered[A:! C where .T = .U and .U = i32]() {} +// ✅ Facet type has `.U = .T` before constraint resolution. +// That rewrite is resolved to `.U = i32`. +fn ReorderedIndirect[A:! (C where .T = i32) & (C where .U = .T)]() {} +// ❌ Constraint resolution fails because +// no fixed point of rewrites exists. +fn Cycle[A:! C where .T = .U and .U = .T]() {} +``` + +To find a fixed point, we can perform rewrites on other rewrites, cycling +between them until they don't change or until a rewrite would apply to itself. +In the latter case, we have found a cycle and can reject the constraint. Note +that it's not sufficient to expand only a single rewrite until we hit this +condition: + +```carbon +// ❌ Constraint resolution fails because +// no fixed point of rewrites exists. +// If we only expand the right-hand side of `.T`, +// we find `.U`, then `.U*`, then `.U**`, and so on, +// and never detect a cycle. +// If we alternate between them, we find +// `.T = .U*`, then `.U = .U**`, then `.V = .U***`, +// then `.T = .U**`, then detect that the `.U` rewrite +// would apply to itself. +fn IndirectCycle[A:! C where .T = .U and .U = .V* and .V = .U*](); +``` + +After constraint resolution, no references to rewritten associated constants +remain in the constraints on `T`. + +If a facet type is never used to constrain a type, it is never subject to +constraint resolution, and it is possible for a facet type to be formed for +which constraint resolution would always fail. For example: + +```carbon +package Broken api; + +interface X { + let T:! type; + let U:! type; +} +let Bad:! auto = (X where .T = .U) & (X where .U = .T); +// Bad is not used here. +``` + +In such cases, the facet type `Broken.Bad` is not usable: any attempt to use +that facet type to constrain a type would perform constraint resolution, which +would always fail because it would discover a cycle between the rewrites for +`.T` and for `.U`. In order to ensure that such cases are diagnosed, a trial +constraint resolution is performed for all facet types. Note that this trial +resolution can be skipped for facet types that are actually used, which is the +common case. + +## Precise rules and termination + +This section explains the detailed rules used to implement rewrites. There are +two properties we aim to satisfy: + +1. After type-checking, no symbolic references to associated constants that + have an associated rewrite rule remain. +2. Type-checking always terminates in a reasonable amount of time, ideally + linear in the size of the problem. + +Rewrites are applied in two different phases of program analysis. + +- During qualified name lookup and type checking for qualified member access, + if a rewritten member is looked up, the right-hand side's value and type are + used for subsequent checks. +- During substitution, if the symbolic name of an associated constant is + substituted into, and substitution into the left-hand side results in a + value with a rewrite for that constant, that rewrite is applied. + +In each case, we always rewrite to a value that satisfies property 1 above, and +these two steps are the only places where we might form a symbolic reference to +an associated cosntant, so property 1 is recursively satisfied. Moreover, we +apply only one rewrite in each of the above cases, satisfying property 2. + +### Qualified name lookup + +Qualified name lookup into either a facet parameter or into an expression whose +type is a symbolic type `T` -- either a facet parameter or an associated facet +-- considers names from the facet type `C` of `T`, that is, from `T`’s declared +type. + +```carbon +interface C { + let M:! i32; + let U:! C; +} +fn F[T:! C](x: T) { + // Value is C.M in all four of these + let a: i32 = x.M; + let b: i32 = T.M; + let c: i32 = x.U.M; + let d: i32 = T.U.M; +} +``` + +When looking up the name `N`, if `C` is an interface `I` and `N` is the name of +an associated constant in that interface, the result is a symbolic value +representing "the member `N` of `I`". If `C` is formed by combining interfaces +with `&`, all such results are required to find the same associated constant, +otherwise we reject for ambiguity. + +If a member of a class or interface is named in a qualified name lookup, the +type of the result is determined by performing a substitution. For an interface, +`Self` is substituted for the self type, and any parameters for that class or +interface (and enclosing classes or interfaces, if any) are substituted into the +declared type. + +```carbon +interface SelfIface { + fn Get[self: Self]() -> Self; +} +class UsesSelf(T:! type) { + // Equivalent to `fn Make() -> UsesSelf(T)*;` + fn Make() -> Self*; + impl as SelfIface; +} + +// ✅ `T = i32` is substituted into the type of `UsesSelf(T).Make`, +// so the type of `UsesSelf(i32).Make` is `fn () -> UsesSelf(i32)*`. +let x: UsesSelf(i32)* = UsesSelf(i32).Make(); + +// ✅ `Self = UsesSelf(i32)` is substituted into the type +// of `SelfIface.Get`, so the type of `UsesSelf(i32).(SelfIface.Get)` +// is `fn [self: UsesSelf(i32)]() -> UsesSelf(i32)`. +let y: UsesSelf(i32) = x->Get(); +``` + +If a facet type `C` into which lookup is performed includes a `where` clause +saying `.N = U`, and the result of qualified name lookup is the associated +constant `N`, that result is replaced by `U`, and the type of the result is the +type of `U`. No substitution is performed in this step, not even a `Self` +substitution -- any necessary substitutions were already performed when forming +the facet type `C`, and we don’t consider either the declared type or value of +the associated constant at all for this kind of constraint. Going through an +example in detail: + +```carbon +interface A { + let T:! type; +} +interface B { + let U:! type; + // More explicitly, this is of type `A where .(A.T) = Self.(B.U)` + let V:! A where .T = U; +} +// Type of W is B. +fn F[W:! B](x: W) { + // The type of the expression `W` is `B`. + // `W.V` finds `B.V` with type `A where .(A.T) = Self.(B.U)`. + // We substitute `Self` = `W` giving the type of `u` as + // `A where .(A.T) = W.(B.U)`. + let u:! auto = W.V; + // The type of `u` is `A where .(A.T) = W.(B.U)`. + // Lookup for `u.T` resolves it to `u.(A.T)`. + // So the result of the qualified member access is `W.(B.U)`, + // and the type of `v` is the type of `W.(B.U)`, namely `type`. + // No substitution is performed in this step. + let v:! auto = u.T; +} +``` + +The more complex case of + +```carbon +fn F2[Z:! B where .U = i32](x: Z); +``` + +is discussed later. + +### Type substitution + +At various points during the type-checking of a Carbon program, we need to +substitute a set of (binding, value) pairs into a symbolic value. We saw an +example above: substituting `Self = W` into the type `A where .(A.T) = Self.U` +to produce the value `A where .(A.T) = W.U`. Another important case is the +substitution of inferred parameter values into the type of a function when +type-checking a function call: + +```carbon +fn F[T:! C](x: T) -> T; +fn G(n: i32) -> i32 { + // Deduces T = i32, which is substituted + // into the type `fn (x: T) -> T` to produce + // `fn (x: i32) -> i32`, giving `i32` as the type + // of the call expression. + return F(n); +} +``` + +Qualified name lookup is not re-done as a result of type substitution. For a +template, we imagine there’s a completely separate step that happens before type +substitution, where qualified name lookup is redone based on the actual value of +template arguments; this proceeds as described in the previous section. +Otherwise, we performed the qualified name lookup when type-checking symbolic +expressions, and do not do it again: + +```carbon +interface IfaceHasX { + let X:! type; +} +class ClassHasX { + class X {} +} +interface HasAssoc { + let Assoc:! IfaceHasX; +} + +// Qualified name lookup finds `T.(HasAssoc.Assoc).(IfaceHasX.X)`. +fn F(T:! HasAssoc) -> T.Assoc.X; + +fn G(T:! HasAssoc where .Assoc = ClassHasX) { + // `T.Assoc` rewritten to `ClassHasX` by qualified name lookup. + // Names `ClassHasX.X`. + var a: T.Assoc.X = {}; + // Substitution produces `ClassHasX.(IfaceHasX.X)`, + // not `ClassHasX.X`. + var b: auto = F(T); +} +``` + +During substitution, we might find a member access that named an opaque symbolic +associated constant in the original value can now be resolved to some specific +value. It’s important that we perform this resolution: + +```carbon +interface A { + let T:! type; +} +class K { fn Member(); } +fn H[U:! A](x: U) -> U.T; +fn J[V:! A where .T = K](y: V) { + // We need the interface of `H(y)` to include + // `K.Member` in order for this lookup to succeed. + H(y).Member(); +} +``` + +The values being substituted into the symbolic value are themselves already +fully substituted and resolved, and in particular, satisfy property 1 given +above. + +Substitution proceeds by recursively rebuilding each symbolic value, bottom-up, +replacing each substituted binding with its value. Doing this naively will +propagate values like `i32` in the `F`/`G` case earlier in this section, but +will not propagate rewrite constants like in the `H`/`J` case. The reason is +that the `.T = K` constraint is in the _type_ of the substituted value, rather +than in the substituted value itself: deducing `T = i32` and converting `i32` to +the type `C` of `T` preserves the value `i32`, but deducing `U = V` and +converting `V` to the type `A` of `U` discards the rewrite constraint. + +In order to apply rewrites during substitution, we associate a set of rewrites +with each value produced by the recursive rebuilding procedure. This is somewhat +like having substitution track a refined facet type for the type of each value, +but we don’t need -- or want -- for the type to change during this process, only +for the rewrites to be properly applied. For a substituted binding, this set of +rewrites is the rewrites found on the type of the corresponding value prior to +conversion to the type of the binding. When rebuilding a member access +expression, if we have a rewrite corresponding to the accessed member, then the +resulting value is the target of the rewrite, and its set of rewrites is that +found in the type of the target of the rewrite, if any. Because the target of +the rewrite is fully resolved already, we can ask for its type without +triggering additional work. In other cases, the rewrite set is empty; all +necessary rewrites were performed when type-checking the value we're +substituting into. + +Continuing an example from [qualified name lookup](#qualified-name-lookup): + +```carbon +interface A { + let T:! type; +} +interface B { + let U:! type; + let V:! A where .T = U; +} + +// Type of the expression `Z` is `B where .(B.U) = i32` +fn F2[Z:! B where .U = i32](x: Z) { + // The type of the expression `Z` is `B where .U = i32`. + // `Z.V` is looked up and finds the associated facet `(B.V)`. + // The declared type is `A where .(A.T) = Self.U`. + // We substitute `Self = Z` with rewrite `.U = i32`. + // The resulting type is `A where .(A.T) = i32`. + // So `u` is `Z.V` with type `A where .(A.T) = i32`. + let u:! auto = Z.V; + // The type of `u` is `A where .(A.T) = i32`. + // Lookup for `u.T` resolves it to `u.(A.T)`. + // So the result of the qualified member access is `i32`, + // and the type of `v` is the type of `i32`, namely `type`. + // No substitution is performed in this step. + let v:! auto = u.T; +} +``` + +### Examples + +```carbon +interface Container { + let Element:! type; +} +interface SliceableContainer { + extend Container; + let Slice:! Container where .Element = Self.(Container.Element); +} +// ❌ Qualified name lookup rewrites this facet type to +// `SliceableContainer where .(Container.Element) = .Self.(Container.Element)`. +// Constraint resolution rejects this because this rewrite forms a cycle. +fn Bad[T:! SliceableContainer where .Element = .Slice.Element](x: T.Element) {} +``` + +```carbon +interface Helper { + let D:! type; +} +interface Example { + let B:! type; + let C:! Helper where .D = B; +} +// ✅ `where .D = ...` by itself is fine. +// `T.C.D` is rewritten to `T.B`. +fn Allowed(T:! Example, x: T.C.D); +// ❌ But combined with another rewrite, creates an infinite loop. +// `.C.D` is rewritten to `.B`, resulting in `where .B = .B`, +// which causes an error during constraint resolution. +// Using `==` instead of `=` would make this constraint redundant, +// rather than it being an error. +fn Error(T:! Example where .B = .C.D, x: T.C.D); +``` + +```carbon +interface Allowed; +interface AllowedBase { + let A:! Allowed; +} +interface Allowed { + extend AllowedBase where .A = .Self; +} +// ✅ The final type of `x` is `T`. It is computed as follows: +// In `((T.A).A).A`, the inner `T.A` is rewritten to `T`, +// resulting in `((T).A).A`, which is then rewritten to +// `(T).A`, which is then rewritten to `T`. +fn F(T:! Allowed, x: ((T.A).A).A); +``` + +```carbon +interface MoveYsRight; +constraint ForwardDeclaredConstraint(X:! MoveYsRight); +interface MoveYsRight { + let X:! MoveYsRight; + // Means `Y:! MoveYsRight where .X = X.Y` + let Y:! ForwardDeclaredConstraint(X); +} +constraint ForwardDeclaredConstraint(X:! MoveYsRight) { + extend MoveYsRight where .X = X.Y; +} +// ✅ The final type of `x` is `T.X.Y.Y`. It is computed as follows: +// The type of `T` is `MoveYsRight`. +// The type of `T.Y` is determined as follows: +// - Qualified name lookup finds `MoveYsRight.Y`. +// - The declared type is `ForwardDeclaredConstraint(Self.X)`. +// - That is a named constraint, for which we perform substitution. +// Substituting `X = Self.X` gives the type +// `MoveYsRight where .X = Self.X.Y`. +// - Substituting `Self = T` gives the type +// `MoveYsRight where .X = T.X.Y`. +// The type of `T.Y.Y` is determined as follows: +// - Qualified name lookup finds `MoveYsRight.Y`. +// - The declared type is `ForwardDeclaredConstraint(Self.X)`. +// - That is a named constraint, for which we perform substitution. +// Substituting `X = Self.X` gives the type +// `MoveYsRight where .X = Self.X.Y`. +// - Substituting `Self = T.Y` with +// rewrite `.X = T.X.Y` gives the type +// `MoveYsRight where .X = T.Y.X.Y`, but +// `T.Y.X` is replaced by `T.X.Y`, giving +// `MoveYsRight where .X = T.X.Y.Y`. +// The type of `T.Y.Y.X` is determined as follows: +// - Qualified name lookup finds `MoveYsRight.X`. +// - The type of `T.Y.Y` says to rewrite that to `T.X.Y.Y`. +// - The result is `T.X.Y.Y`, of type `MoveYsRight`. +fn F4(T:! MoveYsRight, x: T.Y.Y.X); +``` + +### Termination + +Each of the above steps performs at most one rewrite, and doesn't introduce any +new recursive type-checking steps, so should not introduce any new forms of +non-termination. Rewrite constraints thereby give us a deterministic, +terminating type canonicalization mechanism for associated constants: in `A.B`, +if the type of `A` specifies that `.B = C`, then `A.B` is replaced by `C`. +Equality of types constrained in this way is transitive. + +However, some existing forms of non-termination may remain, such as template +instantiation triggering another template instantiation. Such cases will need to +be detected and handled in some way, such as by a depth limit, but doing so +doesn't compromise the soundness of the type system. diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index e3f17420985a6..56b36f14affe3 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -52,16 +52,6 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception - [Kinds of `where` constraints](#kinds-of-where-constraints) - [Recursive constraints](#recursive-constraints) - [Rewrite constraints](#rewrite-constraints) - - [Combining constraints with `&`](#combining-constraints-with-) - - [Combining constraints with `and`](#combining-constraints-with-and) - - [Combining constraints with `extend`](#combining-constraints-with-extend) - - [Combining constraints with `require` and `impls`](#combining-constraints-with-require-and-impls) - - [Rewrite constraint resolution](#rewrite-constraint-resolution) - - [Precise rules and termination](#precise-rules-and-termination) - - [Qualified name lookup](#qualified-name-lookup) - - [Type substitution](#type-substitution) - - [Examples](#examples) - - [Termination](#termination) - [Same-type constraints](#same-type-constraints) - [Implementation of same-type `ImplicitAs`](#implementation-of-same-type-implicitas) - [Manual type equality](#manual-type-equality) @@ -2733,8 +2723,8 @@ fn Add[T:! Container where .Element = i32](p: T*, y: T.Slice.Element) { Rewrites aren't performed on the left-hand side of such an `=`, so `where .A = .B and .A = C` is not rewritten to `where .A = .B and .B = C`. Instead, such a `where` clause is invalid when the constraint is -[resolved](#rewrite-constraint-resolution) unless each rule for `.A` specifies -the same rewrite. +[resolved](appendix-rewrite-constraints.md#rewrite-constraint-resolution) unless +each rule for `.A` specifies the same rewrite. Note that `T:! C where .R = i32` can result in a type `T.R` whose behavior is different from the behavior of `T.R` given `T:! C`. For example, member lookup @@ -2756,598 +2746,8 @@ This approach has some good properties that enable efficient type equality. - [Transitivity of equality of types](/proposals/p2173.md#transitivity-of-equality) -##### Combining constraints with `&` - -Suppose we have `X = C where .R = A` and `Y = C where .R = B`. What should -`C & X` produce? What should `X & Y` produce? - -- Combining two rewrite rules with different rewrite targets results in a - facet type where the associated constant is ambiguous. Given `T:! X & Y`, - the type expression `T.R` is ambiguous between a rewrite to `A` and a - rewrite to `B`. But given `T:! X & X`, `T.R` is unambiguously rewritten to - `A`. -- Combining a constraint with a rewrite rule with a constraint with no rewrite - rule preserves the rewrite rule, so `C & X` is the same as `X`. For example, - supposing that `interface Container` extends `interface Iterable`, and - `Iterable` has an associated constant `Element`, the constraint - `Container & (Iterable where .Element = i32)` is the same as the constraint - `(Container & Iterable) where .Element = i32` which is the same as the - constraint `Container where .Element = i32`. - -If the rewrite for an associated constant is ambiguous, the facet type is -rejected during [constraint resolution](#rewrite-constraint-resolution). - -> **Alternative considered:** We could perhaps say that `X & Y` results in a -> facet type where the type of `R` has the union of the interface of `A` and the -> interface of `B`, and that `C & X` similarly results in a facet type where the -> type of `R` has the union of the interface of `A` and the interface originally -> specified by `C`. - -##### Combining constraints with `and` - -It's possible for one `=` constraint in a `where` to refer to another. When this -happens, the facet type `C where A and B` is interpreted as -`(C where A) where B`, so rewrites in `A` are applied immediately to names in -`B`, but rewrites in `B` are not applied to names in `A` until the facet type is -[resolved](#rewrite-constraint-resolution): - -```carbon -interface C { - let T:! type; - let U:! type; - let V:! type; -} -class M { - alias Me = Self; -} -// ✅ Same as `C where .T = M and .U = M.Me`, which is -// the same as `C where .T = M and .U = M`. -fn F[A:! C where .T = M and .U = .T.Me]() {} -// ❌ No member `Me` in `A.T:! type`. -fn F[A:! C where .U = .T.Me and .T = M]() {} -``` - -##### Combining constraints with `extend` - -Within an interface or named constraint, `extend` can be used to extend a -constraint that has rewrites. - -```carbon -interface A { - let T:! type; - let U:! type; -} -interface B { - extend A where .T = .U and .U = i32; -} - -var n: i32; - -// ✅ Resolved constraint on `T` is -// `B where .(A.T) = i32 and .(A.U) = i32`. -// `T.(A.T)` is rewritten to `i32`. -fn F(T:! B) -> T.(A.T) { return n; } -``` - -##### Combining constraints with `require` and `impls` - -Within an interface or named constraint, the `require T impls C` and -`require Self impls C` syntaxes do not change the type of `T` or `Self`, -respectively, so any `=` constraints that they specify do not result in rewrites -being performed when the type `T` or `Self` is later used. Such `=` constraints -are equivalent to `==` constraints: - -```carbon -interface A { - let T:! type; - let U:! type; -} -constraint C { - extend A where .T = .U and .U = i32; -} -constraint D { - extend A where .T == .U and .U == i32; -} -interface B { - // OK, equivalent to `require Self impls D;` or - // `require Self impls A where .T == .U and .U == i32;`. - require Self impls C; -} - -var n: i32; - -// ❌ No implicit conversion from `i32` to `T.(A.T)`. -// Resolved constraint on `T` is -// `B where T.(A.T) == T.(A.U) and T.(A.U) == i32`. -// `T.(A.T)` is single-step equal to `T.(A.U)`, and -// `T.(A.U)` is single-step equal to `i32`, but -// `T.(A.T)` is not single-step equal to `i32`. -fn F(T:! B) -> T.(A.T) { return n; } -``` - -Because `=` constraints are effectively treated as `==` constraints in an -`require Self impls C` or `require T impls C` declaration in an interface or -named constraint, it is an error to specify such a `=` constraint directly in -`C`. A purely syntactic check is used to determine if an `=` is specified -directly in an expression: - -- An `=` constraint is specified directly in its enclosing `where` expression. -- If an `=` constraint is specified directly in an operand of an `&` or - `(`...`)`, then it is specified directly in that enclosing expression. - -For example: - -```carbon -// Compile-time identity function. -fn Identity[T:! type](x:! T) -> T { return x; } - -interface E { - // ❌ Rewrite constraint specified directly. - require Self impls A where .T = .U and .U = i32; - // ❌ Rewrite constraint specified directly. - require Self impls type & (A where .T = .U and .U = i32); - // ✅ Not specified directly, but does not result - // in any rewrites being performed. - require Self impls Identity(A where .T = .U and .U = i32); -} -``` - -The same rules apply to `where`...`impls` constraints. Note that `.T == U` -constraints are also not allowed in this context, because the reference to `.T` -is rewritten to `.Self.T`, and `.Self` is ambiguous. - -```carbon -// ❌ Rewrite constraint specified directly in `impls`. -fn F[T:! A where .U impls (A where .T = i32)](); - -// ❌ Reference to `.T` in same-type constraint is ambiguous: -// does this mean the outer or inner `.Self.T`? -fn G[T:! A where .U impls (A where .T == i32)](); - -// ✅ Not specified directly, but does not result -// in any rewrites being performed. Return type -// is not rewritten to `i32`. -fn H[T:! type where .Self impls C]() -> T.(A.U); - -// ✅ Return type is rewritten to `i32`. -fn I[T:! C]() -> T.(A.U); -``` - -##### Rewrite constraint resolution - -**FIXME: Should the precise rules for constraints be moved into an appendix?** - -When a facet type is used as the declared type of a facet `T`, the constraints -that were specified within that facet type are _resolved_ to determine the -constraints that apply to `T`. This happens: - -- When the constraint is used explicitly when declaring a symbolic binding, - like a generic parameter or associated constant, of the form - `T:! Constraint`. -- When declaring that a type implements a constraint with an `impl` - declaration, such as `impl T as Constraint`. Note that this does not include - `require` ... `impls` constraints appearing in `interface` or `constraint` - declarations. - -In each case, the following steps are performed to resolve the facet type's -abstract constraints into a set of constraints on `T`: - -- If multiple rewrites are specified for the same associated constant, they - are required to be identical, and duplicates are discarded. -- Rewrites are performed on other rewrites in order to find a fixed point, - where no rewrite applies within any other rewrite. If no fixed point exists, - the generic parameter declaration or `impl` declaration is invalid. -- Rewrites are performed throughout the other constraints in the facet type -- - that is, in any `==` constraints and `impls` constraints -- and the type - `.Self` is replaced by `T` throughout the constraint. - -```carbon -// ✅ `.T` in `.U = .T` is rewritten to `i32` when initially -// forming the facet type. -// Nothing to do during constraint resolution. -fn InOrder[A:! C where .T = i32 and .U = .T]() {} -// ✅ Facet type has `.T = .U` before constraint resolution. -// That rewrite is resolved to `.T = i32`. -fn Reordered[A:! C where .T = .U and .U = i32]() {} -// ✅ Facet type has `.U = .T` before constraint resolution. -// That rewrite is resolved to `.U = i32`. -fn ReorderedIndirect[A:! (C where .T = i32) & (C where .U = .T)]() {} -// ❌ Constraint resolution fails because -// no fixed point of rewrites exists. -fn Cycle[A:! C where .T = .U and .U = .T]() {} -``` - -To find a fixed point, we can perform rewrites on other rewrites, cycling -between them until they don't change or until a rewrite would apply to itself. -In the latter case, we have found a cycle and can reject the constraint. Note -that it's not sufficient to expand only a single rewrite until we hit this -condition: - -```carbon -// ❌ Constraint resolution fails because -// no fixed point of rewrites exists. -// If we only expand the right-hand side of `.T`, -// we find `.U`, then `.U*`, then `.U**`, and so on, -// and never detect a cycle. -// If we alternate between them, we find -// `.T = .U*`, then `.U = .U**`, then `.V = .U***`, -// then `.T = .U**`, then detect that the `.U` rewrite -// would apply to itself. -fn IndirectCycle[A:! C where .T = .U and .U = .V* and .V = .U*](); -``` - -After constraint resolution, no references to rewritten associated constants -remain in the constraints on `T`. - -If a facet type is never used to constrain a type, it is never subject to -constraint resolution, and it is possible for a facet type to be formed for -which constraint resolution would always fail. For example: - -```carbon -package Broken api; - -interface X { - let T:! type; - let U:! type; -} -let Bad:! auto = (X where .T = .U) & (X where .U = .T); -// Bad is not used here. -``` - -In such cases, the facet type `Broken.Bad` is not usable: any attempt to use -that facet type to constrain a type would perform constraint resolution, which -would always fail because it would discover a cycle between the rewrites for -`.T` and for `.U`. In order to ensure that such cases are diagnosed, a trial -constraint resolution is performed for all facet types. Note that this trial -resolution can be skipped for facet types that are actually used, which is the -common case. - -##### Precise rules and termination - -This section explains the detailed rules used to implement rewrites. There are -two properties we aim to satisfy: - -1. After type-checking, no symbolic references to associated constants that - have an associated rewrite rule remain. -2. Type-checking always terminates in a reasonable amount of time, ideally - linear in the size of the problem. - -Rewrites are applied in two different phases of program analysis. - -- During qualified name lookup and type checking for qualified member access, - if a rewritten member is looked up, the right-hand side's value and type are - used for subsequent checks. -- During substitution, if the symbolic name of an associated constant is - substituted into, and substitution into the left-hand side results in a - value with a rewrite for that constant, that rewrite is applied. - -In each case, we always rewrite to a value that satisfies property 1 above, and -these two steps are the only places where we might form a symbolic reference to -an associated cosntant, so property 1 is recursively satisfied. Moreover, we -apply only one rewrite in each of the above cases, satisfying property 2. - -###### Qualified name lookup - -Qualified name lookup into either a facet parameter or into an expression whose -type is a symbolic type `T` -- either a facet parameter or an associated facet --- considers names from the facet type `C` of `T`, that is, from `T`’s declared -type. - -```carbon -interface C { - let M:! i32; - let U:! C; -} -fn F[T:! C](x: T) { - // Value is C.M in all four of these - let a: i32 = x.M; - let b: i32 = T.M; - let c: i32 = x.U.M; - let d: i32 = T.U.M; -} -``` - -When looking up the name `N`, if `C` is an interface `I` and `N` is the name of -an associated constant in that interface, the result is a symbolic value -representing "the member `N` of `I`". If `C` is formed by combining interfaces -with `&`, all such results are required to find the same associated constant, -otherwise we reject for ambiguity. - -If a member of a class or interface is named in a qualified name lookup, the -type of the result is determined by performing a substitution. For an interface, -`Self` is substituted for the self type, and any parameters for that class or -interface (and enclosing classes or interfaces, if any) are substituted into the -declared type. - -```carbon -interface SelfIface { - fn Get[self: Self]() -> Self; -} -class UsesSelf(T:! type) { - // Equivalent to `fn Make() -> UsesSelf(T)*;` - fn Make() -> Self*; - impl as SelfIface; -} - -// ✅ `T = i32` is substituted into the type of `UsesSelf(T).Make`, -// so the type of `UsesSelf(i32).Make` is `fn () -> UsesSelf(i32)*`. -let x: UsesSelf(i32)* = UsesSelf(i32).Make(); - -// ✅ `Self = UsesSelf(i32)` is substituted into the type -// of `SelfIface.Get`, so the type of `UsesSelf(i32).(SelfIface.Get)` -// is `fn [self: UsesSelf(i32)]() -> UsesSelf(i32)`. -let y: UsesSelf(i32) = x->Get(); -``` - -If a facet type `C` into which lookup is performed includes a `where` clause -saying `.N = U`, and the result of qualified name lookup is the associated -constant `N`, that result is replaced by `U`, and the type of the result is the -type of `U`. No substitution is performed in this step, not even a `Self` -substitution -- any necessary substitutions were already performed when forming -the facet type `C`, and we don’t consider either the declared type or value of -the associated constant at all for this kind of constraint. Going through an -example in detail: - -```carbon -interface A { - let T:! type; -} -interface B { - let U:! type; - // More explicitly, this is of type `A where .(A.T) = Self.(B.U)` - let V:! A where .T = U; -} -// Type of W is B. -fn F[W:! B](x: W) { - // The type of the expression `W` is `B`. - // `W.V` finds `B.V` with type `A where .(A.T) = Self.(B.U)`. - // We substitute `Self` = `W` giving the type of `u` as - // `A where .(A.T) = W.(B.U)`. - let u:! auto = W.V; - // The type of `u` is `A where .(A.T) = W.(B.U)`. - // Lookup for `u.T` resolves it to `u.(A.T)`. - // So the result of the qualified member access is `W.(B.U)`, - // and the type of `v` is the type of `W.(B.U)`, namely `type`. - // No substitution is performed in this step. - let v:! auto = u.T; -} -``` - -The more complex case of - -```carbon -fn F2[Z:! B where .U = i32](x: Z); -``` - -is discussed later. - -###### Type substitution - -At various points during the type-checking of a Carbon program, we need to -substitute a set of (binding, value) pairs into a symbolic value. We saw an -example above: substituting `Self = W` into the type `A where .(A.T) = Self.U` -to produce the value `A where .(A.T) = W.U`. Another important case is the -substitution of inferred parameter values into the type of a function when -type-checking a function call: - -```carbon -fn F[T:! C](x: T) -> T; -fn G(n: i32) -> i32 { - // Deduces T = i32, which is substituted - // into the type `fn (x: T) -> T` to produce - // `fn (x: i32) -> i32`, giving `i32` as the type - // of the call expression. - return F(n); -} -``` - -Qualified name lookup is not re-done as a result of type substitution. For a -template, we imagine there’s a completely separate step that happens before type -substitution, where qualified name lookup is redone based on the actual value of -template arguments; this proceeds as described in the previous section. -Otherwise, we performed the qualified name lookup when type-checking symbolic -expressions, and do not do it again: - -```carbon -interface IfaceHasX { - let X:! type; -} -class ClassHasX { - class X {} -} -interface HasAssoc { - let Assoc:! IfaceHasX; -} - -// Qualified name lookup finds `T.(HasAssoc.Assoc).(IfaceHasX.X)`. -fn F(T:! HasAssoc) -> T.Assoc.X; - -fn G(T:! HasAssoc where .Assoc = ClassHasX) { - // `T.Assoc` rewritten to `ClassHasX` by qualified name lookup. - // Names `ClassHasX.X`. - var a: T.Assoc.X = {}; - // Substitution produces `ClassHasX.(IfaceHasX.X)`, - // not `ClassHasX.X`. - var b: auto = F(T); -} -``` - -During substitution, we might find a member access that named an opaque symbolic -associated constant in the original value can now be resolved to some specific -value. It’s important that we perform this resolution: - -```carbon -interface A { - let T:! type; -} -class K { fn Member(); } -fn H[U:! A](x: U) -> U.T; -fn J[V:! A where .T = K](y: V) { - // We need the interface of `H(y)` to include - // `K.Member` in order for this lookup to succeed. - H(y).Member(); -} -``` - -The values being substituted into the symbolic value are themselves already -fully substituted and resolved, and in particular, satisfy property 1 given -above. - -Substitution proceeds by recursively rebuilding each symbolic value, bottom-up, -replacing each substituted binding with its value. Doing this naively will -propagate values like `i32` in the `F`/`G` case earlier in this section, but -will not propagate rewrite constants like in the `H`/`J` case. The reason is -that the `.T = K` constraint is in the _type_ of the substituted value, rather -than in the substituted value itself: deducing `T = i32` and converting `i32` to -the type `C` of `T` preserves the value `i32`, but deducing `U = V` and -converting `V` to the type `A` of `U` discards the rewrite constraint. - -In order to apply rewrites during substitution, we associate a set of rewrites -with each value produced by the recursive rebuilding procedure. This is somewhat -like having substitution track a refined facet type for the type of each value, -but we don’t need -- or want -- for the type to change during this process, only -for the rewrites to be properly applied. For a substituted binding, this set of -rewrites is the rewrites found on the type of the corresponding value prior to -conversion to the type of the binding. When rebuilding a member access -expression, if we have a rewrite corresponding to the accessed member, then the -resulting value is the target of the rewrite, and its set of rewrites is that -found in the type of the target of the rewrite, if any. Because the target of -the rewrite is fully resolved already, we can ask for its type without -triggering additional work. In other cases, the rewrite set is empty; all -necessary rewrites were performed when type-checking the value we're -substituting into. - -Continuing an example from [qualified name lookup](#qualified-name-lookup): - -```carbon -interface A { - let T:! type; -} -interface B { - let U:! type; - let V:! A where .T = U; -} - -// Type of the expression `Z` is `B where .(B.U) = i32` -fn F2[Z:! B where .U = i32](x: Z) { - // The type of the expression `Z` is `B where .U = i32`. - // `Z.V` is looked up and finds the associated facet `(B.V)`. - // The declared type is `A where .(A.T) = Self.U`. - // We substitute `Self = Z` with rewrite `.U = i32`. - // The resulting type is `A where .(A.T) = i32`. - // So `u` is `Z.V` with type `A where .(A.T) = i32`. - let u:! auto = Z.V; - // The type of `u` is `A where .(A.T) = i32`. - // Lookup for `u.T` resolves it to `u.(A.T)`. - // So the result of the qualified member access is `i32`, - // and the type of `v` is the type of `i32`, namely `type`. - // No substitution is performed in this step. - let v:! auto = u.T; -} -``` - -###### Examples - -```carbon -interface Container { - let Element:! type; -} -interface SliceableContainer { - extend Container; - let Slice:! Container where .Element = Self.(Container.Element); -} -// ❌ Qualified name lookup rewrites this facet type to -// `SliceableContainer where .(Container.Element) = .Self.(Container.Element)`. -// Constraint resolution rejects this because this rewrite forms a cycle. -fn Bad[T:! SliceableContainer where .Element = .Slice.Element](x: T.Element) {} -``` - -```carbon -interface Helper { - let D:! type; -} -interface Example { - let B:! type; - let C:! Helper where .D = B; -} -// ✅ `where .D = ...` by itself is fine. -// `T.C.D` is rewritten to `T.B`. -fn Allowed(T:! Example, x: T.C.D); -// ❌ But combined with another rewrite, creates an infinite loop. -// `.C.D` is rewritten to `.B`, resulting in `where .B = .B`, -// which causes an error during constraint resolution. -// Using `==` instead of `=` would make this constraint redundant, -// rather than it being an error. -fn Error(T:! Example where .B = .C.D, x: T.C.D); -``` - -```carbon -interface Allowed; -interface AllowedBase { - let A:! Allowed; -} -interface Allowed { - extend AllowedBase where .A = .Self; -} -// ✅ The final type of `x` is `T`. It is computed as follows: -// In `((T.A).A).A`, the inner `T.A` is rewritten to `T`, -// resulting in `((T).A).A`, which is then rewritten to -// `(T).A`, which is then rewritten to `T`. -fn F(T:! Allowed, x: ((T.A).A).A); -``` - -```carbon -interface MoveYsRight; -constraint ForwardDeclaredConstraint(X:! MoveYsRight); -interface MoveYsRight { - let X:! MoveYsRight; - // Means `Y:! MoveYsRight where .X = X.Y` - let Y:! ForwardDeclaredConstraint(X); -} -constraint ForwardDeclaredConstraint(X:! MoveYsRight) { - extend MoveYsRight where .X = X.Y; -} -// ✅ The final type of `x` is `T.X.Y.Y`. It is computed as follows: -// The type of `T` is `MoveYsRight`. -// The type of `T.Y` is determined as follows: -// - Qualified name lookup finds `MoveYsRight.Y`. -// - The declared type is `ForwardDeclaredConstraint(Self.X)`. -// - That is a named constraint, for which we perform substitution. -// Substituting `X = Self.X` gives the type -// `MoveYsRight where .X = Self.X.Y`. -// - Substituting `Self = T` gives the type -// `MoveYsRight where .X = T.X.Y`. -// The type of `T.Y.Y` is determined as follows: -// - Qualified name lookup finds `MoveYsRight.Y`. -// - The declared type is `ForwardDeclaredConstraint(Self.X)`. -// - That is a named constraint, for which we perform substitution. -// Substituting `X = Self.X` gives the type -// `MoveYsRight where .X = Self.X.Y`. -// - Substituting `Self = T.Y` with -// rewrite `.X = T.X.Y` gives the type -// `MoveYsRight where .X = T.Y.X.Y`, but -// `T.Y.X` is replaced by `T.X.Y`, giving -// `MoveYsRight where .X = T.X.Y.Y`. -// The type of `T.Y.Y.X` is determined as follows: -// - Qualified name lookup finds `MoveYsRight.X`. -// - The type of `T.Y.Y` says to rewrite that to `T.X.Y.Y`. -// - The result is `T.X.Y.Y`, of type `MoveYsRight`. -fn F4(T:! MoveYsRight, x: T.Y.Y.X); -``` - -###### Termination - -Each of the above steps performs at most one rewrite, and doesn't introduce any -new recursive type-checking steps, so should not introduce any new forms of -non-termination. Rewrite constraints thereby give us a deterministic, -terminating type canonicalization mechanism for associated constants: in `A.B`, -if the type of `A` specifies that `.B = C`, then `A.B` is replaced by `C`. -Equality of types constrained in this way is transitive. - -However, some existing forms of non-termination may remain, such as template -instantiation triggering another template instantiation. Such cases will need to -be detected and handled in some way, such as by a depth limit, but doing so -doesn't compromise the soundness of the type system. +The precise rules governing rewrite constraints are described in +[an appendix](appendix-rewrite-constraints.md). #### Same-type constraints From 74fa36c51bfcf5c3cb72a2339523b1f32821b8a8 Mon Sep 17 00:00:00 2001 From: josh11b Date: Fri, 29 Sep 2023 13:54:16 -0700 Subject: [PATCH 16/19] Apply suggestions from code review Co-authored-by: Richard Smith --- docs/design/generics/details.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 56b36f14affe3..bee69d4cb76cf 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -2898,9 +2898,9 @@ interface Edge { } interface Node { let E:! EdgeFor(Self); - fn GetE[self: Self]() -> EdgeT; - fn AddE[addr self: Self*](e: EdgeT); - fn NearN[self: Self](n: N) -> bool; + fn GetE[self: Self]() -> E; + fn AddE[addr self: Self*](e: E); + fn NearN[self: Self](n: Self) -> bool; } constraint EdgeFor(NodeT:! Node) { @@ -3022,7 +3022,7 @@ fn J[G: Graph](g: G) { ``` the expression `G.E.N.E.N` is one equality away from `G.N.E.N` and so it is -allowed. This is even though `G.N.E.N` isn't the type expression immediately +allowed. This is true even though `G.N.E.N` isn't the type expression immediately prior to `G.E.N.E.N`. After an `observe` declaration, all of the listed type expressions are From dca0f20f9d2ed7784fbbaba4271a43c2c8019665 Mon Sep 17 00:00:00 2001 From: Josh L Date: Fri, 29 Sep 2023 20:54:49 +0000 Subject: [PATCH 17/19] Fix formatting --- docs/design/generics/details.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index bee69d4cb76cf..b10c1523dcab3 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -3022,8 +3022,8 @@ fn J[G: Graph](g: G) { ``` the expression `G.E.N.E.N` is one equality away from `G.N.E.N` and so it is -allowed. This is true even though `G.N.E.N` isn't the type expression immediately -prior to `G.E.N.E.N`. +allowed. This is true even though `G.N.E.N` isn't the type expression +immediately prior to `G.E.N.E.N`. After an `observe` declaration, all of the listed type expressions are considered equal to each other using a single `where` equality. In this example, From 371045b6290eebb4d6574d7cd2988853dcb13a6b Mon Sep 17 00:00:00 2001 From: Josh L Date: Sat, 30 Sep 2023 00:01:02 +0000 Subject: [PATCH 18/19] Future work --- docs/design/generics/details.md | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index b10c1523dcab3..a1f6ed0f63421 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -2592,19 +2592,25 @@ this interface while `.Self` refers to the associated facet currently being defined. ```carbon +interface Container; +constraint SliceConstraint(E:! type, S:! Container); + interface Container { let ElementType:! type; let IteratorType:! Iterator where .ElementType = ElementType; - let SliceType:! Container - where .ElementType = ElementType and - // `.Self` means `SliceType`. - .SliceType = .Self; + // `.Self` means `SliceType`. + let SliceType:! SliceConstraint(ElementType, .Self); // `Self` means the type implementing `Container`. fn GetSlice[addr self: Self*] (start: IteratorType, end: IteratorType) -> SliceType; } + +constraint SliceConstraint(E:! type, S:! Container) { + extend Container where .ElementType = E and + .SliceType = S; +} ``` Note that [naming](#named-constraint-constants) a recursive constraint using the @@ -3148,6 +3154,11 @@ the above example, `Container` defines `ElementType` as having type `type`, but need to be a bit careful when talking about the type of `ContainerType` when there is a `where` clause modifying it. +> **Future work:** We may want to use a different operator in this case, such as +> `&=`, in place of `impls`, to reflect the change in the type. This is +> analogous to rewrite constraints using `=` instead of `==` to visibly reflect +> the different impact on the type. + An implements constraint can be applied to [`.Self`](#recursive-constraints), as in `I where .Self impls C`. This has the same requirements as `I & C`, but that `where` clause does not affect the API. This means that a From 2abc3b387bfcee5f9f870d8c900834802ad29f85 Mon Sep 17 00:00:00 2001 From: josh11b Date: Mon, 2 Oct 2023 16:50:48 -0700 Subject: [PATCH 19/19] Update docs/design/generics/details.md Co-authored-by: Richard Smith --- docs/design/generics/details.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index a1f6ed0f63421..dc16eb9648f60 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -2600,7 +2600,7 @@ interface Container { let IteratorType:! Iterator where .ElementType = ElementType; // `.Self` means `SliceType`. - let SliceType:! SliceConstraint(ElementType, .Self); + let SliceType:! Container where .Self is SliceConstraint(ElementType, .Self); // `Self` means the type implementing `Container`. fn GetSlice[addr self: Self*]