It's hard to define initial elements for folds without `chooseSome` or similar

[bugarela]

From https://github.com/informalsystems/quint/issues/1235

If we are trying to compute the minimum value of a set of generic type, there's no way of defining a initial value for fold, even though it would work the same with any element of the set.

We should provide a way of arbitrarily picking an initial element. That is arbitrary behavior, but fold itself already introduces arbitrary behavior since the order in which the set is folded is arbitrary.

One additional idea is to introduce some sort of warning when something with arbitrary behavior is used. Then, that warning could be disable by a special comment that makes explicit the assumption of how the arbitrary behavior doesn't matter. Example:

pure def minBy(__set: Set[a], __f: a => int): a = {
  // [safe-arbitrary] any initial value can be picked
  const initial = __set.pick()
  // [safe-arbitrary] any fold order will result in a minimum value
  __set.fold(
    initial,
    (__m, __e) => if(__f(__m) < __f(__e)) {__m } else {__e}
  )
}

[konnov]

I guess, we would be able to solve this issue with sum types by returning None in the case of an empty set. Am I right, @shonfeder?

[bugarela]

We should try to write this with sum types when https://github.com/informalsystems/quint/issues/1073 is done