paradox about receiver parameter in jls-8.4 and jls-8.8.1

jls-8.4 states that

The receiver parameter is an optional syntactic device for an instance method or an inner class's constructor. For an instance method, the receiver parameter represents the object for which the method is invoked. For an inner class's constructor, the receiver parameter represents the immediately enclosing instance of the newly constructed object.

There is also an example in jls-8.4.1, note the highlighted part

However, jls-8.8.1 states that

The constructor of a non-private inner member class implicitly declares, as the first formal parameter, a variable representing the immediately enclosing instance of the class

So in jls-8.8.1, the parameter in highlighted constructors of above example should be called formal parameter. classfile structure conforms to it, because I can find this parameter in method descriptor and in MethodParameters attribute of the constructor.

But clearly receiver parameter and formal parameter are two different things in jls, see Method Declaration in jls-8.4, Formal Parameters in jls-8.4.1 and Constructor Declaration in jls-8.8.

What's the right kind of such parameter in jls?

Solution

TL;DR: it's not contradictory for the JLS to call this a "formal parameter" in §8.8.1, because §8.8.1 isn't describing a syntactic form.

This is a deceptively subtle question, and we need to be very careful to distinguish between the English language terms "formal parameter" and "receiver parameter", which can have different meanings in different contexts, and the terms FormalParameter and ReceiverParameter defined in the Java grammar, which have specific definitions in any given version of the JLS, but these definitions have changed over time.

The normal semantic meaning of the English term "formal parameter" is given by Wikipedia:

The term parameter (sometimes called formal parameter) is often used to refer to the variable as found in the function definition, while argument (sometimes called actual parameter) refers to the actual input supplied at function call.

Essentially this just means a "parameter", but the word "formal" is used, analogously to the concept of a formal variable in mathematics, to emphasise that we're talking about an abstract variable defined in the source code rather than one existing at runtime which holds the argument's value.

This corresponds with the meaning of the term "formal parameter" in JLS 7, where in Java 7 all parameters are described as formal parameters.

But then Java 8 introduced "receiver parameters" into the language, and the meaning of the term "formal parameter" in the JLS itself changed in a subtle way. At this point we need to draw a distinction between the syntactic form of a formal parameter (i.e. what FormalParameter refers to), and the semantic meaning of a formal parameter.

Grammatically, in JLS 8 §8.4.1 a ReceiverParameter is not a FormalParameter but it is included in FormalParameters and FormalParameterList. This may seem inconsistent, but it reflects the fact that the names of syntactic forms in the grammar don't necessarily correspond with how we would interpret those names in English. (When making changes to the language grammar, there are other interests to balance besides consistency with English.) The spec also states that "If a method or constructor has no formal parameters, only an empty pair of parentheses appears in the declaration"; but a method with only a receiver parameter does not have an empty pair of parentheses. So we might infer that a receiver parameter is a kind of formal parameter, even though a ReceiverParameter is not a kind of FormalParameter.

But this also doesn't tell us anything about implicitly declared parameters, because "implicitly declared" means those parameters are not written in the source code and have no syntactic form. Therefore, when JLS 8 §8.8.1 says:

The constructor of a non-private inner member class implicitly declares, as the first formal parameter, a variable representing the immediately enclosing instance of the class (§15.9.2, §15.9.3).

the English language term "formal parameter" here does not refer to the language grammar. Note also that this paragraph doesn't say that the implicitly declared parameter is a "receiver parameter".

So we have two different but clearly related things:

A receiver parameter, which is a syntactic form whose type annotation is that of the immediately enclosing class and whose name is this qualified by that class name;
The implicitly declared formal parameter, a purely semantic construct with no syntactic form, which is a variable whose type is the immediately enclosing class and whose name is this qualified by that class name.

The relationship between these two things is obvious, but §8.8.1 says that every method or constructor of an inner class has the latter (in order to receive a reference to the enclosing instance at runtime), regardless of whether or not the former is declared in the source code. Since the latter exists whether or not the former does, they are distinct things.

The question then is whether the latter is a receiver parameter, a formal parameter, or both. Since we are talking about the implicit parameter with no syntactic form,

It cannot be a "receiver parameter" according to the syntactic definition of that term in §8.4.1.
But it also cannot be a "formal parameter" according to the definition of that term in §8.4.1, for the same reason: it is only defined there as a syntactic form.

So when §8.8.1 describes this implicitly declared parameter as a "formal parameter", we can only make sense of this by saying that semantically it is a formal parameter; when the method or constructor is invoked, it receives an implicitly passed value (that is, a reference to the enclosing instance) as if it had been declared as a formal parameter and as if the method or constructor invocation had explicitly passed it a value.

So, in context, calling it a "formal parameter" makes more sense than calling it a "receiver parameter", because a (syntactic) formal parameter does affect the semantic meaning of the method or constructor — it creates a parameter variable which receives a value at runtime — whereas the declaration of a (syntactic) receiver parameter does not change the semantic meaning of the method.

All of that said, despite the JLS giving no meaning to the term "receiver parameter" beyond its syntactical definition in §8.4.1, you and I still understand the term "receiver parameter" to have a conceptual meaning, and according to that conceptual meaning we would identify the implicit parameter of §8.8.1 as a "receiver parameter". But our interpretation is not specified in the JLS, and therefore does not refute the JLS calling it a "formal parameter" instead.

As you note in the comments, if we look at version 19 of the Java Language Specification, we can see that the syntactic definitions in JLS 19 §8.4.1 have changed compared to JLS 8: in particular, ReceiverParameter is no longer included in FormalParameters or FormalParameterList.

However, this doesn't change the interpretation of §8.8.1, which still describes the implicitly declared parameter as a "formal parameter". The changes in §8.4.1 should not affect the intepretation of this section, because it is not describing a syntactic form. Really, these changes only affect the structure of a parse tree, and the implicit parameter described in §8.8.1 is never present in a parse tree anyway.

Note also that the use of similar terminology in the Java classfile format has no bearing on this question, because the classfile format is essentially a different language with its own specification (the Java Virtual Machine Specification) which the Java Language Specification does not depend on. The meaning of a program written in Java is defined by the JLS, not the JVMS.