Variants
Variants (also called tagged unions or sum types) are useful, when you want to combine values of different shapes in a single set or a sequence.
Idiomatic tagged unions in untyped TLA+. In untyped TLA+, one can construct sets, which contain records with different fields, where one filed is typically used as a disambiguation tag. For instance, we could create a set that contains two records of different shapes:
ApplesAndOranges == {
[ tag |-> "Apple", color |-> "red" ],
[ tag |-> "Orange", seedless |-> TRUE ]
}
We can dynamically reason about the elements of ApplesAndOranges based on their tag:
\E e \in ApplesAndOranges:
/\ e.tag = "Apple"
/\ e.color /= "green"
This idiom is quite common in untyped TLA+. Tagged unions in Paxos is probably the most illuminating example of this idiom. Unfortunately, it is way too easy to make a typo in the tag name, since it is a string, or simply access a field, which records marked with the given tag do not have. For example:
\E e \in ApplesAndOranges:
/\ e.tag = "Apple"
/\ e.seedless
Variants module. Apalache formalizes the above idiom in the module Variants.tla. Apalache's type checker alerts users with a type error when they access a wrong value. Additionally, the default implementation raises an error in TLC when a variant is used incorrectly.
Immutability. All variants are immutable.
Construction. An instance of a variant can be constructed via the operator
Variant:
Variant("Apple", "red")
If we just construct a variant like in the example above, it will be assigned a parametric variant type:
Apple(Str) | a
In this type, we know that whenever a value is tagged with "Apple" it should be of the string type. However, we know nothing about other options. Most of the time, we want to define variants that are sealed, that is, we know all available options. Suppose we wanted to reason about different kinds of fruit, but wanted to limit our model to only comparing apples and oranges. In Apalache, the type for a value that could be either an apple or an orange, but nothing else, would be as follows:
Apple(Str) | Orange(Bool)
To make it easier to represent the fruits, we can introduce variants together with user-defined constructors for each option::
\* @typeAlias: FRUIT = Apple(Str) | Orange(Bool);
\* @type: Str => FRUIT;
Apple(color) == Variant("Apple", color)
\* @type: Bool => FRUIT;
Orange(seedless) == Variant("Orange", seedless)
Now we can naturally construct apples and orange as follows:
Apple("red")
Orange(TRUE)
Variants can wrap records, for when we want to represent compound data with named fields:
\* @typeAlias: DRINK =
\* Water({ sparkling: Bool })
\* | Beer({ malt: Str, strength: Int });
\*
\* @type: Bool => DRINK;
Water(sparkling) == Variant("Water", [ sparkling |-> sparkling ])
\* @type: (Str, Int) => DRINK;
Beer(malt, strength) == Variant("Beer", [ malt |-> malt, strength |-> strength ])
Once a variant is constructed, it becomes opaque to the type checker, that is,
the type checker only knows that Water(TRUE) and Beer("Dark", 5) are both
of type DRINK. This is exactly what we want, in order to combine these values
in a single set. However, we have lost the ability to access the fields of
these values. To deconstruct values of a variant type, we have to use other
operators, presented below.
Filtering by tag name. Following the idiomatic use of tagged unions in untyped TLA+, we can filter a set of variants:
LET Drinks == { Water(TRUE), Water(FALSE), Beer("Radler", 2) } IN
\E d \in VariantFilter("Beer", Drink):
d.strength < 3
We believe that VariantFilter is the most commonly used way to partition a
set of variants. Note that VariantFilter transforms a set of variants into a
set of values (that correspond to the associated tag name).
Type-safe get. Sometimes, we do have just a value that does not belong to a
set, so we cannot use VariantFilter directly. In this case, we can use
VariantGetOrElse:
LET water == Water(TRUE) IN
VariantGetOrElse("Beer", water,
[ malt |-> "Non-alcoholic", strength |-> 0])).strength
In the above example, we unpack water by using the tag name "Beer". Since
water is actually tagged with "Water", the operator falls back to the
default case and returns the record [ malt |-> "Non-alcoholic", strength |-> 0].
Type-unsafe get. Sometimes, using VariantFilter and VariantGetOrElse
is a nuisance, when we know the exact value type. In this case, we can bypass
the type checker and get the value notwithstanding the tag:
LET drink == ... IN
LET nonFree ==
IF VariantTag(drink) = "Water"
THEN VariantGetUnsafe("Water", drink).sparkling
ELSE VariantGetUnsafe("Beer", drink).strength > 0
IN
...
In general, you should avoid using VariantGetUnsafe, as it is type unsafe.
Consider the following example:
VariantGetUnsafe("Beer", Water(TRUE)).strength
In the above example, we treat water as beer. If you try this example with TLC,
it would complain about the missing field strength, as it computes some form
of types dynamically. If you try this example with Apalache, it would compute
types statically and in the case of VariantGetUnsafe it would simply produce
an arbitrary integer. Most likely, this arbitrary integer would propagate into
an invariant violation and will lead to a spurious counterexample.
Operators
Variant constructor
Notation: Variant(tagName, associatedValue)
LaTeX notation: same
Arguments: Two arguments: the tag name (a string literal) and a value (a TLA+ expression).
Apalache type: (Str, a) => tagName(a) | b , for some types a and b.
Note that tagName is an identifier in this notation. In this type, b is a
type variable that captures other options in the variant type.
Effect: The variant constructor returns a new value of the variant type.
Determinism: Deterministic.
Errors: No errors.
Example in TLA+:
\* @typeAlias: DRINK =
\* Water({ sparkling: Bool })
\* | Beer({ malt: Str, strength: Int });
\*
\* @type: Bool => DRINK;
Water(sparkling) == Variant("Water", [ sparkling |-> sparkling ])
\* @type: (Str, Int) => DRINK;
Beer(malt, strength) == Variant("Beer", [ malt |-> malt, strength |-> strength ])
Variant tag
Notation: VariantTag(variant)
LaTeX notation: same
Arguments: One argument: a variant constructed via Variant.
Apalache type: (tagName(a) | b) => Str, for some types a and b. Note
that tagName is an identifier in this notation. In this type, b is a type
variable that captures other options in the variant type.
Effect: This operator simply returns the tag attached to the variant.
Determinism: Deterministic.
Errors: No errors.
Example in TLA+:
VariantTag(Variant("Water", [ sparkling |-> sparkling ])) = "Water"
Variant filter
Notation: VariantFilter(tagName, set)
LaTeX notation: same
Arguments: Two arguments: the tag name (a string literal) and a set of variants (a TLA+ expression).
Apalache type: (Str, Set(tagName(a) | b)) => Set(a), for some types a
and b. Note that tagName is an identifier in this notation. In this type,
b is a type variable that captures other options in the variant type.
Effect: The variant filter keeps the set elements that are tagged with
tagName. It removes the tags from these elements and produces the set of
values that were packed with Variant.
Determinism: Deterministic.
Errors: No errors.
Example in TLA+:
\* @typeAlias: DRINK =
\* Water({ sparkling: Bool })
\* | Beer({ malt: Str, strength: Int });
\*
\* @type: Bool => DRINK;
Water(sparkling) == Variant("Water", [ sparkling |-> sparkling ])
\* @type: (Str, Int) => DRINK;
Beer(malt, strength) == Variant("Beer", [ malt |-> malt, strength |-> strength ])
LET Drinks == { Water(TRUE), Water(FALSE), Beer("Radler", 2) } IN
\E d \in VariantFilter("Beer", Drinks):
d.strength < 3
Unpacking a variant safely
Notation: VariantGetOrElse(tagName, variant, defaultValue)
LaTeX notation: same
Arguments: Three arguments: the tag name (a string literal), a variant
constructed via Variant, a default value compatible with the value carried by
the variant.
Apalache type: (Str, tagName(a) | b, a) => a, for some types a and b.
Note that tagName is an identifier in this notation. In this type, b is a
type variable that captures other options in the variant type.
Effect: The operator VariantGetOrElse returns the value that was wrapped
via the Variant constructor, if the variant is tagged with tagName.
Otherwise, the operator returns defaultValue.
Determinism: Deterministic.
Errors: No errors.
Example in TLA+:
\* @typeAlias: DRINK =
\* Water({ sparkling: Bool })
\* | Beer({ malt: Str, strength: Int });
\*
\* @type: Bool => DRINK;
Water(sparkling) == Variant("Water", [ sparkling |-> sparkling ])
\* @type: (Str, Int) => DRINK;
Beer(malt, strength) == Variant("Beer", [ malt |-> malt, strength |-> strength ])
LET water == Water(TRUE) IN
VariantGetOrElse("Beer", water,
[ malt |-> "Non-alcoholic", strength |-> 0])).strength
Unpacking a variant unsafely
Notation: VariantGetUnsafe(tagName, variant)
LaTeX notation: same
Arguments: Two arguments: the tag name (a string literal) and a variant
constructed via Variant.
Apalache type: (Str, tagName(a) | b) => a, for some types a and b.
Note that tagName is an identifier in this notation. In this type, b is a
type variable that captures other options in the variant type.
Effect: The operator VariantGetUnsafe unconditionally returns some value
that is compatible with the type of values tagged with tagName. If variant
is tagged with tagName, the returned value is the value that was wrapped via
the Variant constructor. Otherwise, it is some arbitrary value of a proper type.
As such, this operator does not guarantee that the retrieved value
is always constructed via Variant, unless the operator is used with the right tag.
Determinism: Deterministic.
Errors: No errors.
Example in TLA+:
\* @typeAlias: DRINK =
\* Water({ sparkling: Bool })
\* | Beer({ malt: Str, strength: Int });
\*
\* @type: Bool => DRINK;
Water(sparkling) == Variant("Water", [ sparkling |-> sparkling ])
\* @type: (Str, Int) => DRINK;
Beer(malt, strength) == Variant("Beer", [ malt |-> malt, strength |-> strength ])
LET drink == Beer("Dunkles", 4) IN
LET nonFree ==
IF VariantTag(drink) = "Water"
THEN VariantGetUnsafe("Water", drink).sparkling
ELSE VariantGetUnsafe("Beer", drink).strength > 0
IN
...