Types in Quint

Contrary to TLA+, Quint is a statically typed language. This means that the types of all variables, constants, parameters and return values must be known before the specification is run. Hence, static analysis performed by a type checker can verify type consistency on very early stages of the modeling, providing near-instant feedback from the very first drafts of the specification.

What this lesson covers:

• Quint’s static type system: annotations and inference.
• Basic types: bool, int, str.
• Compound types: records, sets, maps, lists, tuples and operators.
• Type aliases: alternative names to types for readability, maintainability and avoidance of repetition.
• Polymorphism and type variables: operators and functions that work for any type.
• Sum types and pattern matching: define values that can be one of several distinct variants, and inspect them via match.
• Uninterpreted types: for abstract modeling.

Type System

In Quint the general rule is that every definition must be either type-annotated or inferable. In a nutshell, this means all variables and constants must be annotated with a type, whereas definitions such as operators and expressions may have their type annotation omitted, as long as their type is inferable by the type checker.

Type annotations use the : type syntax on variables, constants, operator parameters and return values. So declaring a variable can be very straightforward:

var counter: int

Removing the : int annotation in this example will fail to type-check, since variables always require explicit type annotations. Operators on the other hand can often omit them, as sometimes the type checker is able to infer the types from the definition body:

pure def is_even(x) = x % 2 == 0

In this case, Quint’s typechecker is able to infer that parameter x must be of type int, as well as the return value of the operator. The same definition but with complete type annotations looks like this:

pure def is_even(x: int): bool = x % 2 == 0

Basic Types

Quint has three primitive types: booleans, integers and strings:

Values of these types can be declared as follows:

// bool: negation of true
pure val not_true: bool = not(true)
 
// int: maximum value for a 32-bit unsigned integer
pure val max_uint32: int = 2^32 - 1
 
// str: a default username
pure val default_user: str = "admin"

We will cover integers and booleans in their corresponding dedicated lessons. For now however, it is important to notice that strings are special in Quint as str has no string-specific manipulation operators. Unlike other languages, there is no concatenation, length or indexing for strings. The only allowed operations are comparison for equality and inequality. Additionally, strings can also be stored as elements of a collection or used as map keys. The reason behind this constraint is that Quint is a specification language and not a general-purpose programming one.

A possible workaround for this would be defining a custom character type or using a compound type such as a record (Compound Types are discussed in the following section). However, if you find yourself needing string manipulation, it may be worth stepping back and reconsidering the level of abstraction you want for your specification.

Compound Types

Quint has six core compound types: records, sets, maps, lists, tuples and operators.

Observe that parameters T, T_1 and T_n are type parameters, they can be instantiated by any valid Quint type, including other compound types. This means that a type in Quint can be arbitrarily complex, due to the composition of nested types.

Instantiating these data structures looks like this:

// Set: an unordered collection of unique strings representing currencies
pure val currencies: Set[str] = Set("USD", "EUR", "GBP")
 
// List: an ordered sequence of records representing messages in a log
pure val log: List[{timestamp: int, message: str}] = List({timestamp: 0, message: "init"})
 
// Map: a binding from user identifiers to their balance
pure val balances: str -> int = Map("alice" -> 100, "bob" -> 50)
 
// Tuple: a user identifier paired with their balance 
pure val pair: (str, int) = ("alice", 100)
 
// Record: a user account with an owner and a balance
pure val account: {owner: str, balance: int} = {owner: "alice", balance: 100}
 
// Operators cannot be assigned to values but they can be passed as arguments to other operators.
// isValid is an operator that takes the operator pred as argument 
pure def isValid(pred: (int) => bool, value: int): str = if (pred(value)) "valid" else "invalid"

Similarly to other functional languages, Quint allows for passing operators as arguments which in itself can be a very powerful feature. Let’s try it in the REPL with the example we provided above. Start a REPL session in the terminal with the quint repl command and define the isValid operator:

pure def isValid(pred: (int) => bool, value: int): str = if (pred(value)) "valid" else "invalid"

Now define a suitable predicate. For example:

pure def OK(x:int): bool = x == 5

This allows us to check for the validity of integers. Try these examples on the terminal and see what gets printed:

isValid(OK, 4)

isValid(OK, 5)

Each of the above types, with their appropriate use-cases and built-in operators will be covered in-depth in their corresponding dedicated lessons.

Type Aliases

A type alias gives an alternative name to an existing type. It is a very useful tool for making specifications more declarative and readable. To define one, use the type keyword followed by a capitalised name:

type Temperature = int

The behaviour of Temperature values has not changed: they are still integers only that now is clearer for the reader that they are dealing with numbers that are representing temperatures and are expected to behave as such. This way type aliases actually document the intent of the data structures they represent.

Type aliases can also be useful when refactoring code: if Temperature needs to change from int to a record type, you can update one line and fix the type errors the checker finds, which may be better than hunting for all int annotations that just happened to mean “Temperature”. This is an example where a statically typed language helps eliminate certain bugs very early. In an untyped language, a missed occurrence could lead to a hidden bug that only surfaces much later.

Another important use for type aliases is the avoidance of repetition. Imagine we are dealing with a very complicated data structure such as a message. By defining a type alias we can avoid rewriting the long type over and over again, which is tedious and error-prone:

type Address = str
 
type Message = {
    sender: Address,
    receiver: Address,
    kind: str,                     
    subject: str,
    body: str,                        
    timestamp: int,
  }

Notice how Message uses Address (itself an alias). Aliases compose: each layer adds clarity without repetition.

Polymorphism

Sometimes we want to define operators that work for values of any type. For example, ideally we would want S.size() to work on any set S regardless of the type of its elements. Without polymorphism we would need to implement one version of size() for each of the infinite element types (such as sizeInt(), sizeStr(), and so on). By leveraging Quint’s polymorphic types, we can write a single operator that works for all of them. Before diving into how to write these polymorphic definitions we must introduce the concept of type variables.

Type Variables

Type variables are identifiers that stand for any concrete type. They must start with a lowercase letter. By convention, lowercase short names like a, b, t, ok, err are used. The type checker infers the concrete type at each call site. Notice you have already seen this: the compound types we have seen earlier in this lesson are already parametrized type variables:

• List[a]: a list of elements of any type a
• a -> b: a map from any key type a to any value type b. Notice that choosing different variable names in this case means something: a and b may or may not be of the same type. On the contrary, a -> a can only be a map where keys and values are of the same data type.
• Set[a]: a set of elements of any type a

We can try this on the REPL. Start a session on a terminal with the quint repl command and input the following definition:

pure def isEmpty(s: Set[a]): bool = s.size() == 0

In this case, the type variable is a. We can test sets of different types to see if they work:

isEmpty(Set(1, 2, 3))

The type checker sees Set[int], infers a = int.

isEmpty(Set("x", "y"))

The checker sees Set[str], infers a = str.

Sum Types

Unlike TLA+, Quint supports Sum types  (also known as variants or tagged unions). Sum types are a way of defining a value that can be one of several distinct variants, each of them possibly carrying additional data.

We can define a sum type like we did with type aliases:

type Result =
  | Ok
  | Err

As we do not want correct results to mix with executions ending in an error, we define the type Result that can be either an Ok value or an Err value. The | separates variants. The first | is optional, we added it in the example for clarity but the same structure could be defined in one line as type Result = Ok | Err. Each of the | separated variants is a type constructor that can optionally carry a payload.

The definition can be extended by adding a payload to the variants, and take full advantage of Quint’s sum types:

type Result =
  | Ok
  | Err(str)

Now the program can either return Ok if it executed correctly, or an Err(str) value carrying an informative error message.

Moreover, sum types can take type variables which is a very useful feature as it makes them reusable across types.

type Result[ok,err] =
    | Ok(ok)
    | Err(err)

The canonical example of this is the Option sum type, defined in Quint’s Basic Spells :

type Option[a] = Some(a) | None

Pattern Matching

Expressions of a sum type can be eliminated using a case analysis via a match statement. This is also very useful for extracting the payload of the variant value.

For an interactive example, let’s consider an excerpt of the TicTacToe  spec from our Examples :

module tictactoe {
  type Player = X | O
  type Square = Occupied(Player) | Empty
 
  var board: int -> (int -> Square)
 
  def square(coordinate: (int, int)): Square =
    board.get(coordinate._1).get(coordinate._2)
 
  def hasPlayer(coordinate: (int, int), player: Player): bool = 
    match square(coordinate) {
      | _   => false
    }
 
  def isEmpty(coordinate) = match square(coordinate) {
    | Empty  => true
    | _      => false
  }
}

Notice that in the hasPlayer operator, we have to destructure the sum type in order to know if the Square is empty or not and, furthermore, we need this to be able to compare the payload of an occupied square with the player we are interested in.

For the isEmpty operator, we use the _ syntax. This is very useful to enforce exhaustiveness (in a match expression all variants of the sum type must be covered) and to discard uninteresting cases. In this particular case we are discarding the payload of the occupied square, as we do not need it.

If you are interested in reading more about polymorphic sum types, this spec  is a good starting point.

Uninterpreted Types

Defining a type without any constructors for values of that type introduces an uninterpreted type to our specification:

type MY_TYPE

Uninterpreted types, as other types in quint, must start with a capital letter. These identifiers are abstract, opaque type names used for specification-level modeling. The typical use case is in specifications where you want to reason conceptually without worrying about the internal, low-level structures of your abstractions.

For example if you know that there is a collection of values whose only important property is that each value is considered unique, modeling them as str just to be able to model them in Quint would be taking an unnecessary commitment. The general correctness of your system may have nothing to do with your components being (or not) strings, integers, or anything else. Consider a distributed systems spec were you might write:

  type PROCESS                          // abstract: we do not care what a process "is"
  const Procs: Set[PROCESS]             // assume some set of processes exists
  var leader: PROCESS                   // one of them is the leader
  var mailbox: PROCESS -> Set[Message]  // each process has a mailbox

An important distinction is that uninterpreted types are truly abstract: the type checker will not let you mix them with concrete types. They are useful for abstract reasoning, but not for running or simulating directly.

Summing it up

This lesson covered the full landscape of Quint’s type system. Most of the types introduced here have a dedicated lesson that goes deeper into its operators and use cases. Type aliases, polymorphism, and sum types will also reappear constantly as they are essential tools for writing clear, maintainable specifications.