[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Possible new language constructs for TLA+3?

TLA+ as a language is pretty much perfect, but there are a couple scenarios where I wish for additional language constructs/features:

Combined set-builder notation

When defining a set with set-builder notation, we have two options:

I often find myself wanting to both map and filter at the same time, which requires the following somewhat cumbersome _expression_:

I think this would be much improved in readability if we had a language-level construct similar to:

This is similar to set comprehensions in Python, which is probably my favorite feature of that language.

EXCEPT support for nested functions

Many of the specs I write are of distributed systems, so I'll usually have one or more variables of this type:

When I want to update a single value in distributedData, I use this notation:

It would be nicer if we could write it something like this:

I recall this also as a common point of confusion among TLA+ course attendees, who intuitively tried this notation at first.

I'm not sure whether either of these suggestions violate some bedrock principle in the TLA+ construction (I could see that for the latter) but they certainly would both make my life simpler and reduce the cognitive overhead of reading/writing TLA+.

New standard module: Query

Not a fully fleshed-out idea, but it might be nice to have a new standard module that implements something like relational algebra for easy manipulation of sets of records, in addition to other common higher-level functions like fold and zip.

Anyone else have suggestions of their own?