Add getOnlyElement() built in operator

[bugarela]

Hello

Context

chooseSome is a tricky operator to implement as, in theory, it should be deterministic. However, people are struggling with the lack of chooseSome even in scenarios with no room for non-determinism. So, we decided to at least give them something that only works in this scenarios: getOnlyElement.

This won't help with cases like choosing a base element for fold, but it will help in scenarios that involve taking the single element of a singleton (a set with exactly one element).

General example: MySet.filter(e => e.name == "Gabriela"). If I know that names are unique in this set, I know that this will result in a singleton. I should be able to extract the element out of it.

Special case - when I want to evaluate f(x) for an element of the set, and I know that f(x) has the same exact result for all elements in the set (∀ x,y ∈ S : f(x) = f(y)).

• I can write MySet.map(f) and obtain a singleton
• I'd like to extract the result of f(x) for any element x, which is now the only element in this set.

getOnlyElement() is enough for these scenarios.

Behavior

This operator only works in singletons. If it is called with a set of size different than 1, it will result in an error.

Apalache

I still haven't added this to the Apalache translation. We should somehow force a similar behavior to Quint* when it is called with a non-singleton (as opposed to allowing Apalache to do a not-fully-deterministic choice using it's own CHOOSE implementation). I'm thinking something like:

\* S.getOnlyElement()
LET 
  __S == IF Cardinality(S) == 1 THEN S ELSE {} 
IN 
  CHOOSE x \in __S: TRUE

• Unfortunately, runtime errors in Quint just mean undefined behavior in Apalache, which can hide errors. But this is already a problem with other instances of runtime errors.

• Tests added for any new code
• Documentation added for any new functionality
• Entries added to the respective CHANGELOG.md for any new functionality
• Feature table on README.md updated for any listed functionality

[konnov]

Perhaps, you could just use fold on the set? You could even return None on the empty set and Some(e) on the first element.

Please do not use Cardinality(S) in Apalache. It is a very expensive operator in the SMT encoding.

[bugarela]

Perhaps, you could just use fold on the set? You could even return None on the empty set and Some(e) on the first element.

This is a workaround, but it doesn't make the assumption that the set is a singleton explicit - and calling a fold on a set with many elements means that the result depends on the order of fold, and then we end up with the same problem as in chooseSome (where we don't guarantee determinism). The origin of this discussion is that @josef-widder was using this hack in his specs.

I actually wrote this different hacky version:

pure def getOnlyElement(s: Set[a]): a = {
  pure val hack = s.map(e => ("value", e)).setToMap()
  if (s.size() != 1) {
    hack.get("error: expected singleton")
  } else {
    hack.get("value")
  }
}

But I think having the builtin support with proper error messages is a better idea.

Also on this topic, I'm planning to make the Option type a builtin and adding unwrap(). Since we already have runtime errors, it's a matter of time before people start writing stuff like my hack to use the existing runtime errors to emulate runtime errors of their own. This was discussed in a Quint co-design meeting, and we don't think adding the ability to throw errors is a good idea, as people might start asking for a way to rescue those errors and we definitely don't want to go on that direction. So we though unwrap() should be enough. And then, using Option types for cases where we can assume things will be much better.

Please do not use Cardinality(S) in Apalache. It is a very expensive operator in the SMT encoding.

Oh right! I guess I can write

\* S.getOnlyElement()
CHOOSE x \in S: S = {x}

I was playing with some versions to see if Apalache would report an error for an empty S in any forms - that's when I pinged you on Signal.

[konnov]

This is a workaround, but it doesn't make the assumption that the set is a singleton explicit - and calling a fold on a set with many elements means that the result depends on the order of fold, and then we end up with the same problem as in chooseSome (where we don't guarantee determinism). The origin of this discussion is that @josef-widder was using this hack in his specs.

Well, in this case, you could still use chooseSome and throw an error when it is applied to a non-singleton set? I am a bit worried about adding a lot of new operators. This would increase the surface for all the tools around Quint.

[konnov]

This was discussed in a Quint co-design meeting, and we don't think adding the ability to throw errors is a good idea, as people might start asking for a way to rescue those errors and we definitely don't want to go on that direction

Good. Please do not add any kind of exceptions. This makes program analysis much harder. You can model unwrap with if-then-else internally.