Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

update variants.md to new alias syntax #3028

Merged
merged 2 commits into from
Nov 4, 2024
Merged

update variants.md to new alias syntax #3028

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
99e3e4c
update variants.md to new alias syntax
nano-o Oct 31, 2024
bc73f96
Merge branch 'main' into main
coffeeinprogress Nov 4, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 20 additions & 20 deletions docs/src/lang/variants.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,12 +73,12 @@ To make it easier to represent the fruits, we can introduce variants together wi
user-defined constructors for each option::

```tla
\* @typeAlias: FRUIT = Apple(Str) | Orange(Bool);
\* @typeAlias: fruit = Apple(Str) | Orange(Bool);

\* @type: Str => FRUIT;
\* @type: Str => $fruit;
Apple(color) == Variant("Apple", color)

\* @type: Bool => FRUIT;
\* @type: Bool => $fruit;
Orange(seedless) == Variant("Orange", seedless)
```

Expand All @@ -92,20 +92,20 @@ Orange(TRUE)
Variants can wrap records, for when we want to represent compound data with named fields:

```tla
\* @typeAlias: DRINK =
\* @typeAlias: drink =
\* Water({ sparkling: Bool })
\* | Beer({ malt: Str, strength: Int });
\*
\* @type: Bool => DRINK;
\* @type: Bool => $drink;
Water(sparkling) == Variant("Water", [ sparkling |-> sparkling ])

\* @type: (Str, Int) => DRINK;
\* @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
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.
Expand All @@ -115,7 +115,7 @@ untyped TLA+, we can filter a set of variants:

```tla
LET Drinks == { Water(TRUE), Water(FALSE), Beer("Radler", 2) } IN
\E d \in VariantFilter("Beer", Drink):
\E d \in VariantFilter("Beer", Drinks):
d.strength < 3
```

Expand Down Expand Up @@ -195,14 +195,14 @@ type variable that captures other options in the variant type.
**Example in TLA+:**

```tla
\* @typeAlias: DRINK =
\* @typeAlias: drink =
\* Water({ sparkling: Bool })
\* | Beer({ malt: Str, strength: Int });
\*
\* @type: Bool => DRINK;
\* @type: Bool => $drink;
Water(sparkling) == Variant("Water", [ sparkling |-> sparkling ])

\* @type: (Str, Int) => DRINK;
\* @type: (Str, Int) => $drink;
Beer(malt, strength) == Variant("Beer", [ malt |-> malt, strength |-> strength ])
```

Expand Down Expand Up @@ -260,14 +260,14 @@ values that were packed with `Variant`.
**Example in TLA+:**

```tla
\* @typeAlias: DRINK =
\* @typeAlias: drink =
\* Water({ sparkling: Bool })
\* | Beer({ malt: Str, strength: Int });
\*
\* @type: Bool => DRINK;
\* @type: Bool => $drink;
Water(sparkling) == Variant("Water", [ sparkling |-> sparkling ])

\* @type: (Str, Int) => DRINK;
\* @type: (Str, Int) => $drink;
Beer(malt, strength) == Variant("Beer", [ malt |-> malt, strength |-> strength ])

LET Drinks == { Water(TRUE), Water(FALSE), Beer("Radler", 2) } IN
Expand Down Expand Up @@ -303,14 +303,14 @@ Otherwise, the operator returns `defaultValue`.
**Example in TLA+:**

```tla
\* @typeAlias: DRINK =
\* @typeAlias: drink =
\* Water({ sparkling: Bool })
\* | Beer({ malt: Str, strength: Int });
\*
\* @type: Bool => DRINK;
\* @type: Bool => $drink;
Water(sparkling) == Variant("Water", [ sparkling |-> sparkling ])

\* @type: (Str, Int) => DRINK;
\* @type: (Str, Int) => $drink;
Beer(malt, strength) == Variant("Beer", [ malt |-> malt, strength |-> strength ])

LET water == Water(TRUE) IN
Expand Down Expand Up @@ -348,14 +348,14 @@ is always constructed via `Variant`, unless the operator is used with the right
**Example in TLA+:**

```tla
\* @typeAlias: DRINK =
\* @typeAlias: drink =
\* Water({ sparkling: Bool })
\* | Beer({ malt: Str, strength: Int });
\*
\* @type: Bool => DRINK;
\* @type: Bool => $drink;
Water(sparkling) == Variant("Water", [ sparkling |-> sparkling ])

\* @type: (Str, Int) => DRINK;
\* @type: (Str, Int) => $drink;
Beer(malt, strength) == Variant("Beer", [ malt |-> malt, strength |-> strength ])

LET drink == Beer("Dunkles", 4) IN
Expand Down
Loading