Sets

Sets are one of the most powerful and frequently used compound types in Quint. Because sets carry no notion of ordering and permit no duplicates, their very semantics strip away the incidental complexity and overhead that sequential structures introduce. This makes sets particularly well-suited for specification work, and further differentiates Quint from traditional programming languages such as JavaScript, Python or Go, where arrays and lists predominate as the everyday data structure, and sets are rarely used. Ultimately, understanding and properly utilizing this abstract data structure is a gateway to writing cleaner, more expressive specs, and for improving overall abstract thinking.

What this lesson covers:

• The Set constructor.
• The range operator i.to(j).
• Properties of sets.
• Built-in operators.
• Leveraging Quint’s spells for advanced set operations.

The Set Type

In Quint, sets are expressed through the Set[a] type, which comes with a dedicated constructor and a rich collection of built-in operators. Before diving into those operators, it is worth understanding how sets are created and what properties they carry.

Creating Sets

The most direct way to create a set in Quint is by explicitly enumerating its elements using the Set constructor. This syntax allows you to define collections of any type, as well as empty collections:

Set(1, 2, 3)

Set("a","b","c")

Set()

Alternatively, for sets of consecutive integers, you can use the range operator i.to(j), which produces the set of all integers from i to j, inclusive on both ends:

assert(1.to(5) == Set(1, 2, 3, 4, 5))

assert(3.to(3) == Set(3))

assert(3.to(2) == Set())

Notice that this operator only works if both i and j arguments are integers.

Set Properties

A set is a collection of values preserving the following main properties:

1. All values must be of the same type.

If we try to define a set with values of different types, we will get an error similar to the following:

>>> Set(1,"b")
static analysis error: 
 Error [QNT000]: Couldn't unify int and str
Trying to unify int and str
Trying to unify (_t0, _t0) => Set[_t0] and (int, str) => _t1

2. The collection has a dynamic, variable size.

Unlike other collection types such as tuples (which have a fixed size dictated by their type signature), a Set[a] can hold any number of values of type a. For example, the following variables share the exact same type signature (Set[int]), despite containing a different number of elements:

pure val divisorsOfSix: Set[int] = Set(1, 2, 3, 6)

pure val divisorsOfTwelve: Set[int] = Set(1, 2, 3, 4, 6, 12)

3. The collection is unordered.

This means the order in which you enumerate a set’s elements does not matter. For instance, Set(1,2,3) and Set(3,1,2) are completely interchangeable. You can verify this equivalence in the REPL:

assert(Set(1,2,3) == Set(3,1,2))

4. The collection does not contain duplicates.

Because sets never contain duplicates, any repeated elements are silently dropped. Try it in the REPL:

assert(Set(1,1,2,2,3) == Set(1,2,3))

These elegant properties have direct practical consequences on how you write specifications when working with sets, as they come without the operations that most sequential structures typically offer. For sets there is no indexing, no head or tail, no slicing or splitting by position and no counting of occurrences. Iteration also works differently: rather than a traditional for loop with a predictable traversal order, sets are navigated through fold, whose iteration order is deliberately unspecified, a direct reflection of the fact that sets carry no inherent structure. We will cover the semantics of this advanced operator in a follow-up lesson.

While these constraints may feel a bit restrictive, there is a big tradeoff that compensates for these limitations, and it is the reduction of the state space. Although we will cover model checkers and different ways to run your models in later lessons, it is important to have in mind that a core value of specification languages such as Quint is exhaustive state exploration. This means that, given the right tooling and a well-written spec, it is sometimes possible to investigate every reachable state of your system (a remarkable guarantee). The practical obstacle is that state spaces can easily grow explosively, which makes it computationally infeasible to run such tools to completion. Whether this is achievable depends, to a large extent, on the state space reduction techniques employed and the spec writer’s expertise.

In the case of sets and lists, this plays out concretely: when using lists, variables assigned to List(1,2,3) and to List(3,2,1) (and all the possible permutations) convey two distinct states. If your system does not actually care about order (for example your collection is a set of unique ids), this would be a noisy redundancy that the tooling you execute still has to process. Sets collapse those redundant states into one, making exploration both faster and more tractable.

The rule of thumb is straightforward: whenever order and duplicate occurrences are irrelevant to your system, reach for a set. If they are not, then another of Quint’s composed types may be the right choice.

Built-in Operators

Quint’s set-specific built-in operators can be summarized in the following table:

Observe that sets are not dynamic data structures. They are immutable in the sense that you cannot modify a set in place. Every operation that accepts a set and alters its contents actually evaluates to a brand-new value rather than modifying the existing one.

Many of these operators may feel familiar to you if you have some functional programming background. As you begin writing your specs, you can consult Quint’s cheatsheet  whenever you need a quick overview with a short explanation of the existing language expressions.

The chooseSome() operator corresponds to the “choose” operator in TLA+. You can think of chooseSome() as a placeholder for a function that returns one element of a set. Given the same set, it will always return the same element (think of minimum or maximum over a set of integers). However, chooseSome() does not fix this function. As its behavior is not obvious and does not easily relate to code in programming languages, we suggest not using it unless you are certain that you want it. In most use cases we have encountered, you actually want to filter a set down to a singleton and use getOnlyElement().

Spells

Although comprehensive, this basic set of operations may not immediately cover all your needs regarding sets, and sometimes you will require defining a helper function or a local workaround. To cover for that gap, Quint’s spells  expand the built-in definitions with a curated set of carefully designed new operators. The following is an excerpt from the basicSpells module  showing some of its set-related definitions:

module basicSpells {
 
  /// Remove a set element.
  ///
  /// - @param s a set to remove an element from
  /// - @param elem an element to remove
  /// - @returns a new set that contains all elements of set but elem
  pure def setRemove(s: Set[a], elem: a): Set[a] = {
    s.exclude(Set(elem))
  }
 
  run setRemoveTest = all {
    assert(Set(2, 4) == Set(2, 3, 4).setRemove(3)),
    assert(Set() == Set().setRemove(3)),
  }
 
  /// Adds an element to a set.
  ///
  /// - @param s a set to add an element to
  /// - @param elem an element to add
  /// - @returns a new set that contains all elements of set and elem
  pure def setAdd(s: Set[a], elem: a): Set[a] = {
    s.union(Set(elem))
  }
 
  run setAddTest = all{
    assert(Set(2, 3, 4) == Set(2, 4).setAdd(3)),
    assert(Set(3) == Set().setAdd(3)),
    assert(Set(2,4) == Set(2,4).setAdd(4)),
  }
 
  /// Whether a set is empty
  ///
  /// - @param s a set of any type
  /// - @returns true iff the set is the empty set
  pure def empty(s: Set[a]): bool = s == Set()
 
  run emptyTest = all {
    assert(empty(Set()) == true),
    assert(empty(Set(1, 2)) == false),
    assert(empty(Set(Set())) == false),
  }
}

As you can see, the basicSpells module presents operators for adding an element to a set, removing an element from a set and checking whether a set is empty, among others. Using these operators can improve the readability of your specs, as spells are very declarative. Also, as all the spell modules have been designed with both correctness and efficiency in mind, in many cases, reaching for a spell will produce better results than a quick workaround written on the spot. Make sure you check the rest of Quint’s spells for more helpful definitions.

Summing it up

In this lesson, we covered one of the most important and frequently used compound types in Quint: the Set[a] type. We reviewed how to construct sets manually via the Set constructor or sequentially via the range operator i.to(j). Crucially, we analyzed the four defining characteristics of sets: uniform typing, dynamic size, lack of ordering, and the automatic exclusion of duplicates.

We then examined the practical consequences of these properties. We discussed both the constraints they impose, such as the absence of indexing, slicing, and ordered iteration, and the significant advantage they offer: state space reduction. By collapsing permutations of the same collection into a single state, sets make exhaustive state exploration more tractable, which is one of the reasons they are so central to specification work in Quint. As a general rule of thumb: whenever order and duplicate occurrences are irrelevant to your system’s domain logic, default to a set. Reserve lists and other compound structures strictly for when structure is vital to your specification.

Finally, we surveyed the built-in set operators the language supports and how we can further expand them by using Quint’s spells .