How to write type annotations

Warning: This HOWTO discusses how to write type annotations for the new type checker Snowcat, which is used in Apalache since version 0.15.0.

This HOWTO gives you concrete steps to extend TLA+ specifications with type annotations. You can find the detailed syntax of type annotations in ADR002. The first rule of writing type annotations:

Do not to write any annotations at all, until the type checker Snowcat is asking you to write a type annotation.

Of course, there must be an exception to this rule. You have to write type annotations for CONSTANTS and VARIABLES. This is because Snowcat infers types of declarations in isolation instead of analyzing the whole specification. The good news is that the type checker finds the types of many operators automatically.

Recipe 1: Recipe variables

Consider the example HourClock.tla from Specifying Systems:

---------------------- MODULE HourClock ----------------------
\* This is a local copy of the example from Specifying Systems:
\* https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/RealTime/HourClock.tla
EXTENDS Naturals
VARIABLE
    \* @type: Int;
    hr

HCini  ==  hr \in (1 .. 12)
HCnxt  ==  hr' = IF hr # 12 THEN hr + 1 ELSE 1
HC  ==  HCini /\ [][HCnxt]_hr

TypeOK == hr \in (1 .. 12)

Without thinking much about the types, run the type checker:

$ apalache typecheck HourClock.tla

The type checker complains about not knowing the type of the variable hr:

...
[HourClock.tla:6:12-6:13]: Undefined name hr. Introduce a type annotation.
...

Annotate the type of variable hr as below. Note carefully that the type annotation should be between the keyword VARIABLE and the variable name. This is because variable declarations may declare several variables at once. In this case, you have to write one type annotation per name.

VARIABLE
  \* @type: Int;
  hr

Run the type checker again. You should see the following message:

 > Your types are great!

Recipe 2: Annotating constants

Consider the example Channel.tla from Specifying Systems:


-------------------------- MODULE Channel -----------------------------
\* This is a typed version of the example from Specifying Systems:
\* https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/FIFO/Channel.tla
EXTENDS Naturals
CONSTANT Data
VARIABLE chan 

TypeInvariant  ==  chan \in [val : Data,  rdy : {0, 1},  ack : {0, 1}]
-----------------------------------------------------------------------
Init  ==  /\ TypeInvariant
          /\ chan.ack = chan.rdy 

Send(d) ==  /\ chan.rdy = chan.ack
            /\ chan' = [chan EXCEPT !.val = d, !.rdy = 1 - @]

Rcv     ==  /\ chan.rdy # chan.ack
            /\ chan' = [chan EXCEPT !.ack = 1 - @]

Next  ==  (\E d \in Data : Send(d)) \/ Rcv

Spec  ==  Init /\ [][Next]_chan
-----------------------------------------------------------------------
THEOREM Spec => []TypeInvariant
=======================================================================

Run the type checker:

$ apalache typecheck Channel.tla

The type checker does not know the type of the variable chan:

[Channel.tla:6:20-6:23]: Undefined name chan. Introduce a type annotation.

According to TypeInvariant, the variable chan is a record that has three fields: val, rdy, and ack. The field val ranges over a set Data, which is actually defined as CONSTANT. In principle, we can annotate the constant Data with a set of any type, e.g., Set(Int) or Set(BOOLEAN). Since the specification is not using any operators over Data except equality, we can use an uninterpreted type as a type for set elements, e.g., we can define Data to have the type Set(DATUM). Uninterpreted types are always written in CAPITALS. Now we can annotate Data and chan as follows:

CONSTANT
    \* @type: Set(DATUM);
    Data
VARIABLE
    \* @type: [val: DATUM, rdy: Int, ack: Int];
    chan 

Note carefully that the type annotation should be between the keyword CONSTANT and the constant name. This is because constant declarations may declare several constants at once. In this case, you have to write one type annotation per name.

Run the type checker again. You should see the following message:

 > Your types are great!

Recipe 3: Annotating operators

Check the example CarTalkPuzzle.tla from the repository of TLA+ examples. This example has 160 lines of code, so we do not inline it here. By running the type checker as in previous sections, you should figure out that the constants N and P should be annotated with the type Int. Annotate N and P with Int and run the type checker:

$ apalache typecheck CarTalkPuzzle.tla

Now you should see the following error:

[CarTalkPuzzle.tla:57:9-57:12]: Need annotation. Arguments match
2 operator signatures: (((a56 -> a57), a56) => a57) and ((Seq(a56), Int) => a56)

Although the error message may look confusing, the reason is simple: The type checker cannot figure out, whether the operator Sum expects a sequence or a function of integers as its first parameter. By looking carefully at the definition of Sum, we can see that it expects: (1) a function from integers to integers as its first parameter, (2) a set of integers as its second parameter, and (3) an integer as a result. Hence, we annotate Sum as follows:

RECURSIVE Sum(_,_)
\* type: (Int -> Int, Set(Int)) => Int;
Sum(f,S) ==
    ...

Note that the annotation has to be written between RECURSIVE Sum(_, _) and the definition of Sum. This might change later, see Issue 578 at tlaplus.

After providing the type checker with the annotation for Sum, we get one more type error:

[CarTalkPuzzle.tla:172:23-172:26]: Need annotation. Arguments match
2 operator signatures: (((p -> q), p) => q) and ((Seq(p), Int) => p)

This time the type checker cannot choose between two options for the second parameter of Image: It could be a function, or a sequence. We help the type checker by writing that the second parameter should be a function of integers to integers, that is, Int -> Int:

      \* @type: (Set(Int), Int -> Int) => Set(Int);
      Image(S, B) == {B[x] : x \in S}

This time the type checker can find the types of all expressions:

 > Your types are great!

Recipe 4: Annotating records

Check the example TwoPhase.tla from the repository of TLA+ examples. This example has 176 lines of code, so we do not inline it here.

As you probably expected, the type checker complains about not knowing the types of constants and variables. As for constant RM, we opt for using an uninterpreted type that we call RM. That is:

CONSTANT
        \* @type: Set(RM);
        RM

By looking at the spec, it is easy to guess the types of the variables rmState, tmState, and tmPrepared:

VARIABLES
  \* @type: RM -> Str;
  rmState,
  \* @type: Str;
  tmState,
  \* @type: Set(RM);
  tmPrepared

The type of the variable msgs is less obvious. We can check the definitions of TPTypeOK and Message to get the idea about the type of msgs:

Message ==
  ({[type |-> t, rm |-> r]: t \in {"Prepared"}, r \in RM }
   \union
   {[type |-> t] : t \in {"Commit", "Abort"}})

TPTypeOK ==
  ...
  /\ msgs \in SUBSET Message

From these definitions, you can see that msgs is a set that contains records of two types: [type: Str] and [type: Str, rm: RM]. When you have a set of heterogeneous records, you have to choose the type of a super-record that contains the fields of all records that could be put in the set. That is:

  \* @type: Set([type: Str, rm: RM]);
  msgs           

A downside of this approach is that Snowcat will not help you in finding an incorrect field access. We probably will introduce more precise types for records later. See Issue 401.

Recipe 5: functions as sequences

Check the example Queens.tla from the repository of TLA+ examples. It has 85 lines of code, so we do not include it here. Similar to the previous sections, we annotate constants and variables:

CONSTANT 
         \* @type: Int;
         N
...         
VARIABLES
    \* @type: Set(Seq(Int));
    todo,
    \* @type: Set(Seq(Int));
    sols

After having inspected the type errors reported by Snowcat, we annotate the operators Attacks, IsSolution, and vars as follows:

\* @type: (Seq(Int), Int, Int) => Bool;
Attacks(queens,i,j) == ...

\* @type: Seq(Int) => Bool;
IsSolution(queens) == ...

\* @type: <<Set(Seq(Int)), Set(Seq(Int))>>;
vars == <<todo,sols>>

Now we run the type checker and receive the following type error:

[Queens.tla:47:21-47:38]: Mismatch in argument types.
Expected: ((Seq(Int)) => Bool)

Let's have a closer look at the problematic operator definition of Solutions:

Solutions ==
    { queens \in [1..N -> 1..N]: IsSolution(queens) }

This looks funny: IsSolution is expecting a sequence, whereas Solutions is clearly producing a set of functions. Of course, it is not a problem in the untyped TLA+. In fact, it is a well-known idiom: Construct a function by using function operators and then apply sequence operators to it. In Apalache we have to explicitly write that a function should be reinterpreted as a sequence. To this end, we have to use the operator FunAsSeq from the module Apalache.tla. Hence, we add Apalache to the EXTENDS clause and apply the operator FunAsSeq as follows:

EXTENDS Naturals, Sequences, Apalache
...
Solutions ==
  LET Queens == { queens \in [1..N -> 1..N] : FunAsSeq(queens, N) } IN
  { FunAsSeq(queens, N): queens \in Queens }

This time the type checker can find the types of all expressions:

 > Your types are great!

Recipe 6: type aliases

Type aliases can be used to provide a concise label for complex types, or to clarify the intended meaning of a simple types in the given context.

Type aliases are declared with the @typeAlias annotation, as follows:

\* @typeAlias: ALIAS = <type>;

For example, suppose we have annotated some constants as follows:

CONSTANTS
    \* @type: Set(PERSON);
    Missionaries,
    \* @type: Set(PERSON);
    Cannibals 

If we continue annotating other declarations in the specification, we will see that the type Set(PERSON) is used frequently. Type aliases let us provide a shortcut.

By convention, we introduce all type aliases by annotating an operator called <PREFIX>TypeAliases, where the <PREFIX> is replaced with a unique prefix to prevent name clashes. In the MissionariesAndCannibals.tla example, we have

\* @typeAlias: PERSONS = Set(PERSON);
MCTypeAliases = TRUE

Having defined the type alias, we can use it in other definitions anywhere else in the file:

CONSTANTS
    \* @type: PERSONS;
    Missionaries,
    \* @type: PERSONS;
    Cannibals 

VARIABLES
    \* @type: Str;
    bank_of_boat,
    \* @type: Str -> PERSONS;
    who_is_on_bank 

Surely, we did not gain much by writing PERSONS instead of Set(PERSON). But if your specification has complex types (e.g., records), aliases may help you in minimizing the burden of specification maintenance. When you add one more field to the record type, it suffices to change the definition of the type alias, instead of changing the record type everywhere.

For more details on the design and usage, see ADR002.

Recipe 7: Multi-line annotations

A type annotation may span over multiple lines. You may use both the (* ... *) syntax as well as the single-line syntax \* .... All three examples below are accepted by the parser:

VARIABLES
   (*
    @type: Int
            => Bool;
    *)           
    f,
    \* @type:
    \*       Int
    \*          => Bool;
    g,
    \* @type("Int
    \*          => Bool
    \*       ")
    h

Note that the parser removes the leading strings " \*" from the annotations, similar to how multi-line strings are treated in modern programming languages.

Recipe 8: Comments in annotations

Sometimes, it helps to document the meaning of type components. Consider the following example from Recipe 5:

\* @type: (Seq(Int), Int, Int) => Bool;
Attacks(queens,i,j)

If you think that an explanation of the arguments would help, you can do that as follows:

(*
  @type:
    (
      // the column of an n-th queen, for n in the sequence domain
      Seq(Int),
      // the index (line number) of the first queen
      Int,
      // the index (line number) of the second queen
      Int
    ) => Bool;
*)
Attacks(queens,i,j)

You don't have to do that, but if you feel that types can also help you in documenting your specification, you have this option.

Known issues

Annotations of LOCAL operators

In contrast to all other cases, a local operator definition does require a type annotation before the keyword LOCAL, not after it. For example:

\* @type: Int => Int;
LOCAL LocalInc(x) == x + 1

This may change later, when the tlaplus Issue 578 is resolved.