Documentation of nameonly and default values for formals #3903
Conversation
docs/DafnyRef/Types.md
Outdated
| may be called as either | ||
| <!-- %check-resolve %use f.tmp --> | ||
| ```dafny | ||
| const i := f(1,2); |
docs/DafnyRef/Types.md
Outdated
| const i := f(1,2); | ||
| const j := f(1); | ||
| ``` | ||
| where `f(1)` is equivalent to `f(1,10)` in this case. |
docs/DafnyRef/Types.md
Outdated
| The above function may be called as | ||
| <!-- %no-check --> | ||
| ```dafny | ||
| var k := f(y:=10, x:=2); |
There was a problem hiding this comment.
Add a space on both sides of :=
docs/DafnyRef/Types.md
Outdated
| Formal parameters may also be declared `nameonly`, in which case a call site | ||
| must explicitly name the formal when providing its actual argument. |
There was a problem hiding this comment.
I think it would be nicer to explain nameonly after explaining (in lines 4522-2527) that actual parameters may be given by name.
docs/DafnyRef/Types.md
Outdated
| as opposed to _required_. All required parameters must be declared | ||
| before any optional parameters. |
There was a problem hiding this comment.
No, this is no longer true (once #3864 is merged). A required parameter is allowed to follow an optional parameter, provided the required parameter is nameonly. (It may be best to omit the sentence here and explain this below, after nameonly has been introduced.)
Actually, L4538 says what needs to be said.
There was a problem hiding this comment.
Removed the sentence.
docs/DafnyRef/Types.md
Outdated
| ```dafny | ||
| function ff(x: int, nameonly y: int): int | ||
| ``` | ||
| may be called only using `ff(0, y := 4)`. A `nameonly` formal may also have a default value and thus be optional. |
There was a problem hiding this comment.
"only" here feels a bit confusing. For one, the parameters don't have to be passed in as 0 and 4. But also, one can call ff with ff(y := 4, x := 0).
docs/DafnyRef/Types.md
Outdated
| may be called only using `ff(0, y := 4)`. A `nameonly` formal may also have a default value and thus be optional. | ||
|
|
||
| Any formals after a `nameonly` formal must either be `nameonly` themselves or have default values. | ||
| Otherwise an error will result when an attempt is made to call the function or method with such a formal list. |
There was a problem hiding this comment.
L4539 describes the motivation for L4538, from the language-design perspective. If L4538 is violated, Dafny will give an error for the declaration of the formals, so what happens at a call site is a moot point. I suggest keeping just L4538 and deleting L4539.
There was a problem hiding this comment.
In this code
function f(x: int, nameonly y: int, z: int): int
const c := f(0, y:=0)
Dafny gives an error on the const declaration, but not on the function.
There was a problem hiding this comment.
Apparently, this has been fixed since Dafny 4.0. We now get an error on the function declaration as well.
docs/DafnyRef/Types.md
Outdated
| The formals of datatype constructors are not required to have names. Such formals may have default values but | ||
| may not be declared `nameonly`. Such nameless formals must be declared before `nameonly` formals. |
There was a problem hiding this comment.
No, a nameless formal is neither allowed to have a default value nor allowed to be declared nameonly. Also, missing here is the rule that a nameless formal parameter is not allowed to follow an optional parameter. I suggest replacing the second and third sentences with "A nameless parameter is not allowed to follow a parameter with a default value.".
There was a problem hiding this comment.
OK, but I would think a default value for a nameless formal to be a perfectly reasonable thing.
There was a problem hiding this comment.
I agree. It would be a perfectly reasonable thing. We could add it in the future.
docs/DafnyRef/Expressions.md
Outdated
| At a call site, positional arguments are not allowed to follow named arguments. Therefore, if `x` is a nameonly parameter, then there is no way to supply the parameters after `x` by position. | ||
| Thus, any parameter that follows `x` must either by passed by name or have a default value. | ||
| That is, if a later (in the formal parameter declaration) parameter does not have a default value, it is effectively nameonly. |
There was a problem hiding this comment.
Since this paragraph explains "effectively nameonly", you may want to add a similar paragraph that explains "effectively required" (see #3864).
There was a problem hiding this comment.
Actually, I found the 'effectively' terminology unhelpful -- better is simply stating and enforcing the rules about which formals can be optional and which can be nameonly.
Fixes #
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.