Define free parameters and concrete #549
Conversation
Havvy
force-pushed the
Havvy:concrete
branch
2 times, most recently
from
e003e82
to
5596bf9
| The *free variables* of an item or type are the type and lifetime variables | ||
| that refer to a generically declared parameter. A *concrete item* or *concrete | ||
| type* is one that does not have any free variables. See [Wikipeida][concrete | ||
| wikipedia] for more. |
Centril
Mar 19, 2019
Contributor
Some general notes about this paragraph that I think are not well captured:
- Bounds/Constraints can also have free variables, e.g.
u8: 'a has 'a as a free variable.
- A lifetime can be concrete:
'static.
Some general notes about this paragraph that I think are not well captured:
- Bounds/Constraints can also have free variables, e.g.
u8: 'ahas'aas a free variable. - A lifetime can be concrete:
'static.
| @@ -83,6 +83,56 @@ where | |||
| } | |||
| ``` | |||
|
|
|||
| ## Free variables and concrete items and types | |||
|
|
|||
| The *free variables* of an item or type are the type and lifetime variables | |||
Centril
Mar 19, 2019
Contributor
Suggested change
The *free variables* of an item or type are the type and lifetime variables
In a given context, the *free variables* of an item or type are the type and lifetime variables
| The *free variables* of an item or type are the type and lifetime variables | |
| In a given context, the *free variables* of an item or type are the type and lifetime variables |
| | Type | Free Variables | | ||
| | `i32` | concrete | | ||
| | `&'a i32` | `'a` | | ||
| | `&'static i32` | concrete | |
Centril
Mar 19, 2019
Contributor
Would be good to have &i32 and say that it has an (anonymous) free (inference) variable.
Would be good to have &i32 and say that it has an (anonymous) free (inference) variable.
Havvy
Mar 21, 2019
Author
Collaborator
How's that?
How's that?
Centril
Mar 21, 2019
Contributor
Well &i32 really means &'_ i32 and _ is a placeholder for something that may be substituted or unified with something else, possibly concrete.
Well &i32 really means &'_ i32 and _ is a placeholder for something that may be substituted or unified with something else, possibly concrete.
Co-Authored-By: Havvy <Ryan.havvy@gmail.com>
|
Rebased against master because of conflicts in |
| itself. Furthermore, `foo` has `A` as a free variable because it uses it as the | ||
| type of its first argument. The function `bar` has `A` as a free type variable, | ||
| getting `A` from the trait's generic parameters. However, the lifetime `'b` is | ||
| bound in `baz` but is free in tye type `&'b SomeStruct`. Both `baz` and `quux` |
Centril
Mar 21, 2019
•
Contributor
Suggested change
bound in `baz` but is free in tye type `&'b SomeStruct`. Both `baz` and `quux`
bound in `baz` but is free in the type `&'b SomeStruct`. All of these functions
also have `Self` as a free variable despite not being explicitly quantified.
| bound in `baz` but is free in tye type `&'b SomeStruct`. Both `baz` and `quux` | |
| bound in `baz` but is free in the type `&'b SomeStruct`. All of these functions | |
| also have `Self` as a free variable despite not being explicitly quantified. |
matthewjasper
Mar 21, 2019
Collaborator
Bound in bar
Bound in bar
Centril
Mar 21, 2019
Contributor
I don't follow...
I don't follow...
| } | ||
| ``` | ||
|
|
||
| In it, the trait `Example` has a free variable `A` because it declares it |
Centril
Mar 21, 2019
Contributor
Suggested change
In it, the trait `Example` has a free variable `A` because it declares it
In it, the trait `Example` has a bound variable `A` because it declares it
| In it, the trait `Example` has a free variable `A` because it declares it | |
| In it, the trait `Example` has a bound variable `A` because it declares it |
| type of its first argument. The function `bar` has `A` as a free type variable, | ||
| getting `A` from the trait's generic parameters. However, the lifetime `'b` is | ||
| bound in `baz` but is free in tye type `&'b SomeStruct`. Both `baz` and `quux` | ||
| have no free type variables and are thus concrete. |
Centril
Mar 21, 2019
Contributor
Suggested change
have no free type variables and are thus concrete.
| have no free type variables and are thus concrete. |
| ``` | ||
|
|
||
| In it, the trait `Example` has a free variable `A` because it declares it | ||
| itself. Furthermore, `foo` has `A` as a free variable because it uses it as the |
Centril
Mar 21, 2019
Contributor
Suggested change
itself. Furthermore, `foo` has `A` as a free variable because it uses it as the
itself. The trait also has `Self` as an implicitly bound variable. Furthermore, `foo` has `A` as a free variable because it uses it as the
| itself. Furthermore, `foo` has `A` as a free variable because it uses it as the | |
| itself. The trait also has `Self` as an implicitly bound variable. Furthermore, `foo` has `A` as a free variable because it uses it as the |
|
The trait example needs to be rewritten, but that can be done as another PR. We also need an actual section on type and item constructors, but that should be its own PR. Further exposition on binders (and how unbinding through item declarations works) should also be done; also as its own PR? Perhaps next time I look at this, since the build just failed? |
|
|
||
| * [Types] | ||
| * Type constructors (for example, `Option` in `enum Option<T> { ... }`) | ||
| * Lifetimes (only lifetime variables) |
Centril
Mar 21, 2019
Contributor
Not sure what you mean by this parenthetical...?
Not sure what you mean by this parenthetical...?
Havvy
Mar 21, 2019
Author
Collaborator
As in, no type variables are allowed in lifetimes.
As in, no type variables are allowed in lifetimes.
Centril
Mar 21, 2019
Contributor
Ah; can you expand to "(only lifetime variables are allowed here)"?
Ah; can you expand to "(only lifetime variables are allowed here)"?
| @@ -83,6 +83,98 @@ where | |||
| } | |||
| ``` | |||
|
|
|||
| ## Formulae and Free Variables | |||
|
|
|||
| The syntatic locations a *variable* is allowed is a *formulae*. Formulae for | |||
Centril
Mar 21, 2019
Contributor
Suggested change
The syntatic locations a *variable* is allowed is a *formulae*. Formulae for
The syntatic locations a *variable* is allowed is a *formulae*.
Formulae which may include type and lifetime variables are:
| The syntatic locations a *variable* is allowed is a *formulae*. Formulae for | |
| The syntatic locations a *variable* is allowed is a *formulae*. | |
| Formulae which may include type and lifetime variables are: |
| ## Formulae and Free Variables | ||
|
|
||
| The syntatic locations a *variable* is allowed is a *formulae*. Formulae for | ||
| type and lifetime variables are: |
Centril
Mar 21, 2019
Contributor
Suggested change
type and lifetime variables are:
| type and lifetime variables are: |
| * `<T>` in `fn identity<T>(x: T) -> T { x }` for item constructors | ||
| * [Traits] and [implementations] implicitly bind `Self` | ||
|
|
||
| All type and lifetimes are unbound at the boundaries of items. |
Centril
Mar 21, 2019
Contributor
Suggested change
All type and lifetimes are unbound at the boundaries of items.
All types and lifetimes are unbound at the boundaries of items.
| All type and lifetimes are unbound at the boundaries of items. | |
| All types and lifetimes are unbound at the boundaries of items. |
| * `<T>` in `fn identity<T>(x: T) -> T { x }` for item constructors | ||
| * [Traits] and [implementations] implicitly bind `Self` | ||
|
|
||
| All type and lifetimes are unbound at the boundaries of items. |
Centril
Mar 21, 2019
Contributor
Also not sure what this sentence is saying...
Also not sure what this sentence is saying...
Havvy
Mar 21, 2019
Author
Collaborator
T'was the last thing I wrote before my brain turned off. I need to expand it, but it's the fact that in the following example, CONST has no free variables, whether implicitly Self from traits or the generic parameter T of the function itself:
fn generic<T>(t: T) {
const CONST: () = ();
}
T'was the last thing I wrote before my brain turned off. I need to expand it, but it's the fact that in the following example, CONST has no free variables, whether implicitly Self from traits or the generic parameter T of the function itself:
fn generic<T>(t: T) {
const CONST: () = ();
}
Centril
Mar 21, 2019
Contributor
Ah yes; that's a good point, we don't have scoped type variables. Be careful not to imply that this applies to bar in trait Foo { fn bar(); } because Foo and bar are both in the syntactic category of items here.
Ah yes; that's a good point, we don't have scoped type variables. Be careful not to imply that this applies to bar in trait Foo { fn bar(); } because Foo and bar are both in the syntactic category of items here.
| Formulae nest. For example, in a function item, the entire function item is a | ||
| formulae but so are the types of the parameters of the function. A type or | ||
| lifetime variable may be free in one formulae but bound in a containing | ||
| formulae. For example, in the function prototype `for<'a> fn foo(a: &'a i32>`, |
Centril
Mar 21, 2019
Contributor
Suggested change
formulae. For example, in the function prototype `for<'a> fn foo(a: &'a i32>`,
formulae. For example, in the function prototype `for<'a> fn foo(a: &'a i32)`,
"prototype"?
| formulae. For example, in the function prototype `for<'a> fn foo(a: &'a i32>`, | |
| formulae. For example, in the function prototype `for<'a> fn foo(a: &'a i32)`, |
"prototype"?
Havvy
Mar 21, 2019
Author
Collaborator
Name for everything of a function except the block expression. The part you can put in a trait. Do you have a better name?
Name for everything of a function except the block expression. The part you can put in a trait. Do you have a better name?
Centril
Mar 21, 2019
Contributor
I'd call this "function signature" or "function declaration".
I'd call this "function signature" or "function declaration".
| formulae but so are the types of the parameters of the function. A type or | ||
| lifetime variable may be free in one formulae but bound in a containing | ||
| formulae. For example, in the function prototype `for<'a> fn foo(a: &'a i32>`, | ||
| `'a` is bound by the `for<'a>` but in the formulae of the type |
Centril
Mar 21, 2019
Contributor
Suggested change
`'a` is bound by the `for<'a>` but in the formulae of the type
`'a` is bound by the binder `for<'a>` but in the type
| `'a` is bound by the `for<'a>` but in the formulae of the type | |
| `'a` is bound by the binder `for<'a>` but in the type |
| formulae while having no free variables when looked at as another formulae. Most | ||
| commonly, the type or item will have a free variable when the type or item | ||
| constructor does not. For example, `Option<T>` as a type has `T` as a free | ||
| variable but as a type constructor, has no free variables. |
Centril
Mar 21, 2019
Contributor
Suggested change
variable but as a type constructor, has no free variables.
variable but as a type constructor, `Option` has no free variables.
(it's not the same type expression so it's not a valid example)
| variable but as a type constructor, has no free variables. | |
| variable but as a type constructor, `Option` has no free variables. |
(it's not the same type expression so it's not a valid example)
|
cc @Havvy -- this is waiting for you if you want to pursue this further :) |
|
Every time I get back to this, I always lead myself into an unhappy path. So closing. |
Fixes #548
I'm dissatisfied by just having two definitions and then mostly showing examples. But still better than nothing.
And while they're called "free variables" elsewhere, while we say they're generic parameters, I'd also like to call them "free parameters". I'd be willing to change
generic parameter->generic variable.