diff --git a/content/blog/01_types_basics.md b/content/blog/01_types_basics.md index 39264f0..0dee2fa 100644 --- a/content/blog/01_types_basics.md +++ b/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 \sim).
+
+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 LatexTypeBin, and change : to +\\sim 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.
+
+In Bergamot, the claim that an expression e has type t +is written as type(e, t). A rule looks like RuleName @ conclusion <- premise1, premise2;. +Thus, the rule
TNumber @ type(lit(?n), number) <- num(?n);
+
+Has one premise, that the term \(n\) is a number, and the conclusion is that +a number literal has type \(\text{number}\). The num 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 num(1), num(2), +etc. The equivalent builtin for something being a string is str.
+
+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 TString and TPlusS respectively.
+
+When you're done, you should be able to properly determine the types of +expressions such as "Hello" and "Hello" + "World". +{{< /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.