Names for similar operators over sets, lists and maps

[bugarela]

Naming is already a hard problem, and we need a lot of different names for similar things since we don't want any name to be overloaded. Currently, we have some sets of names that, for me, are impossible to distinguish by name:

1. length vs size
2. put, with, update
3. select vs filter
4. range vs to
5. mapOf vs mapBy

The IDE can help our users remember which one they need given they use the dot notation and have already written an expression for which we can infer the type (i.e. set(1, 2). triggers autocompletion). However, we should not expect all users to use our LSP when we are making design decisions.

I think having similar names for similar things can be a barrier for people considering to learn the language. Seems like a lot of things to memorize, since there's no good way of rationalizing which operators are defined for each types. Even experienced users might be dependent on an IDE.

Having said that, I do realize it is a hard problem to solve and perhaps that's even our best alternative. Let's consider some other alternatives in this discussions and try to make a recorded decision on this matter.

Alternative 1. Different names (current solution)

Pros:

• Easy to read

Cons:

• Hard to remember without IDE support
• We can run out of names (i.e. we have length and size, what do we do if we want to define a new operator to calculate the size of a map?). Can be a problem for defining libraries.

Alternative 2. Namespacing

Adding some sort of namespace on top of the names. It could be something like @shonfeder suggested, with proper namespaces like List.range and Set.range, which is done by Elixir; or even something simpler like @konnov suggested at some point with filterl for filtering lists.

Pros (both):

• Easy to remember

Cons (proper namespaces):

• Don't work with dot syntax (i.e. list(1,2).List.range)
• Can be pretty noisy while reading and annoying while typing (That's my feeling from using Elixir).

Cons (adding suffixes or prefixes to the names):

• Hard to read (specially out loud). filterl is ok, but some are not: tol, putl ...
• Looks very hacky

Alternative 3. Libraries and imports

If we use proper namespaces with different modules for sets and lists, we can move this out of the core module and users can choose to import one or the other if they don't want to use sets and lists in the same spec. We could also implement qualified importing so they can choose their own namespaces.

import List.*
import Set.filter as setFilter
import Map.* as m

Pros:

• Flexible, users can adapt the names to what's best to their spec
• Easy to read (unless users make weird things)
• Easy to remember
• Easy to extend (I can write my own Seq module with all defs from List and use it instead)

Cons:

• Adds a lot of importing to handle (and you might need to import 6 different modules to specify abstract sort 😝)

Alternative 4. Handle it at the type system

We could dive into the overloading problem and address it with type classes. I can't estimate how hard that would be, perhaps it is worth giving it a try to assess the complexity. Is it necessarily the same problem Apalache had to solve for TLA+? Or can we make it simpler by having more control of the language?

I was actually looking at Haskell and, even tho it has type classes, functions common to sets and lists have conflicting names rather than a constrained generalized type. That makes me concerned that the problem is even harder than I think it is.

Pros:

• (Very) easy to write and remember
• (Very) easy to read
• Easy to extend, as libraries can write instances of type classes

Cons:

• Hard to implement and maintain. For the end user, this could mean bad error messages from the type checker.

[shonfeder]

re: IDE support, we should consider that (afaiu) part of the point of a high-level specification language is that it can be read to provide a clear description of the specified behavior, and while reading the spec people are most likely not to have any IDE at all I think?

[bugarela]

You're right. We should focus on IDE features that make Quint easier to write, and we should never rely on it for reading. However, in this naming problem, I'm arguing we can be relying on the IDE too much for writing.

[shonfeder]

Yep, I agree! I meant this to be an amplification of your point about the importance of not expecting the IDE to fix everything w/r/t naming :D

[konnov]

My understanding is that general programming languages treat every collection (e.g., Set, Sequence, List) as one of the many implementations of the more-or-less the same interface. Some of the collections should be drop-in replacements, such as replacing SortedMap with a HashMap. I cannot tell much about Haskell, but this is the motivation for hiding collections behind interfaces in Java and Scala.

I think there are several historical reasons for following this path:

1. It was understood long time ago that interfaces of collections could be nicely axiomatised. The classical example is a stack:

$$$ \forall s \in Stacks: pop(push(s)) = s $$$

2. Different implementations of the same interface have different performance (typically, measured with amortized complexity)

3. Perhaps, a belief that similar-looking things should have similar-looking names?

I don't think that any of the above points apply in our case. Actually, TLA+ does not have this problem, as there are only sets and functions. We have explicitly partitioned TLA+ functions into maps, lists, tuples, and records. Our language core is still quite small, so there is no real need for extending the language with overloading (which is a big problem for code readers). As for additional operators over the standard collections, we will definitely introduce extension modules, as we have started doing with spells.

[konnov]

I will close this discussion for now, so we can focus on other user stories. But we can always reopen it when we feel we have a few cycles to think about it again.