Add an exercise about conversions to types: basics

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

content/blog/01_types_basics.md

@@ -384,6 +384,55 @@ from the conversion rules. Chapter 15 of _Types and Programming Languages_
 by Benjamin Pierce is a nice explanation, but the [Wikipedia page](https://en.wikipedia.org/wiki/Subtyping)
 ain't bad, either.
 
+{{< bergamot_preset name="conversion-preset" prompt="PromptConverter @ prompt(type(?term, ?t)) <- input(?term);" >}}
+section "Conversion rules" {
+    ConvertsIS @ converts(integer, string) <-;
+    ConvertsIF @ converts(integer, float) <-;
+    ConvertsFS @ converts(float, string) <-;
+}
+
+section "Rules for literals" {
+    TInt @ type(lit(?n), integer) <- int(?n);
+    TFloat @ type(lit(?f), float) <- float(?f);
+    TString @ type(lit(?s), string) <- str(?s);
+}
+
+section "" {
+    TPlusInt @ type(plus(?e_1, ?e_2), integer) <- type(?e_1, integer), type(?e_2, integer);
+    TPlusFloat @ type(plus(?e_1, ?e_2), float) <- type(?e_1, float), type(?e_2, float);
+    TPlusString @ type(plus(?e_1, ?e_2), string) <- type(?e_1, string), type(?e_2, string);
+}
+
+TConverts @ type(?e, ?tau_2) <- type(?e, ?tau_1), converts(?tau_1, ?tau_2);
+{{< /bergamot_preset >}}
+
+{{< bergamot_exercise label="advanced; a taste of conversions" preset="conversion-preset" id="exercise-3" >}}
+This exercise is simply an early taste of formalizing conversions, which
+allow users to (for example) write numbers where the language expects strings, with the
+understanding that the number will be automatically turned into a string.
+
+To avoid having an explosion of various rules, we instead define the "converts to"
+relation, \\(\\tau_1 \\preceq \\tau_2\\), where \\(\\tau_1\\) and \\(\\tau_2\\)
+are types. To say that an integer can be automatically converted to a floating
+pointer number, we can write \\(\\text{integer} \\preceq \\text{float}\\).
+Then, we add only a single additional rule to our language: `TConverts`.
+This rule says that we can treat an expression of type \\(\\tau_1\\) as
+an expression of type \\(\\tau_2\\), if the former can be converted to the
+latter.
+
+I have written some rules using these concepts. Input some expressions into
+the box below that would require a conversion: some examples might be
+`1 + 3.14` (adding an integer to a float), `1 + "hello"` (adding
+an integer to a string), and `1.0 + "hello"` (adding a float to a string).
+Click the "Proof Tree" tab to see how the various rules combine to make
+the expression well-typed.
+
+Now, remove the `ConvertsIS` rule that allows integers to be converted to
+strings. Do all of the expressions from the previous paragraph still typecheck?
+Can you see why?
+
+{{< /bergamot_exercise >}}
+
 Subtyping, however, is quite a bit beyond the scope of a "basics"
 post. For the moment, we shall content ourselves with the tedious approach.
 

layouts/shortcodes/bergamot_js_css.html

@@ -68,6 +68,8 @@ const renderRules =
     LatexTypeBin @ latex(type(?e, ?t), ?l) <- latex(?e, ?l_e), latex(?t, ?l_t), join([?l_e, " : ", ?l_t], ?l);
     LatexTypeTer @ latex(type(?G, ?e, ?t), ?l) <- latex(?G, ?l_G), latex(?e, ?l_e), latex(?t, ?l_t), join([?l_G, " \\\\vdash ", ?l_e, " : ", ?l_t], ?l);
 
+    LatexConverts @ latex(converts(?f, ?t), ?l) <- latex(?f, ?l_f), latex(?t, ?l_t), join([?l_f, " \\\\preceq ", ?l_t], ?l);
+
     LatexIsInt @ latex(int(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\\\in \\\\texttt{Int}"], ?l);
     LatexIsFloat @ latex(float(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\\\in \\\\texttt{Float}"], ?l);
     LatexIsNum @ latex(num(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\\\in \\\\texttt{Num}"], ?l);