Update HOWTO on types

.unreleased/documentation/1940.md

@@ -0,0 +1 @@
+Update HOWTO on types with new records and variants, see #1940

docs/src/HOWTOs/howto-write-type-annotations.md

@@ -1,8 +1,19 @@
 # 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.
-Note that the example specification uses recursive operators, which were removed in version 0.23.1.*
+**Revision:** July 7, 2022
+
+**Important updates:**
+
+ - Version 0.25.9: This HOWTO introduces new syntax for record types and
+   variants, which is currently under testing. This syntax is activated via the
+   option `--features=rows`. See [Type System 1.2](../adr/002adr-types.md#ts12).
+
+ - Version 0.23.1: The example specification uses recursive operators, which
+   were removed in version 0.23.1.
+
+ - Version 0.15.0: This HOWTO discusses how to write type annotations for the type checker
+   [Snowcat][], which is used in Apalache since version 0.15.0 (introduced in
+   2021).
 
 This HOWTO gives you concrete steps to extend TLA+ specifications with type
 annotations. You can find the detailed syntax of type annotations in
@@ -17,7 +28,7 @@ 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
+## Recipe 1: Annotating variables
 
 Consider the example [HourClock.tla][] from [Specifying Systems][]:
 
@@ -92,27 +103,39 @@ 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:
 
 ```tla
-CONSTANT
-    \* @type: Set(DATUM);
-    Data
-VARIABLE
-    \* @type: [val: DATUM, rdy: Int, ack: Int];
-    chan 
+{{#include ../../../test/tla/ChannelTyped.tla:declarations}}
 ```
 
 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.
 
+Have a look at the type of `chan`:
+
+```
+\* @type: { val: DATUM, rdy: Int, ack: Int };
+```
+
+The type of `chan` is a record that has three fields: field `val` of type
+`DATUM`, field `rdy` of type `Int`, field `ack` of type `Int`. The record type syntax is similar to dictionary syntax from programming languages (e.g. Python). We made it different
+from TLA+'s syntax for records `[ val |-> v, rdy |-> r, ack |-> a ]`
+and record sets `[ val: V, rdy: R, ack: A ]`, to avoid confusion between
+types and values.
+
 Run the type checker again. You should see the following message:
 
 ```
+$ apalache-mc typecheck --features=rows ChannelTyped.tla
+...
 > Running Snowcat .::.
 > Your types are purrfect!
 > All expressions are typed 
 ```
 
+Note that we had to pass the option `--features=rows`, as we are using the
+experimental syntax for records.
+
 ## Recipe 3: Annotating operators
 
 Check the example [CarTalkPuzzle.tla][] from the repository of TLA+
@@ -178,38 +201,30 @@ This time the type checker can find the types of all expressions:
 ...
 ```
 
+## Recipe 4: Using variants in heterogenous sets
 
-## Recipe 4: Annotating records
-
-Check the example [TwoPhase.tla][] from the repository of TLA+ examples (you will also need [TCommit.tla][], which
-is imported by TwoPhase.tla).
-This example has 176 lines of code, so we do not inline it here.
+Check the example [TwoPhase.tla][] from the repository of TLA+ examples (you
+will also need [TCommit.tla][], which is imported by TwoPhase.tla). 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:
 
 ```tla
-CONSTANT
-        \* @type: Set(RM);
-        RM
+{{#include ../../../test/tla/TwoPhaseTyped.tla:constants}}
 ```
 
 By looking at the spec, it is easy to guess the types of the variables
 `rmState`, `tmState`, and `tmPrepared`:
 
 ```tla
-VARIABLES
-  \* @type: RM -> Str;
-  rmState,
-  \* @type: Str;
-  tmState,
-  \* @type: Set(RM);
-  tmPrepared,
+{{#include ../../../test/tla/TwoPhaseTyped.tla:vars1}}
 ```
 
-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`:
+The type of the variable `msgs` is less obvious. We can check the original
+(untyped) definitions of `TPTypeOK` and `Message` to get an idea about the
+type of `msgs`:
 
 ```tla
 Message ==
@@ -222,20 +237,72 @@ 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:
+From these (untyped) definitions, you can see that `msgs` is a set that
+contains records of two types: `{ type: Str }` and `{ type: Str, rm: RM }`.
+This seems to be problematic, as we have to mix in two records types in a
+single set, which requires us to specify its only type.
+
+To this end, we have to use the [Variants module][], which is distributed with
+Apalache. For reference, check the [Chapter on variants][]. First, we declare a
+type alias for the type of messages in a separate file called
+`TwoPhaseTyped_typedefs.tla`:
 
 ```tla
-  \* @type: Set([type: Str, rm: RM]);
-  msgs           
+{{#include ../../../test/tla/TwoPhaseTyped_typedefs.tla}}
 ```
 
-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][].
+Usually, we place type aliases in a separate file for when we have
+to use the same type alias in different specifications, e.g., the specification
+and its instance for model checking.
 
+With the type alias `MESSAGE`, we specify that a message is a variant type,
+that is, it can represent three kinds of different values:
+
+ - A value tagged with `Commit`. Since we do not require the variant to carry
+   any value here, we simply declare that the value has the uninterpreted type
+   `NIL`. This is simply a convention, we could use any type in this case.
+
+ - A value tagged with `Abort`. Similar to `Commit`, we are using the `NIL`
+   type.
+
+ - A value tagged with `Prepared`. In this case, the value is of importance.
+   We are using the value `RM`, that is, the (uninterpreted) type of a resource
+   manager.
+
+Once we have specified the variant type, we introduce three constructors,
+one per variant option:
+
+```tla
+{{#include ../../../test/tla/TwoPhaseTyped.tla:constructors}}
+```
+
+Since the values carried by the `Commit` and `Abort` messages are not
+important, we use the uninterpeted value `"0_OF_NIL"`. This is merely a
+convention. We could use any value of type `NIL`. Importantly, the operators
+`MkAbort`, `MkCommit`, and `MkPrepared` all produce values of type `MESSAGE`,
+which makes it possible to add them to a single set of messages.
+
+Now it should be clear how to specify the type of the variable `msgs`:
+
+```tla
+{{#include ../../../test/tla/TwoPhaseTyped.tla:vars2}}
+```
+
+We run the type checker once again (pay attention to the option
+`--features=rows`, required for variants):
+
+```sh
+$ apalache-mc typecheck --features=rows TwoPhaseTyped.tla
+...
+ > All expressions are typed
+Type checker [OK]
+```
+
+As you can see, variants require quite a bit of boilerplate. If you can simply
+introduce a set of records of the same type, this is usually a simpler
+solution. For instance, we could partition `msgs` into three subsets: the
+subset of `Commit` messages, the subset of `Abort` messages, and the subset of
+`Prepared` messages. See the discussion in [Idiom 3][].
 
 <a id="funAsSeq"></a>
 ## Recipe 5: functions as sequences
@@ -245,29 +312,22 @@ Check the example [Queens.tla][] from the repository of TLA+ examples.  It has
 sections, we annotate constants and variables:
 
 ```tla
-CONSTANT 
-         \* @type: Int;
-         N
-...         
-VARIABLES
-    \* @type: Set(Seq(Int));
-    todo,
-    \* @type: Set(Seq(Int));
-    sols
+{{#include ../../../test/tla/QueensTyped.tla:constants}}
+...
+{{#include ../../../test/tla/QueensTyped.tla:variables}}
 ```
 
 After having inspected the type errors reported by Snowcat, we annotate the
 operators `Attacks`, `IsSolution`, and `vars` as follows:
 
 ```tla
-\* @type: (Seq(Int), Int, Int) => Bool;
-Attacks(queens,i,j) == ...
+{{#include ../../../test/tla/QueensTyped.tla:Attacks}}
+  ...
 
-\* @type: Seq(Int) => Bool;
-IsSolution(queens) == ...
+{{#include ../../../test/tla/QueensTyped.tla:IsSolution}}
+  ...
 
-\* @type: <<Set(Seq(Int)), Set(Seq(Int))>>;
-vars == <<todo,sols>>
+{{#include ../../../test/tla/QueensTyped.tla:vars}}
 ```
 
 Now we run the type checker and receive the following type error:
@@ -285,13 +345,13 @@ 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
+This looks interesting: `IsSolution` expects a sequence, whereas
+`Solutions` produces a set of functions. This is obviously not a
+problem in untyped TLA+. In fact, it is a well-known idiom: Construct a
+function by using the function set operator, 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:
 
 ```tla
@@ -458,3 +518,7 @@ This may change later, when the tlaplus [Issue 578][] is resolved.
 [Issue 578]: https://github.com/tlaplus/tlaplus/issues/578
 [Issue 718]: https://github.com/informalsystems/apalache/issues/718
 [MissionariesAndCannibals.tla]: https://github.com/tlaplus/Examples/blob/master/specifications/MissionariesAndCannibals/MissionariesAndCannibals.tla
+[Variants module]: https://github.com/informalsystems/apalache/blob/unstable/src/tla/Variants.tla
+[Chapter on variants]: ../lang/variants.md
+[Idiom 3]: ../idiomatic/003record-sets.md
+[LamportMutex.tla]: https://github.com/tlaplus/Examples/blob/master/specifications/lamport_mutex/LamportMutex.tla

docs/src/SUMMARY.md

@@ -12,6 +12,12 @@
 - [Symbolic Model Checking](./tutorials/symbmc.md)
 - [Specifying temporal properties and understanding counterexamples](./tutorials/temporal-properties.md)
 
+# HOWTOs
+
+- [Overview](HOWTOs/index.md)
+- [How to write type annotations](./HOWTOs/howto-write-type-annotations.md)
+- [How to use uninterpreted types](./HOWTOs/uninterpretedTypes.md)
+
 # Apalache User Manual
 
 - [Getting Started](./apalache/index.md)
@@ -45,12 +51,6 @@
 - [KerA: kernel logic of actions](./apalache/kera.md)
 
 
-# HOWTOs
-
-- [Overview](HOWTOs/index.md)
-- [How to write type annotations](./HOWTOs/howto-write-type-annotations.md)
-- [How to use uninterpreted types](./HOWTOs/uninterpretedTypes.md)
-
 # TLA+ Language Manual for Engineers
 
 - [Introduction](./lang/index.md)

test/tla/ChannelTyped.tla

@@ -2,12 +2,14 @@
 \* 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
+\* ANCHOR: declarations
 CONSTANT
     \* @type: Set(DATUM);
     Data
 VARIABLE
-    \* @type: [val: DATUM, rdy: Int, ack: Int];
+    \* @type: { val: DATUM, rdy: Int, ack: Int };
     chan 
+\* ANCHOR_END: declarations
 
 TypeInvariant  ==  chan \in [val : Data,  rdy : {0, 1},  ack : {0, 1}]
 -----------------------------------------------------------------------

test/tla/QueensTyped.tla

@@ -19,23 +19,29 @@ EXTENDS Naturals, Sequences, Apalache
 (* of length \leq N.                                                       *)
 (***************************************************************************)
 
+\* ANCHOR: constants
 CONSTANT
     \* @type: Int;
     N              \** number of queens and size of the board
+\* ANCHOR_END: constants
 ASSUME N \in Nat \ {0}
 
 (* The following predicate determines if queens i and j attack each other
    in a placement of queens (represented by a sequence as above). *)
+\* ANCHOR: Attacks
 \* @type: (Seq(Int), Int, Int) => Bool;
 Attacks(queens,i,j) ==
+\* ANCHOR_END: Attacks
   \/ queens[i] = queens[j]                 \** same column
   \/ queens[i] - queens[j] = i - j         \** first diagonal
   \/ queens[j] - queens[i] = i - j         \** second diagonal
 
 (* A placement represents a (partial) solution if no two different queens
    attack each other in it. *)
+\* ANCHOR: IsSolution
 \* @type: Seq(Int) => Bool;
 IsSolution(queens) ==
+\* ANCHOR_END: IsSolution
   \A i \in 1 .. Len(queens)-1 : \A j \in i+1 .. Len(queens) : 
        ~ Attacks(queens,i,j) 
 
@@ -61,11 +67,13 @@ Solutions ==
 (* to the set todo.                                                        *)
 (***************************************************************************)
 
+\* ANCHOR: variables
 VARIABLES
     \* @type: Set(Seq(Int));
     todo,
     \* @type: Set(Seq(Int));
     sols
+\* ANCHOR_END: variables
 
 Init == /\ todo = { << >> }   \** << >> is a partial (but not full) solution
         /\ sols = {}          \** no full solution found so far
@@ -84,8 +92,10 @@ PlaceQueen == \E queens \in todo :
       ELSE /\ todo' = (todo \ {queens}) \union exts
            /\ sols' = sols
 
+\* ANCHOR: vars
 \* @type: <<Set(Seq(Int)), Set(Seq(Int))>>;
 vars == <<todo,sols>>
+\* ANCHOR_END: vars
 Spec == Init /\ [][PlaceQueen]_vars /\ WF_vars(PlaceQueen)
 
 TypeInvariant ==