[Question] How to interpret void and what is the difference with never in typespec?

[MaryGao]

In container service fleet tsp we have following definition(tsp here).

  @doc("Lists the user credentials of a Fleet.")
  listCredentials is ArmResourceActionSync<Fleet, void, FleetCredentialResults>;

And the second template argument in ArmResourceActionSync is void, which means the request body is void. So finally we would get similar definition as below.
https://github.com/Azure/typespec-azure/blob/079aa68184a182ad9c954213a18453785c92d598/packages/typespec-azure-resource-manager/lib/operations.tsp#L587-L606

  @doc("Lists the user credentials of a Fleet.")
  listCredentials(@body body: void): FleetCredentialResults;

I was wondering what the void body mean? The same question on how to express void when used as model property, header/query parameter and response body.

[timotheeguerin]

It means there is no body

[MaryGao]

Does that mean we should ignore any property defined by void? Ideally the void could be used in any places like request or response body, header, query parameter or model property.

Also according to the doc, it meantioned void is used for return type not input model.

[MaryGao]

Offline discussed this with @timotheeguerin here is the take-away:

• void as request or response body property means no body property
• void as response means no body
• void as normal property in model(playground), this is not decided yet, the preference is to emit an error for this considering it doesn't make sense to support
• never could also be considered to also mean don’t include the body property which would be consistent with other use of never

never vs void

It seems that never could express the same payload as void, the former means the property is never there; the latter means there is no that property.

In azure core some use never(example) and others use void(example). What is our best practice?

Is the following expression the same? playground

op test(): never;
// vs
op test(): void;

[tadelesh]

from my experiment, i believe never could only used for model property (parameter is also a model property) and means this property not exist, so it could not be used for response type. while void is a type that could be used in any place. idk if it is right for the typespec syntax meaning.

[timotheeguerin]

Yeah never as a response type would mean the operation never returns(not that it has no body) which I’m not really sure what that would mean in http.

[dgetu]

In the interest of not coupling TypeSpec semantics to HTTP internals, never probably ought not actually depend on what happens at the HTTP layer. I think that either the emitter or the client/service should respond with an error while serializing/deserializing something with never type. That doesn't have to have the semantics of not sending a HTTP response - a never response type could mean the HTTP response is always an error, or the transport layer (TCP and maybe UDP/WebSocket in the future) drops the connection on the service side with no response.