Lists

Lists are the ordered counterpart to sets; they preserve insertion order and allow duplicate elements. While this makes them familiar to most programmers, and an overall more intuitive data structure, it also makes them more expensive for state exploration, which is one of Quint’s core advantages. With this in mind, you should reach for lists only when ordering or duplicates genuinely matter, and default to sets for all other cases.

What this lesson covers:

The List and [] constructors.
The range operator.
Properties of lists.
Built-in operators.
Common and basic list spells.

The List Type

In Quint, the List[a] type comes with dedicated constructors and a rich collection of built-in operators. Before diving into those operators, it is worth understanding how lists are created and what properties they carry.

Creating Lists

Lists can be created by enumerating their elements as a comma-separated list inside the List or [] constructors:


pure val ones: List[int] = List(1, 1, 1)
 
pure val strings: List[str] = ["a","b","c"]
 
pure val emptyList1 = List()
 
pure val emptyList2 = []

Notably, order and duplicates do matter:


assert([1,1,2] != [1,2])
 
assert([2,1] != [1,2])

Alternatively, lists of consecutive integers can be defined with the range(i, j) operator, which produces a list from i (inclusive) to j (exclusive):


assert(range(1, 4) == [1,2,3])

Note: This is different from the to(i, j) operator we covered for sets, which was inclusive on both ends.

List Properties

Here is an overview of the defining traits of lists. Reach for them when your model calls for a data structure aligned with these requirements.

All elements must be of the same type.

Trying to define a list with values of different type will result in an error:


>>> List(1,"b")
static analysis error: 
 Error [QNT000]: Couldn't unify int and str
Trying to unify int and str
Trying to unify (_t0, _t0) => List[_t0] and (int, str) => _t1
 
 
  at <input-0>:0:1
  List(1,"b")
  ^^^^^^^^^^^

The collection does not have a fixed size.

The following variables share the exact same type signature (List[int]), despite containing a different number of elements:


pure val firstFiveFibonacci: List[int] = [0, 1, 1, 2, 3]
                                                                                     
pure val firstEightFibonacci: List[int] = [0, 1, 1, 2, 3, 5, 8, 13]

The collection is ordered.

Unlike sets, List(1, 2, 3) and List(3, 2, 1) are two distinct values. Test this in the REPL:


assert(List(1, 2, 3) != List(3, 2, 1))

Duplicates allowed.

List(1, 1, 2) is a valid and distinct value from List(1, 2):


assert(List(1, 1, 2) != List(1, 2))

The collection has 0-based indexing.

In Quint, a list’s first element is at index 0, not 1. Unlike sets, list elements can be accessed by their position in the list using the element access operator. We can access the ith element of a list by writing the list followed by the position i inside square brackets:


pure val fibonacciFirst: int = firstFiveFibonacci[0]
 
pure val fibonacciSecond: int = firstFiveFibonacci[1]

Built-in Operators

All list-related built-in operators can be summarized in the following table:

Operator	Signature	Description
`List(e_1,..., e_n)`	`(a, ..., a) => List[a]`	New list: duplicates are kept and order is preserved
`[e_1,..., e_n]`	`(a, ..., a) => List[a]`	Same as `List(e_1,..., e_n)`
`range(i, j)`	`(int, int) => List[int]`	New list: integer range from `i` (inclusive) to `j` (exclusive)
`L.length()`	`(List[a]) => int`	Number of elements
`L[i]`	`(List[a], int) => a`	Element at index `i` (0-based)
`L.nth(i)`	`(List[a], int) => a`	Same as `L[i]`
`L.concat(K)`	`(List[a], List[a]) => List[a]`	New list: `K` joined at the end of `L`
`L.append(e)`	`(List[a], a) => List[a]`	New list: `e` added at the end of `L`
`L.replaceAt(i, e)`	`(List[a], int, a) => List[a]`	New list: element at index `i` replaced by `e`
`L.slice(i, j)`	`(List[a], int, int) => List[a]`	New list: sublist of `L` from index `i` (inclusive) to `j` (exclusive)
`L.select(p)`	`(List[a], (a) => bool) => List[a]`	New list: elements of `L` that satisfy `p`
`L.foldl(z, f)`	`(List[a], b, (b, a) => b) => b`	Walk `L` left to right, carrying an accumulator (initially equal to `z`); at each element `e`, update the accumulator to `f(accumulator, e)`. Returns the final accumulator.
`L.head()`	`(List[a]) => a`	First element of `L`
`L.tail()`	`(List[a]) => List[a]`	New list: all elements except the first
`L.indices()`	`(List[a]) => Set[int]`	New set: all valid indices of `L`
`S.allListsUpTo(n)`	`(Set[a], int) => Set[List[a]]`	New set: all lists of elements in `S` with length <= `n`

Spells

There are some common list operations that are not built into Quint, but that you can find in the Spells catalog .

The following table provides a summary of the list-related basic and common spells:

Spell	Signature	Description	Source
`L.sortList(lt)`	`(List[a], (a, a) => bool) => List[a]`	New list: `L` sorted according to `lt`	`basicSpells`
`L.listMap(f)`	`(List[a], (a) => b) => List[b]`	New list: `L` with `f` applied to each of its elements	`basicSpells`
`L.last()`	`(List[a]) => a`	Last element of list `L`	`basicSpells`
`decreasingRange(i, j)`	`(int, int) => List[int]`	New list: integers from `i` down to `j`, both inclusive	`basicSpells`
`L.takeWhile(cond)`	`(List[a], (a) => bool) => List[a]`	Longest prefix of `L` such that all elements in the prefix satisfy `cond`	`basicSpells`
`L1.isPrefixOf(L2)`	`(List[a], List[a]) => bool`	`true` if `L1` is a prefix of `L2`	`basicSpells`
`L.findFirst(f)`	`(List[a], (a) => bool) => Option[a]`	First element of `L` satisfying `f`, or `None` if no such element exists	`basicSpells`
`L.listSum()`	`(List[int]) => int`	Sum of all elements in `L`	`commonSpells`
`L.listContains(e)`	`(List[a], a) => bool`	`true` if `e` is in `L`	`commonSpells`

Summing it up

In this lesson, we covered the List[a] type: a compound type representing an ordered collection of elements. We reviewed how to construct lists using the List and [] constructors, or sequentially via the range(i, j) operator. We analyzed the five defining characteristics of lists: uniform typing, dynamic size, preserved insertion order, allowance of duplicates, and 0-based indexing.

We then examined the practical consequences of these properties. The ordered nature of lists and their tolerance for duplicates make them a natural fit for modeling sequences, logs, and other structures where position and repetition matter. However, these same properties come at a cost: because permutations of the same elements are treated as distinct states, lists produce a larger state space than sets for unordered data. As a general rule of thumb: reach for a list only when ordering or duplicates genuinely matter to your model, and default to sets in all other cases.

Finally, we surveyed the built-in list operators the language supports and how we can further expand them using the list-related spells from basicSpells and commonSpells modules.