Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Clarify checked vs unchecked parameters #1443

Closed
wants to merge 1 commit into from
Closed
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 21 additions & 7 deletions docs/design/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
- [Name lookup](#name-lookup)
- [Name lookup for common types](#name-lookup-for-common-types)
- [Generics](#generics)
- [Checked and template parameters](#checked-and-template-parameters)
- [Checked and unchecked parameters](#checked-and-unchecked-parameters)
- [Interfaces and implementations](#interfaces-and-implementations)
- [Combining constraints](#combining-constraints)
- [Associated types](#associated-types)
Expand Down Expand Up @@ -2226,18 +2226,21 @@ being passed as a separate explicit argument.
> - Proposal
> [#950: Generic details 6: remove facets](https://github.com/carbon-language/carbon-lang/pull/950)

### Checked and template parameters
### Checked and unchecked parameters
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think we want to change terminology here, we arrived at this after some iteration and consideration. Note that there are actually three kinds of parameters: checked, template, and dynamic, and that the template choice is still checked, just later (you use the word "defer").

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is a dynamic parameter? What do you mean "defer"?

Copy link
Contributor

@josh11b josh11b Jul 25, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A dynamic parameter has a value that is passed at runtime, not compile time, like x: i32.
A function with a template parameter is still type-checked, but the type-checking is delayed ("deferred") until the function is instantiated with the value for that parameter is known from the caller. So really "checked" means "eagerly checked" and "template" means "checked on instantiation" not "unchecked".

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wanted to explain a bit more where I'm coming from.

C++ has two kinds of parameters: function parameters and template parameters. And then template parameters are divided further into kinds - type, non-type, and template. We don't currently have checked type template parameters (although we briefly did, and maybe we will again at some point).

Carbon doesn't really meaningfully have that top-level split - so I suppose it would more make more sense to talk about compile-time parameters versus run-time parameters, and then divide up the compile-time parameters into kinds of compile-time parameters: the ones that are checked and the ones that are not. I realize that "template" doesn't mean "literally never checked", but since that also doesn't make sense as a categorization -- it's not like Carbon is going to start deferring type errors to runtime -- it doesn't really seem worthwhile to dedicate a useful term to a use-case that doesn't really exist.

Using the term "template" to refer to unchecked compile-time parameters sort of makes sense for users coming from C++, in the sense that all of our parameters are (currently) unchecked, and so you have that similarity there -- this label indicates that it is more like a C++ template parameter. But it also doesn't make sense for the same reason - again for users coming from C++, checked compile-time parameters are also very much template parameters. If C++ ever adds checked template parameters in the future, the term would then become even more confusing.

This is why I would suggest checked vs unchecked - it accurately and directly describes the meaning of these parameters, in a way that is neither confusing for those coming from C++ (wherein the checked parameters are still template parameters) or for those not coming from C++ (who won't know what a template is and why this keyword is used here).

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it may be useful to expand a little bit about what we mean by "checked".

For me, I think "checked" as meaning "definition type-checked". Not just "type-checked". Everything is type-checked, but only "checked generic parameters" are type-checked in the definition.

But when I see "unchecked", I don't put the "un-" negation on "definition" and read it as "type-checked, but not in the definition". Instead, my brain jumps to "not type-checked at all" which isn't accurate. This is an unfortunate assymetry, I think this is why there is reluctance to have the contrast be between "checked" and "unchecked". The presence of the second term makes me mis-interpret both to be about type-checking at all.

I think "template generic parameters" works well, but not just because C++ templates currently work this way, but because this matches the meaning of the word "template" -- it isn't a type checked entity, it is just a template for some type-checkable entity that needs to be filled in with a concrete type. Only once it is filled in, is it not "templated".

Personally, I don't feel like we should try to avoid a future change to C++ that causes the word "template" to also be associated with something that isn't really "templated" in this way any longer. I understand the concern, but it is about a hypothetical future that hasn't happened and seems hard to predict.

If we had a word that was effective at conveying the right meaning here to our audience ("a template for code, which can't be type checked fully yet, but will be type checked once the templated parameters are filled in") and also avoided this risk, that would be great, but for me at least "template" (even with its problems as you point out) is much more effective at guiding people to the right understanding than "unchecked", especially in conjunction with "checked".


The `:!` indicates that `T` is a _checked_ parameter passed at compile time.
"Checked" here means that the body of `Min` is type checked when the function is
The `:!` indicates that `T` is a type that is bound at compile time. There are
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

:! parameters need not be types, we also support non-type compile-time parameters, like C++'s non-type template parameters.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I can change "type" to "parameter"?

two forms of parameters: checked and unchecked. A parameter declared with the
`template` keyword is an _unchecked parameter_, a parameter declared without the
`template` keyword is a _checked parameter_.

"Checked" here means that the body of `Min` (above) is type checked when the function is
defined, independent of the specific type values `T` is instantiated with, and
name lookup is delegated to the constraint on `T` (`Ordered` in this case). This
type checking is equivalent to saying the function would pass type checking
given any type `T` that implements the `Ordered` interface. Then calls to `Min`
given any type `T` that implements the `Ordered` interface. Subsequent calls to `Min`
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why this change? Is there something ambiguous about the text before?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's just not a good use of "then" - it reads very awkwardly. What you want to say are that any calls to Min made after definition checking have to do something. A word like "subsequent" or "future" or "later" or something is just better.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@jonmeow Could you chime in here, do we have any style guidance for "then"?

Copy link
Contributor

@jonmeow jonmeow Jul 26, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"Then" should typically be used to refer to a direct action sequence, for example:

First, we create an object. Then, we type check it.

"Subsequent" is closer to "Afterwards" in its sense, indicating a time ordering but not an immediate sequence.

https://diffsense.com/diff/subsequent/then

Here, "then" isn't used to refer to a specific consecutive action; instead, it's referring to potential future actions (and in plural). In that context, I do agree "Subsequent" is a better choice.

** I don't think the developer style guide makes a statement here, I think this is just a question of what the word means.

only need to check that the deduced type value of `T` implements `Ordered`.

The parameter could alternatively be declared to be a _template_ parameter by
prefixing with the `template` keyword, as in `template T:! Type`.
The following example uses an unchecked template parameter, `U`:

```carbon
fn Convert[template T:! Type](source: T, template U:! Type) -> U {
Expand All @@ -2252,6 +2255,17 @@ fn Foo(i: i32) -> f32 {
}
```

An unchecked parameter can still use a constraint. The earlier example could have
been declared as:

```carbon
fn Min[template T:! Ordered](x: T, y: T) -> T {
return if x <= y then x else y;
}
```

This defers checking to the point of instantiation (similar to C++ templates).

Carbon templates follow the same fundamental paradigm as
[C++ templates](<https://en.wikipedia.org/wiki/Template_(C%2B%2B)>): they are
instantiated when called, resulting in late type checking, duck typing, and lazy
Expand Down