diff --git a/content/blog/01_types_basics.md b/content/blog/01_types_basics.md index e319558..8511940 100644 --- a/content/blog/01_types_basics.md +++ b/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. diff --git a/layouts/shortcodes/bergamot_js_css.html b/layouts/shortcodes/bergamot_js_css.html index 6ae8bc7..0cefd24 100644 --- a/layouts/shortcodes/bergamot_js_css.html +++ b/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);