mirror of
https://github.com/carbon-language/carbon-lang.git
synced 2026-09-24 19:50:14 +01:00
Document the phase of associated constants, which the discussions of
contextual phase defaults never covered: an associated constant is
always a checked generic binding. This is deliberately not presented as
a contextual default, because no other phase is possible for the
construct; correspondingly, no phase keyword (including `template`) is
allowed on one. Also rework the associated constants section of the
design README where the migration left a non-sequitur ("set to
compile-time values ... and so are defined using a `let` declaration"):
describe the `let` syntax and the binding's contextual phase separately.
Use consistent terminology for bindings versus constants. Bindings are
"checked" or "template" (generic) bindings, replacing the "symbolic
binding" and bare "generic binding" terms, so "symbolic" now only
describes constants and values. The "Symbolic facet bindings" section of
the generics details becomes "Checked facet bindings". The
expression-phase terms "symbolic constant" and "template constant" are
unchanged, and the binding-pattern definitions now name the constant
each kind binds. Template bindings are additionally described as
dependent and late checked, with each instantiation providing the
binding's value.
Also normalize the remaining "regular parameter" mentions to "runtime
parameter" to match the binding terminology, and describe the
compile-time "let template" as introducing a template generic binding
"T: C" whose uses are template constants.
Assisted-by: Claude Code
This commit is contained in:
Chandler Carruth
+18
-12
@@ -739,7 +739,7 @@ Value expressions are further broken down into three _expression phases_:
|
||||
[monomorphization](https://en.wikipedia.org/wiki/Monomorphization) happens,
|
||||
but is not known during type checking. This includes
|
||||
[checked-generic parameters](#checked-and-template-parameters), and type
|
||||
expressions with checked-generic arguments, like `Optional(T*)`.
|
||||
expressions with symbolic constant arguments, like `Optional(T*)`.
|
||||
- A _runtime value_ has a dynamic value only known at runtime.
|
||||
|
||||
Template constants and symbolic constants are collectively called _compile-time
|
||||
@@ -1059,19 +1059,23 @@ Every binding pattern has a _phase_ (either compile-time or runtime). A
|
||||
[compile-time constants](#expression-phases), not run-time values.
|
||||
|
||||
To minimize keyword noise, Carbon uses contextual defaults to determine the
|
||||
phase (compile-time vs runtime) of a binding in parameter lists:
|
||||
phase (compile-time vs runtime) of a binding:
|
||||
|
||||
- Parameters to compile-time entities (such as `interface`, `impl`, and
|
||||
`class`) are checked generics by default.
|
||||
- Deduced function parameters (declared in `[]`) are checked generics by
|
||||
default.
|
||||
- Explicit function parameters and local bindings (declared in `()`) are
|
||||
- Explicit function parameters (declared in `()`) and local bindings are
|
||||
runtime by default.
|
||||
|
||||
These defaults can be overridden by using the `template`, `generic`, or
|
||||
`runtime` keywords. However, using a keyword that matches the contextual default
|
||||
is disallowed to maintain consistency. A `template` keyword before the binding
|
||||
selects a template binding instead of a symbolic binding.
|
||||
selects a template binding instead of a checked binding.
|
||||
|
||||
[Associated constants](#associated-constants) are always checked generic
|
||||
bindings. This is not a contextual default: no other phase is possible for an
|
||||
associated constant, and so no phase keyword is allowed there.
|
||||
|
||||
Binding patterns default to _`let` bindings_. The `var` keyword is used to make
|
||||
it a _`var` binding_.
|
||||
@@ -2806,7 +2810,7 @@ The [expression phase](#expression-phases) of a checked parameter is a symbolic
|
||||
constant whereas the expression phase of a template parameter is template
|
||||
constant. A binding pattern for a compile-time parameter is a _compile-time
|
||||
binding pattern_; more specifically a _template binding pattern_ if it uses
|
||||
`template`, and a _symbolic binding pattern_ if it uses `generic` or defaults to
|
||||
`template`, and a _checked binding pattern_ if it uses `generic` or defaults to
|
||||
it.
|
||||
|
||||
Although checked generics are generally preferred, templates enable translation
|
||||
@@ -3028,13 +3032,15 @@ to a checked parameter.
|
||||
|
||||
An associated constant is a member of an interface whose value is determined by
|
||||
the implementation of that interface for a specific type. These values are set
|
||||
to compile-time values in implementations, and so are defined using a
|
||||
[`let` declaration](#constant-let-declarations) without an initializer, which
|
||||
defines an associated constant in this context. This allows types in the
|
||||
signatures of functions in the interface to vary. For example, an interface
|
||||
describing a [stack](<https://en.wikipedia.org/wiki/Stack_(abstract_data_type)>)
|
||||
might use an associated constant to represent the type of elements stored in the
|
||||
stack.
|
||||
to compile-time values in implementations, which allows types in the signatures
|
||||
of functions in the interface to vary. An associated constant is defined using a
|
||||
[`let` declaration](#constant-let-declarations) without an initializer. Since an
|
||||
interface is a compile-time entity, the binding is a
|
||||
[checked generic binding](#checked-and-template-parameters) by context; no phase
|
||||
keyword is allowed, so an associated constant cannot be made `template`. For
|
||||
example, an interface describing a
|
||||
[stack](<https://en.wikipedia.org/wiki/Stack_(abstract_data_type)>) might use an
|
||||
associated constant to represent the type of elements stored in the stack.
|
||||
|
||||
```
|
||||
interface StackInterface {
|
||||
|
||||
@@ -175,7 +175,7 @@ _Note:_ This rule is intended to be considered more specialized than the other
|
||||
rules in this document.
|
||||
|
||||
Because this `impl` is declared `final`, `T.(CommonType(T)).Result` is always
|
||||
assumed to be `T`, even in contexts where `T` involves a symbolic binding and so
|
||||
assumed to be `T`, even in contexts where `T` involves a checked binding and so
|
||||
the result would normally be an unknown type whose facet type is `type`.
|
||||
|
||||
```
|
||||
|
||||
@@ -468,7 +468,7 @@ fn CallsDrawChecked(c: Cowboy) {
|
||||
|
||||
If the value or type depends on any template bindings, the lookup is redone from
|
||||
a context where the values of those bindings are known, but where the values of
|
||||
any symbolic bindings are still unknown. The lookup results from these two
|
||||
any checked bindings are still unknown. The lookup results from these two
|
||||
contexts are [combined](#lookup-ambiguity).
|
||||
|
||||
```carbon
|
||||
@@ -525,9 +525,9 @@ fn CallH(a: DerivingWrapper(HasField),
|
||||
}
|
||||
```
|
||||
|
||||
**Note:** All lookups are done from a context where the values of any symbolic
|
||||
**Note:** All lookups are done from a context where the values of any checked
|
||||
bindings that are in scope are unknown. Unlike for a template binding, the
|
||||
actual value of a symbolic binding never affects the result of member
|
||||
actual value of a checked binding never affects the result of member
|
||||
resolution.
|
||||
|
||||
#### Lookup ambiguity
|
||||
@@ -628,7 +628,7 @@ For a simple member access `a.b` where `b` names a member of an interface `I`:
|
||||
- Otherwise, `impl` lookup is not performed.
|
||||
|
||||
The appropriate `impl T as I` implementation is located. The program is invalid
|
||||
if no such `impl` exists. When `T` or `I` depends on a symbolic binding, a
|
||||
if no such `impl` exists. When `T` or `I` depends on a checked binding, a
|
||||
suitable constraint must be specified to ensure that such an `impl` will exist.
|
||||
When `T` or `I` depends on a template binding, this check is deferred until the
|
||||
value for the template binding is known.
|
||||
|
||||
@@ -197,7 +197,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 a symbolic binding,
|
||||
- When the constraint is used explicitly when declaring a checked binding,
|
||||
like a generic parameter or associated constant, of the form
|
||||
`T: Constraint`.
|
||||
- When declaring that a type implements a constraint with an `impl`
|
||||
|
||||
@@ -23,7 +23,7 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
|
||||
- [Qualified member names and compound member access](#qualified-member-names-and-compound-member-access)
|
||||
- [Access](#access)
|
||||
- [Checked-generic functions](#checked-generic-functions)
|
||||
- [Symbolic facet bindings](#symbolic-facet-bindings)
|
||||
- [Checked facet bindings](#checked-facet-bindings)
|
||||
- [Return type](#return-type)
|
||||
- [Interfaces recap](#interfaces-recap)
|
||||
- [Facet types](#facet-types)
|
||||
@@ -685,13 +685,13 @@ fn AddAndScaleGeneric[T: Vector](a: T, b: T, s: f64) -> T {
|
||||
var v: Point_Extend = AddAndScaleGeneric(a, w, 2.5);
|
||||
```
|
||||
|
||||
Here `T` is a facet whose type is `Vector`. It declares a _symbolic binding_
|
||||
Here `T` is a facet whose type is `Vector`. It declares a _checked binding_
|
||||
since it did not use the `template` keyword to mark it as a _template binding_.
|
||||
|
||||
> **References:** The syntax for compile-time bindings was decided in
|
||||
> [proposal #7254](https://github.com/carbon-language/carbon-lang/pull/7254).
|
||||
|
||||
Since this symbolic binding pattern is in a function declaration, it marks a
|
||||
Since this checked binding pattern is in a function declaration, it marks a
|
||||
_[checked](terminology.md#checked-versus-template-parameters)
|
||||
[generic parameter](terminology.md#generic-means-compile-time-parameterized)_.
|
||||
That means its value must be known to the caller at compile-time, but we will
|
||||
@@ -701,11 +701,11 @@ the body of `AddAndScaleGeneric`'s definition.
|
||||
Note that types may also be given compile-time parameters, see the
|
||||
["parameterized types" section](#parameterized-types).
|
||||
|
||||
### Symbolic facet bindings
|
||||
### Checked facet bindings
|
||||
|
||||
In our example, `T` is a facet which may be used in type position in the rest of
|
||||
the function. Furthermore, since it omits the keyword `template` prefix, this is
|
||||
a symbolic binding. so we need to be able to typecheck the body of the function
|
||||
a checked binding, so we need to be able to typecheck the body of the function
|
||||
without knowing the specific value `T` from the caller.
|
||||
|
||||
This typechecking is done by looking at the constraint on `T`. In the example,
|
||||
@@ -863,7 +863,7 @@ An interface's name may be used in a few different contexts:
|
||||
- as a namespace name in
|
||||
[a qualified name](#qualified-member-names-and-compound-member-access), and
|
||||
- as a [facet type](terminology.md#facet-type) for
|
||||
[a facet binding](#symbolic-facet-bindings).
|
||||
[a facet binding](#checked-facet-bindings).
|
||||
|
||||
While interfaces are examples of facet types, facet types are a more general
|
||||
concept, for which interfaces are a building block.
|
||||
@@ -893,8 +893,8 @@ This recovers the original type for the facet, so
|
||||
`(Point_Inline as Vector) as type` is `Point_Inline` again.
|
||||
|
||||
However, when a facet type like `Vector` is used as the binding type of a
|
||||
symbolic binding, the
|
||||
[symbolic facet binding](#symbolic-facet-bindings) `T` is disassociated with
|
||||
checked binding, the
|
||||
[checked facet binding](#checked-facet-bindings) `T` is disassociated with
|
||||
whatever facet value `T` is eventually bound to. Instead, `T` is treated as an
|
||||
[archetype](terminology.md#archetype), with the members and
|
||||
[member access](/docs/design/expressions/member_access.md) determined by the
|
||||
@@ -1022,7 +1022,7 @@ whenever an interface may be. This includes all of these
|
||||
[a qualified name](#qualified-member-names-and-compound-member-access). For
|
||||
example, `VectorLegoFish.VAdd` refers to the same name as `Vector.Add`.
|
||||
- A named constraint may be used as a [facet type](terminology.md#facet-type)
|
||||
for [a facet binding](#symbolic-facet-bindings).
|
||||
for [a facet binding](#checked-facet-bindings).
|
||||
|
||||
We don't expect developers to directly define many named constraints, but other
|
||||
constructs we do expect them to use will be defined in terms of them. For
|
||||
@@ -1115,7 +1115,7 @@ class ImplementsS {
|
||||
There is a subtyping relationship between facet types that allows calls of one
|
||||
generic function from another as long as it has a subset of the requirements.
|
||||
|
||||
Given a symbolic facet binding `T` with facet type `I1`, it satisfies a facet
|
||||
Given a checked facet binding `T` with facet type `I1`, it satisfies a facet
|
||||
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:
|
||||
@@ -1844,7 +1844,7 @@ var thriller_count: Optional(i32) =
|
||||
play_count.Find(Song("Thriller"));
|
||||
```
|
||||
|
||||
Since the `KeyT` and `ValueT` are symbolic parameters, the `Find` function is a
|
||||
Since the `KeyT` and `ValueT` are checked parameters, the `Find` function is a
|
||||
checked generic, and it can only use the capabilities of `KeyT` and `ValueT`
|
||||
specified as requirements. This allows us to evaluate when we can convert
|
||||
between two different arguments to a parameterized type. Consider two adapters
|
||||
@@ -2383,7 +2383,7 @@ fn PeekAtTopOfStack[StackType: StackAssociatedFacet](s: StackType*)
|
||||
Inside the checked-generic function `PeekAtTopOfStack`, the `ElementType`
|
||||
associated facet member of `StackType` is an
|
||||
[archetype](terminology.md#archetype), like other
|
||||
[symbolic facet bindings](#symbolic-facet-bindings). This means
|
||||
[checked facet bindings](#checked-facet-bindings). This means
|
||||
`StackType.ElementType` has the API dictated by the declaration of `ElementType`
|
||||
in the interface `StackAssociatedFacet`.
|
||||
|
||||
@@ -2557,8 +2557,8 @@ class Complex {
|
||||
All interface parameters are checked by default. This reflects these two
|
||||
properties of these parameters:
|
||||
|
||||
- They must be resolved at compile-time, and so can't be passed regular
|
||||
dynamic values.
|
||||
- They must be resolved at compile-time, and so can't be passed runtime
|
||||
values.
|
||||
- We allow either symbolic or template values to be passed in.
|
||||
|
||||
**Future work:** We might also allow `template` bindings for interface
|
||||
@@ -2628,7 +2628,7 @@ support parameters. Those parameters work the same way as for interfaces.
|
||||
|
||||
## Where constraints
|
||||
|
||||
So far, we have restricted a [symbolic facet binding](#symbolic-facet-bindings)
|
||||
So far, we have restricted a [checked facet binding](#checked-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`
|
||||
@@ -2858,7 +2858,7 @@ constraint ContainerIsSlice {
|
||||
|
||||
The `.Self` construct follows these rules:
|
||||
|
||||
- A generic binding `X` introduces a checked generic binding `.Self: type`, where
|
||||
- A checked binding `X` introduces a checked generic binding `.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)`.
|
||||
@@ -2874,7 +2874,7 @@ The `.Self` construct follows these rules:
|
||||
to the same facet binding.
|
||||
- `.Self` may not be on the left side of the `=` in a rewrite constraint.
|
||||
|
||||
So in `X: A where ...` (where `X` is a generic binding), `.Self` is
|
||||
So in `X: A where ...` (where `X` is a checked binding), `.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
|
||||
@@ -3387,7 +3387,7 @@ 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`
|
||||
[checked facet binding](#checked-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`.
|
||||
@@ -3433,7 +3433,7 @@ fn PrintValueOrDefault[
|
||||
```
|
||||
|
||||
In this case, Carbon will accept the definition and infer the needed constraints
|
||||
on the symbolic facet parameter. This is both more concise for the author of the
|
||||
on the checked 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
|
||||
@@ -3445,7 +3445,7 @@ 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 symbolic
|
||||
> **Note:** These implied constraints affect the _requirements_ of a checked
|
||||
> 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.
|
||||
@@ -3758,7 +3758,7 @@ interface Graph {
|
||||
#### Parameterized type implements interface
|
||||
|
||||
There are times when a function will pass a
|
||||
[symbolic facet parameter](#symbolic-facet-bindings) of the function as an
|
||||
[checked facet parameter](#checked-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.
|
||||
|
||||
@@ -3796,7 +3796,7 @@ PrintThree(i, i, i);
|
||||
#### Another type implements parameterized interface
|
||||
|
||||
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
|
||||
a [checked facet parameter](#checked-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`:
|
||||
@@ -3813,7 +3813,7 @@ fn Double[T: Mul where i32 impls As(.Self)](x: T) -> T {
|
||||
|
||||
#### Must be legal type argument constraints
|
||||
|
||||
Now consider the case that the symbolic facet parameter is going to be used as
|
||||
Now consider the case that the checked 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
|
||||
@@ -4229,8 +4229,8 @@ 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:
|
||||
To get a template generic binding instead of a checked generic binding, use
|
||||
`let template`, as in:
|
||||
|
||||
```carbon
|
||||
fn TemplateLet(...) {
|
||||
@@ -4242,8 +4242,8 @@ fn TemplateLet(...) {
|
||||
}
|
||||
```
|
||||
|
||||
which introduces a template constant `T` with type `C` and value `U`. This is
|
||||
roughly equivalent to:
|
||||
which introduces a template generic binding `T: C`, bound to the value `U`.
|
||||
Uses of `T` are then template constants. This is roughly equivalent to:
|
||||
|
||||
```carbon
|
||||
fn TemplateLet(...) {
|
||||
|
||||
@@ -107,7 +107,7 @@ Summary of how Carbon generics work:
|
||||
- _Deduced parameters_ are parameters whose values are determined by the types
|
||||
of the explicit arguments. Generic facet parameters are typically deduced.
|
||||
- A function with a generic parameter can have the same function body as an
|
||||
unparameterized one. Functions can freely mix checked, template, and regular
|
||||
unparameterized one. Functions can freely mix checked, template, and runtime
|
||||
parameters.
|
||||
- Interfaces can require other interfaces be implemented.
|
||||
- Interfaces can [extend](terminology.md#extending-an-interface) required
|
||||
@@ -368,11 +368,11 @@ You may also refer to any of the methods of interfaces required by the facet
|
||||
type using a
|
||||
[qualified member access expression](#accessing-members-of-interfaces).
|
||||
|
||||
A function can have a mix of checked, template, and regular parameters. Each
|
||||
kind of parameter is defined using a different syntax: a checked parameter is
|
||||
uses a symbolic binding pattern, a template parameter uses a template binding
|
||||
pattern, and a regular parameter uses a runtime binding pattern. Likewise, it's
|
||||
allowed to pass a symbolic or template constant value to a checked or regular
|
||||
A function can have a mix of checked, template, and runtime parameters. Each
|
||||
kind of parameter is defined using a different syntax: a checked parameter uses
|
||||
a checked binding pattern, a template parameter uses a template binding
|
||||
pattern, and a runtime parameter uses a runtime binding pattern. Likewise, it's
|
||||
allowed to pass a symbolic or template constant value to a checked or runtime
|
||||
parameter. _We have decided to support passing a symbolic constant to a template
|
||||
parameter, see
|
||||
[leads issue #2153: Checked generics calling templates](https://github.com/carbon-language/carbon-lang/issues/2153),
|
||||
|
||||
@@ -99,6 +99,11 @@ checked generic, and template generic parameters.
|
||||
|
||||
Keywords matching the contextual default are disallowed to ensure consistency.
|
||||
|
||||
[Associated constants](#interface-parameters-and-associated-constants) are
|
||||
always checked generic bindings. This is not a contextual default: no other
|
||||
phase is possible for an associated constant, and so no phase keyword is allowed
|
||||
there.
|
||||
|
||||
The syntax for checked and template parameters was decided in
|
||||
[leads issue #6932](https://github.com/carbon-language/carbon-lang/issues/6932).
|
||||
|
||||
@@ -278,7 +283,7 @@ that don’t instantiate the implementation (for example,
|
||||
|
||||
Early type checking is where expressions and statements are type checked when
|
||||
the definition of the function body is compiled, as part of definition checking.
|
||||
This occurs for regular and checked-generic values.
|
||||
This occurs for runtime values and symbolic constants.
|
||||
|
||||
Late type checking is where expressions and statements may only be fully
|
||||
typechecked once calling information is known. Late type checking delays
|
||||
@@ -296,22 +301,28 @@ corresponding to
|
||||
|
||||
- A _runtime binding pattern_ binds to a dynamic value at runtime. It is the
|
||||
default for explicit function parameters.
|
||||
- A _symbolic binding pattern_ (or generic binding) binds to a compile-time
|
||||
value that is not known when type checking. It is the default for deduced
|
||||
function parameters and parameters to compile-time entities.
|
||||
- A _template binding pattern_ binds to a compile-time value that is known
|
||||
when type checking. It is indicated by the `template` keyword.
|
||||
- A _checked generic binding pattern_ binds to a _symbolic constant_: a
|
||||
compile-time value that is not known when type checking. It is the default
|
||||
for deduced function parameters and parameters to compile-time entities, and
|
||||
the only kind allowed for [associated constants](#associated-entity).
|
||||
- A _template generic binding pattern_ binds to a _template constant_: a
|
||||
compile-time value that is known when type checking. It is indicated by the
|
||||
`template` keyword. Expressions using such a binding are
|
||||
[dependent](#dependent-names) and are
|
||||
[late type checked](#early-versus-late-type-checking) once an instantiation
|
||||
provides the binding's value.
|
||||
|
||||
These patterns use the keywords `runtime`, `generic`, and `template` to override
|
||||
the contextual defaults when necessary.
|
||||
|
||||
The name being declared, which is the identifier to the left of the `:` is
|
||||
called a _binding_, or more specifically a _runtime binding_, _compile-time
|
||||
binding_, _symbolic binding_, or _template binding_. The expression to the right
|
||||
defining the type of the binding pattern is called the _binding type
|
||||
expression_, a kind of [type expression](#type-expression). For example, in a
|
||||
generic binding pattern `T: Hashable`, `T` is the binding (a symbolic binding in
|
||||
this case), and `Hashable` is the binding type expression.
|
||||
binding_, _checked generic binding_, or _template generic binding_. The
|
||||
expression to the right defining the type of the binding pattern is called the
|
||||
_binding type expression_, a kind of [type expression](#type-expression). For
|
||||
example, in a checked generic binding pattern `T: Hashable`, `T` is the binding
|
||||
(a checked generic binding in this case), and `Hashable` is the binding type
|
||||
expression.
|
||||
|
||||
## Types and `type`
|
||||
|
||||
@@ -367,7 +378,7 @@ cases, we are concerned with the type value after the implicit conversion.
|
||||
We use the term _facet binding_ to refer to the name introduced by a
|
||||
[compile-time binding pattern](#bindings) (indicated by context or keywords like
|
||||
`generic` or `template`) where the declared type is a [facet type](#facet-type).
|
||||
In a generic binding pattern `T: Hashable`, `T` is a facet binding, and the
|
||||
In a checked binding pattern `T: Hashable`, `T` is a facet binding, and the
|
||||
value of `T` is a [facet](#facet).
|
||||
|
||||
## Deduced parameter
|
||||
|
||||
@@ -156,19 +156,23 @@ or template compile-time:
|
||||
|
||||
- A _runtime binding pattern_ binds to a dynamic value at runtime. It is the
|
||||
default for explicit function parameters and local bindings.
|
||||
- A _symbolic binding pattern_ (or generic binding pattern) binds to a
|
||||
- A _checked generic binding pattern_ binds to a symbolic constant: a
|
||||
compile-time value that is not known when type checking. It is the default
|
||||
for deduced function parameters and parameters to compile-time entities.
|
||||
Explicit function parameters are only symbolic binding patterns if they are
|
||||
declared using the `generic` keyword.
|
||||
- A _template binding pattern_ binds to a compile-time value that is known
|
||||
when type checking. It is declared using the `template` keyword.
|
||||
Explicit function parameters are only checked generic binding patterns if
|
||||
they are declared using the `generic` keyword.
|
||||
[Associated constants](generics/details.md#associated-constants) are always
|
||||
checked generic binding patterns, and do not allow a phase keyword.
|
||||
- A _template generic binding pattern_ binds to a template constant: a
|
||||
compile-time value that is known when type checking. It is declared using
|
||||
the `template` keyword. Expressions using such a binding are dependent and
|
||||
are late type checked once the binding's value is known.
|
||||
|
||||
> **Future work:** If Carbon supports deduced runtime parameters in the future,
|
||||
> the `runtime` keyword will be used to explicitly declare those runtime binding
|
||||
> patterns.
|
||||
|
||||
A symbolic or template binding pattern is collectively called a _compile-time
|
||||
A checked or template binding pattern is collectively called a _compile-time
|
||||
binding pattern_. A compile-time binding pattern cannot appear inside a `var`
|
||||
pattern.
|
||||
|
||||
@@ -181,13 +185,13 @@ components:
|
||||
entire reference" if it's a variable binding pattern, or "durable non-entire
|
||||
reference" if it's a non-variable reference binding pattern.
|
||||
- The phase is "runtime", "symbolic", or "template" depending on whether the
|
||||
pattern is a runtime, symbolic, or template binding pattern.
|
||||
pattern is a runtime, checked, or template binding pattern.
|
||||
|
||||
During pattern matching, the scrutinee is implicitly converted as needed to have
|
||||
the same extended type, and the binding is _bound_ to (and consumes) the result
|
||||
of these conversions. This makes a runtime or template binding a kind of
|
||||
reusable alias for the converted scrutinee expression, with the same extended
|
||||
type and value. Symbolic bindings are more complex: the binding will have the
|
||||
type and value. Checked bindings are more complex: the binding will have the
|
||||
same type, category, and phase as the converted scrutinee expression, but its
|
||||
constant value is an opaque symbol introduced by the binding, which the type
|
||||
system knows to be equal to the converted scrutinee expression.
|
||||
|
||||
@@ -784,7 +784,7 @@ segment, and let `Ys` be a sequence of tuple segments.
|
||||
### Equivalence, equality, and convertibility
|
||||
|
||||
_Pack renaming:_ Let `Ns` be a sequence of names, let `⟬Ns⟭: «T; N»` be a name
|
||||
binding pattern (which may be a symbolic or template binding as well as a
|
||||
binding pattern (which may be a checked or template binding as well as a
|
||||
runtime binding), and let `__A` be an identifier that does not collide with any
|
||||
name that's visible where `⟬Ns⟭` is visible. We can rewrite all occurrences of
|
||||
`⟬Ns⟭` to `each __A` in the scope of the binding pattern (including the pattern
|
||||
|
||||
Reference in New Issue
Block a user