Add a couple of exercises to types: basics.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

content/blog/01_types_basics.md

@@ -114,6 +114,24 @@ Another consequence of this is that not everyone agrees on notation; according
 to [this paper](https://labs.oracle.com/pls/apex/f?p=LABS:0::APPLICATION_PROCESS%3DGETDOC_INLINE:::DOC_ID:959),
 27 different ways of writing down substitutions were observed in the POPL conference alone.
 
+{{< bergamot_preset name="notation-preset" prompt="PromptConverter @ prompt(type(?term, ?t)) <- input(?term);" >}}
+TNumber @ type(lit(?n), number) <- num(?n);
+{{< /bergamot_preset >}}
+
+{{< bergamot_exercise label="bergamot; tweaking notation" preset="notation-preset" id="exercise-1" >}}
+Bergamot, the interactive tool I've developed for doing exercises, supports
+customizing the notation for rules. Try changing the \(:\) symbol to
+the \(\sim\) symbol (denoted in latex as <code>\sim</code>).<br>
+<br>
+To change the way that rules are rendered, click the "Presentation Rules"
+tab in the "Rules" section. There will be a lot there: I've added rules for
+pretty-printing a fair amount of the standard programming languages notation.
+Scroll down to <code>LatexTypeBin</code>, and change <code>:</code> to
+<code>\\sim</code> on that line (the extra backslash is to handle string
+escaping). Now try typing numbers into the input box; you should see
+something like \(1 \sim \text{number} \)
+{{< /bergamot_exercise >}}
+
 One more thing. So far, we've only written down one claim: the value 1 is a number.
 What about the other numbers? To make sure they're accounted for, we need similar
 rules for 2, 3, and so on.
@@ -299,6 +317,37 @@ This rule is read as follows:
 
 > If \\(e_1\\) and \\(e_2\\) have type \\(\\text{string}\\), then \\(e_1+e_2\\) has type \\(\\text{string}\\).
 
+{{< bergamot_preset name="string-preset" prompt="PromptConverter @ prompt(type(?term, ?t)) <- input(?term);" query="\"hello\"+\"world\"">}}
+TNumber @ type(lit(?n), number) <- num(?n);
+TPlusI @ type(plus(?e_1, ?e_2), number) <-
+    type(?e_1, number), type(?e_2, number);
+{{< /bergamot_preset >}}
+
+{{< bergamot_exercise label="bergamot; adding rules for strings" preset="string-preset" id="exercise-2" >}}
+Try writing the Bergamot rules that correspond to the inference rule for strings
+above. I've provided the rules for numbers; the rules for strings should be quite
+similar.<br>
+<br>
+In Bergamot, the claim that an expression <code>e</code> has type <code>t</code>
+is written as <code>type(e, t)</code>. A rule looks like <code>RuleName @ conclusion <- premise1, premise2;</code>.
+Thus, the rule <pre><code>TNumber @ type(lit(?n), number) <- num(?n);
+</code></pre>
+Has one premise, that the term \(n\) is a number, and the conclusion is that
+a number literal has type \(\text{number}\). The <code>num</code> condition
+is a Bergamot builtin, corresponding to our earlier notation of \(n \in \texttt{Num}\).
+It holds for all numbers: it's always true that <code>num(1)</code>, <code>num(2)</code>,
+etc. The equivalent builtin for something being a string is <code>str</code>.<br>
+<br>
+To edit the rules in Bergamot, click the "Editor" button in the "Rules"
+section. You will need to add two rules, just like we did for numbers:
+a rule for string literals (something like \(\texttt{"Hello"} : \text{string}\),
+but more general) and for adding two strings together. I suggest naming
+these two rules <code>TString</code> and <code>TPlusS</code> respectively.<br>
+<br>
+When you're done, you should be able to properly determine the types of
+expressions such as <code>"Hello"</code> and <code>"Hello" + "World"</code>.
+{{< /bergamot_exercise >}}
+
 These rules generally work in other languages. Things get more complicated in languages like Java and Rust,
 where types for numbers are more precise (\\(\\text{int}\\) and \\(\\text{float}\\) instead of
 \\(\\text{number}\\)). In these languages, we need rules for both.