Use of frozenset and frozendict in the manual

[Alexander-N]

Thank you for writing the TLA+ Language Manual for Engineers, I think it's a great resource and I was really missing something like this! To look up syntax I often reached for https://learntla.com/tla/ which was never intended as a reference.

I also like the idea of the Python examples a lot, but the use of frozenset and frozendict spoils it a bit for me. For example what could be very similar code

{ 1 } \ { 1 } = { "a" } \ { "a" }

{ 1 } - { 1 } == { "a" } - { "a" }

now becomes the noisy

frozenset({ 1 }) - frozenset({ 1 }) == frozenset({ "a" }) - frozenset({ "a" })

Also the frozendict examples don't run without a dependency which does not work on recent Python versions.

Generally I think the examples would benefit from making the analogy a bit more liberal, does it really matter if we iterate over a range(1, 4) or a frozenset({ 1, 2, 3 }) in Python?

For example

# TLA:
#  [ n \in 1..3 |->
#      [ i \in 1..n |-> n + i ]][3][2]
S3 = frozenset({ 1, 2, 3 })
f3 = frozendict({
    n: frozendict({
      i: n + i
        for i in frozenset(range(1, n + 1))
    })
        for n in S3
  })
f3[3][2]

Could be

{ n: { i: n + i
      for i in range(1, n + 1) }
        for n in range(1, 4) }[3][2]  # 5

I'm aware that there are some examples which have sets in sets, in these cases we could keep frozenset in the necessary places, like { frozenset({1}) } - {1, 2} instead of frozenset({frozenset({1})}) - frozenset({1, 2}).

If you think that this is a good idea, I wouldn't mind converting the examples.

[konnov]

Hi Alexander,

Thank you for the kind words. We also felt that a concise reference manual was missing.

I now see that our code is not optimal for the common-case scenarios. When I was writing the python examples, I was thinking about the most general case.

You have a point about simplifying the examples. Although I would like to keep the general ones too, how about adding the examples that you have in mind as a starter? You could give your examples under the assumption about the type of a data structure, e.g., Set(Int). This would go well with our approach of enforcing types in TLA+ specifications, see ADR002.

As for frozenset and frozendict, you are right. It looks like we would have to add our custom SET and FUN classes, to make these examples more durable against different versions of python. In the future, I would like to explain most of TLA+ in terms of a programming language that most engineers know. Python seems to be the common denominator.

Best regards,
Igor

[Alexander-N]

I'm open to contributing this if it makes sense, but I'm having trouble picturing how to add the modified examples without confusing the reader. My main suggestion is to simply remove the use of frozenset and frozendict, as in

{ 1 } - { 1 } == { "a" } - { "a" }

vs

frozenset({ 1 }) - frozenset({ 1 }) == frozenset({ "a" }) - frozenset({ "a" })

I think I'm missing something so I'll lay out my naive point of view to clear things up. Sets like everything in Python are mutable by default and frozensets have mainly the niche use case to make them hashable, for example to enable sets in sets. For dicts this is so uncommon that frozendict is not even part of the language. I'm confused about what mutability means in the context of TLA+, I thought of it as being independent of such implementation details [1].

I'm afraid I also don't understand the point about the generality, aren't these very concrete examples where e.g. integers are used?

[konnov]

I'm afraid I also don't understand the point about the generality, aren't these very concrete examples where e.g. integers are used?

I see. You are right. When it comes to integers your examples are perfectly fine. Here is what I meant by generality. Imagine that we have a translator from untyped TLA+ to python. The translator would produce that code with frozen sets, which is, of course, suboptimal. If the translator knew about the types, it could produce your code.

I'm confused about what mutability means in the context of TLA+, I thought of it as being independent of such implementation details [1].

Mutability is entirely python's issue in our examples. You are right in that TLA+ is completely free of such details. Unfortunately python's sets and dicts are mutable and this raises the problems with complex data structures such as sets of sets, sets of functions, or functions of sets, etc. If we were dealing with a typed fragment of TLA+, we could translate this fragment in a much nicer looking code e.g. in Scala.

[konnov]

That said, I think your examples would serve as a perfect starting point. I also see a great value in starting with your examples, as they will help the reader to get the semantics in smaller chunks. We just have to say that these examples work under the assumption that the data structures are flat, that is, they can only contains Booleans, integers, and strings.

Since we are finishing the new type checker, this is a reasonable assumption. We will be able to check that automatically.

[Alexander-N]

Ok, then I will just start with a smaller PR where we can settle the details.

[lemmy]

To me, this discussion about a mathematical set and sets in PLs perfectly demonstrates that TLA+ is not programming. It also shows the challenges created by introducing TLA+ through a programming language. I'd suggest making this more explicit and, perhaps, even point readers at an excerpt of this thread to show them the advantages of a spec language.