Tuple unpacking

[thpani]

We introduced tuple unpacking in #362.
This was in support of naming tuple fields, and to avoid repeating tuple accessors like t._1.

There's some issues with the current design. Consider the following snippet:

pure def c(tup, f) = Set(tup).map(f) 
pure def func(p, g) = p 
pure val test = c((1, 2), func) 

This spec type-checks, but REPL gives undefined value for test.

There's also the question of how to statically type these definitions; e.g., above, the Set constructor is variadic.

Even if we omit Set, it is unclear how to type, for example, the following

pure def c(tup, f) = f(tup)

We should revisit how we do tuple unpacking, and whether we need better syntax for it.
Also, this solution should factor in feasibilty of transpiling to Apalache.

I will think it through once more, but atm I don’t see a way to make this work for built-ins in the Apalache transpiliation. IMO we need a first-class unpacking construct in Quint, or at least unpacking reflected in the Quint IR, or a first-class unpacker in Apalache.

Initial comments (captured from Slack):

@bugarela:

• My initial feeling is that we shouldn't unpack in the Set constructor, perhaps as a general thing for all multi-arity operators
• In typescript, you have the distinction between (a, b) => ... and ([a, b]) => ... ([] being the constructor for tuples

@shonfeder:

• we should only unpack tuples into tuples, and not unpack n tuples into n-arity operators
• Or maybe a special unpacking syntax is called for, like in Python or Scala.
• iiuc, destructuring on tuples should look like (((a,b)) => foo)(1,2)

@thpani:

• If you write t._1 a lot, you probably want a record
• The only remaining use case is tuples
• while \X is prevalant in TLA+, I have a feeling we're using tuples a lot less in more recent specs

[thpani]

I discussed synchronously with @konnov, and we agreed that we should have explicit syntax for tuple unpacking, similar to what @shonfeder suggested above.

In the simple case where a lambda takes a tuple, this would look like

tuples(S, T).filter( ((s,t)) => p(s,t) )

In the example above, the "uncurrying" would be made explicit:

pure def c(tup, f) = Set(tup).map( ((x, y)) => f(x, y) )
pure def func(p, g) = p 
pure val test = c((1, 2), func) 

@bugarela @shonfeder WDYT?

[bugarela]

I like this, seems super intuitive.

[shonfeder]

I like it too!