Proposal to add `?` postfix operator

[ahelwer]

The ? symbol is not currently defined as an operator in TLA+ 2. It was defined as an infix operator in TLA+ v1 (see grammar). I believe it would be useful to define ? as a postfix operator. TLA+ does not have many user-definable postfix operators, and this seems a natural fit for several use cases. Two which come to mind:

Case 1: checking for null

Specs often have a "null" model type which needs to be checked:

---- MODULE Test ----
CONSTANTS Key, Value
VARIABLE kvs
NoValue == CHOOSE v : v \notin Value
Increment(key) ==
  /\ kvs[key] /= NoValue
  /\ kvs' = [kvs EXCEPT ![key] = @ + 1]
=================

The ? operator could be a nice for this:

val ? == val /= NoValue
Increment(key) ==
  /\ kvs[key]?
  /\ kvs' = [kvs EXCEPT ![key] = @ + 1]

Case 2: indicating value is optional

The progenitor of this idea was when I was working with the TLA+ grammar itself. It has constructs like:

set_literal == tok("{") & (Nil | CommaList(G.Expression)) & tok("}") 

This is kind of hard to read. At first I wanted to define an operator Optional, but it could be written more nicely as:

rule ? == Nil | rule
set_literal == tok("{") & CommaList(G.Expression)? & tok("}") 

I'm sure others can come up with even more creative uses.

[xxyzzn]

I don't think ?' was ever an infix operator.??' is and was one, which seems fine to me. Single characters with no current use are rare, and could be useful for future extensions of the language. (Semicolon is the only other one I can think of.) I don't find your use compelling enough to justify not saving it for the future. But in a couple of months, the TLA+ Foundation will be able to do it if you can convince them.

L.

From: Andrew Helwer @.> Sent: Monday, February 13, 2023 11:59 To: tlaplus/rfcs @.> Cc: Subscribed @.***> Subject: [tlaplus/rfcs] Proposal to add ? postfix operator (Issue #6)

Motivation

The ? symbol is not currently defined as an operator in TLA+ 2. It was defined as an infix operator in TLA+ v1 (see grammarhttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Ftlaplus%2FExamples%2Fblob%2F03a1e31245a57143cd0f6613f6b3ce63706fb483%2Fspecifications%2FSpecifyingSystems%2FSyntax%2FTLAPlusGrammar.tla%23L50&data=05%7C01%7Clamport%40microsoft.com%7Cf53d01d298b14113ca2f08db0dfcaf54%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C638119151150499601%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000%7C%7C%7C&sdata=mRJah1khFMuwwDHzwXNkyrdxQxwmodI%2FdqbMpLItPkc%3D&reserved=0. I believe it would be useful to define ? as a postfix operator. TLA+ does not have many user-definable postfix operators, and this seems a natural fit for several use cases. Two which come to mind:

Case 1: checking for null

Specs often have a "null" model type which needs to be checked:

---- MODULE Test ----

CONSTANTS Key, Value

VARIABLE kvs

NoValue == CHOOSE v : v \notin Value

Increment(key) ==

/\ kvs[key] /= NoValue

/\ kvs' = [kvs EXCEPT ![key] = @ + 1]

=================

The ? operator could be a nice for this:

val ? == val /= NoValue

Increment(key) ==

/\ kvs[key]?

/\ kvs' = [kvs EXCEPT ![key] = @ + 1]

Case 2: indicating value is optional

The progenitor of this idea was when I was working with the TLA+ grammar itself. It has constructs like:

set_literal == tok("{") & (Nil | CommaList(G.Expression)) & tok("}")

This is kind of hard to read. At first I wanted to define an operator Optional, but it could be written more nicely as:

rule ? == Nil | rule

set_literal == tok("{") & CommaList(G.Expression)? & tok("}")

I'm sure others can come up with even more creative uses.

- Reply to this email directly, view it on GitHubhttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Ftlaplus%2Frfcs%2Fissues%2F6&data=05%7C01%7Clamport%40microsoft.com%7Cf53d01d298b14113ca2f08db0dfcaf54%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C638119151150499601%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000%7C%7C%7C&sdata=YEehI%2BHOtz4W5XFMUDC%2FXYMBfGFo5n77k34uefKibck%3D&reserved=0, or unsubscribehttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAEUS3OXF4ZK6EUNEV72CGW3WXKG6RANCNFSM6AAAAAAU2WC3SE&data=05%7C01%7Clamport%40microsoft.com%7Cf53d01d298b14113ca2f08db0dfcaf54%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C638119151150499601%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000%7C%7C%7C&sdata=3UkCDjz3zLzvsPef8ssTgxw2htPt09z1oL5OGrF7yn0%3D&reserved=0. You are receiving this because you are subscribed to this thread.Message ID: @.**@.>>

[ahelwer]

@xxyzzn that's a good point, future language features might benefit from being able to use ? as a keyword. Perhaps I will shelve this suggestion for now.