Skip to content

Commit

Permalink
deploy: 978f7a5
Browse files Browse the repository at this point in the history
  • Loading branch information
@konnov
konnov committed Nov 4, 2024
1 parent 7d41e01 commit 5d2987b
Show file tree
Hide file tree
Showing 4 changed files with 42 additions and 42 deletions.
40 changes: 20 additions & 20 deletions docs/lang/variants.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -220,39 +220,39 @@ <h1><a class="header" href="#variants" id="variants">Variants</a></h1>
</code></pre>
<p>To make it easier to represent the fruits, we can introduce variants together with
user-defined constructors for each option::</p>
<pre><code class="language-tla">\* @typeAlias: FRUIT = Apple(Str) | Orange(Bool);
<pre><code class="language-tla">\* @typeAlias: fruit = Apple(Str) | Orange(Bool);

\* @type: Str =&gt; FRUIT;
\* @type: Str =&gt; $fruit;
Apple(color) == Variant(&quot;Apple&quot;, color)

\* @type: Bool =&gt; FRUIT;
\* @type: Bool =&gt; $fruit;
Orange(seedless) == Variant(&quot;Orange&quot;, seedless)
</code></pre>
<p>Now we can naturally construct apples and orange as follows:</p>
<pre><code class="language-tla">Apple(&quot;red&quot;)
Orange(TRUE)
</code></pre>
<p>Variants can wrap records, for when we want to represent compound data with named fields:</p>
<pre><code class="language-tla">\* @typeAlias: DRINK =
<pre><code class="language-tla">\* @typeAlias: drink =
\* Water({ sparkling: Bool })
\* | Beer({ malt: Str, strength: Int });
\*
\* @type: Bool =&gt; DRINK;
\* @type: Bool =&gt; $drink;
Water(sparkling) == Variant(&quot;Water&quot;, [ sparkling |-&gt; sparkling ])

\* @type: (Str, Int) =&gt; DRINK;
\* @type: (Str, Int) =&gt; $drink;
Beer(malt, strength) == Variant(&quot;Beer&quot;, [ malt |-&gt; malt, strength |-&gt; strength ])
</code></pre>
<p>Once a variant is constructed, it becomes opaque to the type checker, that is,
the type checker only knows that <code>Water(TRUE)</code> and <code>Beer(&quot;Dark&quot;, 5)</code> are both
of type <code>DRINK</code>. This is exactly what we want, in order to combine these values
of type <code>drink</code>. 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.</p>
<p><strong>Filtering by tag name.</strong> Following the idiomatic use of tagged unions in
untyped TLA+, we can filter a set of variants:</p>
<pre><code class="language-tla">LET Drinks == { Water(TRUE), Water(FALSE), Beer(&quot;Radler&quot;, 2) } IN
\E d \in VariantFilter(&quot;Beer&quot;, Drink):
\E d \in VariantFilter(&quot;Beer&quot;, Drinks):
d.strength &lt; 3
</code></pre>
<p>We believe that <code>VariantFilter</code> is the most commonly used way to partition a
Expand Down Expand Up @@ -305,14 +305,14 @@ <h3><a class="header" href="#variant-constructor" id="variant-constructor">Varia
<p><strong>Determinism:</strong> Deterministic.</p>
<p><strong>Errors:</strong> No errors.</p>
<p><strong>Example in TLA+:</strong></p>
<pre><code class="language-tla">\* @typeAlias: DRINK =
<pre><code class="language-tla">\* @typeAlias: drink =
\* Water({ sparkling: Bool })
\* | Beer({ malt: Str, strength: Int });
\*
\* @type: Bool =&gt; DRINK;
\* @type: Bool =&gt; $drink;
Water(sparkling) == Variant(&quot;Water&quot;, [ sparkling |-&gt; sparkling ])

\* @type: (Str, Int) =&gt; DRINK;
\* @type: (Str, Int) =&gt; $drink;
Beer(malt, strength) == Variant(&quot;Beer&quot;, [ malt |-&gt; malt, strength |-&gt; strength ])
</code></pre>
<hr />
Expand Down Expand Up @@ -346,14 +346,14 @@ <h3><a class="header" href="#variant-filter" id="variant-filter">Variant filter<
<p><strong>Determinism:</strong> Deterministic.</p>
<p><strong>Errors:</strong> No errors.</p>
<p><strong>Example in TLA+:</strong></p>
<pre><code class="language-tla">\* @typeAlias: DRINK =
<pre><code class="language-tla">\* @typeAlias: drink =
\* Water({ sparkling: Bool })
\* | Beer({ malt: Str, strength: Int });
\*
\* @type: Bool =&gt; DRINK;
\* @type: Bool =&gt; $drink;
Water(sparkling) == Variant(&quot;Water&quot;, [ sparkling |-&gt; sparkling ])

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

LET Drinks == { Water(TRUE), Water(FALSE), Beer(&quot;Radler&quot;, 2) } IN
Expand All @@ -377,14 +377,14 @@ <h3><a class="header" href="#unpacking-a-variant-safely" id="unpacking-a-variant
<p><strong>Determinism:</strong> Deterministic.</p>
<p><strong>Errors:</strong> No errors.</p>
<p><strong>Example in TLA+:</strong></p>
<pre><code class="language-tla">\* @typeAlias: DRINK =
<pre><code class="language-tla">\* @typeAlias: drink =
\* Water({ sparkling: Bool })
\* | Beer({ malt: Str, strength: Int });
\*
\* @type: Bool =&gt; DRINK;
\* @type: Bool =&gt; $drink;
Water(sparkling) == Variant(&quot;Water&quot;, [ sparkling |-&gt; sparkling ])

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

LET water == Water(TRUE) IN
Expand All @@ -410,14 +410,14 @@ <h3><a class="header" href="#unpacking-a-variant-unsafely" id="unpacking-a-varia
<p><strong>Determinism:</strong> Deterministic.</p>
<p><strong>Errors:</strong> No errors.</p>
<p><strong>Example in TLA+:</strong></p>
<pre><code class="language-tla">\* @typeAlias: DRINK =
<pre><code class="language-tla">\* @typeAlias: drink =
\* Water({ sparkling: Bool })
\* | Beer({ malt: Str, strength: Int });
\*
\* @type: Bool =&gt; DRINK;
\* @type: Bool =&gt; $drink;
Water(sparkling) == Variant(&quot;Water&quot;, [ sparkling |-&gt; sparkling ])

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

LET drink == Beer(&quot;Dunkles&quot;, 4) IN
Expand Down
40 changes: 20 additions & 20 deletions docs/print.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10523,39 +10523,39 @@ <h1><a class="header" href="#variants" id="variants">Variants</a></h1>
</code></pre>
<p>To make it easier to represent the fruits, we can introduce variants together with
user-defined constructors for each option::</p>
<pre><code class="language-tla">\* @typeAlias: FRUIT = Apple(Str) | Orange(Bool);
<pre><code class="language-tla">\* @typeAlias: fruit = Apple(Str) | Orange(Bool);

\* @type: Str =&gt; FRUIT;
\* @type: Str =&gt; $fruit;
Apple(color) == Variant(&quot;Apple&quot;, color)

\* @type: Bool =&gt; FRUIT;
\* @type: Bool =&gt; $fruit;
Orange(seedless) == Variant(&quot;Orange&quot;, seedless)
</code></pre>
<p>Now we can naturally construct apples and orange as follows:</p>
<pre><code class="language-tla">Apple(&quot;red&quot;)
Orange(TRUE)
</code></pre>
<p>Variants can wrap records, for when we want to represent compound data with named fields:</p>
<pre><code class="language-tla">\* @typeAlias: DRINK =
<pre><code class="language-tla">\* @typeAlias: drink =
\* Water({ sparkling: Bool })
\* | Beer({ malt: Str, strength: Int });
\*
\* @type: Bool =&gt; DRINK;
\* @type: Bool =&gt; $drink;
Water(sparkling) == Variant(&quot;Water&quot;, [ sparkling |-&gt; sparkling ])

\* @type: (Str, Int) =&gt; DRINK;
\* @type: (Str, Int) =&gt; $drink;
Beer(malt, strength) == Variant(&quot;Beer&quot;, [ malt |-&gt; malt, strength |-&gt; strength ])
</code></pre>
<p>Once a variant is constructed, it becomes opaque to the type checker, that is,
the type checker only knows that <code>Water(TRUE)</code> and <code>Beer(&quot;Dark&quot;, 5)</code> are both
of type <code>DRINK</code>. This is exactly what we want, in order to combine these values
of type <code>drink</code>. 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.</p>
<p><strong>Filtering by tag name.</strong> Following the idiomatic use of tagged unions in
untyped TLA+, we can filter a set of variants:</p>
<pre><code class="language-tla">LET Drinks == { Water(TRUE), Water(FALSE), Beer(&quot;Radler&quot;, 2) } IN
\E d \in VariantFilter(&quot;Beer&quot;, Drink):
\E d \in VariantFilter(&quot;Beer&quot;, Drinks):
d.strength &lt; 3
</code></pre>
<p>We believe that <code>VariantFilter</code> is the most commonly used way to partition a
Expand Down Expand Up @@ -10608,14 +10608,14 @@ <h3><a class="header" href="#variant-constructor" id="variant-constructor">Varia
<p><strong>Determinism:</strong> Deterministic.</p>
<p><strong>Errors:</strong> No errors.</p>
<p><strong>Example in TLA+:</strong></p>
<pre><code class="language-tla">\* @typeAlias: DRINK =
<pre><code class="language-tla">\* @typeAlias: drink =
\* Water({ sparkling: Bool })
\* | Beer({ malt: Str, strength: Int });
\*
\* @type: Bool =&gt; DRINK;
\* @type: Bool =&gt; $drink;
Water(sparkling) == Variant(&quot;Water&quot;, [ sparkling |-&gt; sparkling ])

\* @type: (Str, Int) =&gt; DRINK;
\* @type: (Str, Int) =&gt; $drink;
Beer(malt, strength) == Variant(&quot;Beer&quot;, [ malt |-&gt; malt, strength |-&gt; strength ])
</code></pre>
<hr />
Expand Down Expand Up @@ -10649,14 +10649,14 @@ <h3><a class="header" href="#variant-filter" id="variant-filter">Variant filter<
<p><strong>Determinism:</strong> Deterministic.</p>
<p><strong>Errors:</strong> No errors.</p>
<p><strong>Example in TLA+:</strong></p>
<pre><code class="language-tla">\* @typeAlias: DRINK =
<pre><code class="language-tla">\* @typeAlias: drink =
\* Water({ sparkling: Bool })
\* | Beer({ malt: Str, strength: Int });
\*
\* @type: Bool =&gt; DRINK;
\* @type: Bool =&gt; $drink;
Water(sparkling) == Variant(&quot;Water&quot;, [ sparkling |-&gt; sparkling ])

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

LET Drinks == { Water(TRUE), Water(FALSE), Beer(&quot;Radler&quot;, 2) } IN
Expand All @@ -10680,14 +10680,14 @@ <h3><a class="header" href="#unpacking-a-variant-safely" id="unpacking-a-variant
<p><strong>Determinism:</strong> Deterministic.</p>
<p><strong>Errors:</strong> No errors.</p>
<p><strong>Example in TLA+:</strong></p>
<pre><code class="language-tla">\* @typeAlias: DRINK =
<pre><code class="language-tla">\* @typeAlias: drink =
\* Water({ sparkling: Bool })
\* | Beer({ malt: Str, strength: Int });
\*
\* @type: Bool =&gt; DRINK;
\* @type: Bool =&gt; $drink;
Water(sparkling) == Variant(&quot;Water&quot;, [ sparkling |-&gt; sparkling ])

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

LET water == Water(TRUE) IN
Expand All @@ -10713,14 +10713,14 @@ <h3><a class="header" href="#unpacking-a-variant-unsafely" id="unpacking-a-varia
<p><strong>Determinism:</strong> Deterministic.</p>
<p><strong>Errors:</strong> No errors.</p>
<p><strong>Example in TLA+:</strong></p>
<pre><code class="language-tla">\* @typeAlias: DRINK =
<pre><code class="language-tla">\* @typeAlias: drink =
\* Water({ sparkling: Bool })
\* | Beer({ malt: Str, strength: Int });
\*
\* @type: Bool =&gt; DRINK;
\* @type: Bool =&gt; $drink;
Water(sparkling) == Variant(&quot;Water&quot;, [ sparkling |-&gt; sparkling ])

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

LET drink == Beer(&quot;Dunkles&quot;, 4) IN
Expand Down
2 changes: 1 addition & 1 deletion docs/searchindex.js
View file

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion docs/searchindex.json
View file

Large diffs are not rendered by default.

0 comments on commit 5d2987b

Please sign in to comment.