Add an initial draft of the Bergamot post.

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

content/blog/bergamot/index.md

@@ -0,0 +1,346 @@
+---
+title: "Bergamot: Exploring Programming Language Inference Rules"
+date: 2023-12-22T18:16:44-08:00
+draft: true
+tags: ["Project", "Programming Languages"]
+description: "In this post, I show off Bergamot, a tiny logic programming language and an idea for teaching inference rules."
+---
+
+{{< katex_component_js >}}
+{{< bergamot_js_css >}}
+
+### Inference Rules and the Study of Programming Languages
+In this post, I will talk about _inference rules_, particularly in the field
+of programming language theory. The first question to get out of the way is
+"what on earth is an inference rule?". The answer is simple: an inference rule
+is just a way of writing "if ... then ...". When writing an inference rule,
+we write the "if" stuff above a line, and the "then" stuff below the line. Really,
+that's all there is to it. I'll steal an example from another one of my posts on the blog -- here's an inference rule:
+
+{{< latex >}}
+\frac
+{\text{I'm allergic to cats} \quad \text{My friend has a cat}}
+{\text{I will not visit my friend very much}}
+{{</ latex >}}
+
+We can read this as "__if__ I'm allergic to cats, and my friend has a cat, __then__
+I will not visit my friend very much".
+
+In the field of programming languages, _inference rules_ are everywhere.
+Practically any paper I read has a table that looks something like this:
+
+{{< figure src="rules.png" caption="Inference rules from [Logarithm and program testing](https://dl.acm.org/doi/abs/10.1145/3498726) by Kuen-Bang Hou (Favonia) and Zhuyang Wang" class="fullwide" >}}
+
+And I, for one, love it! They're a precise and concise way to describe static
+and dynamic behavior of programs. I might've written this elsewhere on the blog,
+but whenever I read a paper, my eyes search for the rules first and foremost.
+
+But to those just starting their PL journey, inference rules can be quite cryptic
+-- I know they were to me! The first level of difficulty are the symbols: we have
+lots of Greek (\\(\\Gamma\\) and \\(\\Delta\\) for environments, \\(\\tau\\) and perhaps \\(\\sigma\\)
+for types), and the occasional mathematical symbol (the "entails" symbol \\(\\vdash\\) is the most
+common, but for operational semantics we can have \\(\\leadsto\\) and \\(\\Downarrow\\)).
+If you don't know what they mean, or if you're still getting used to them, symbols
+in judgements are difficult enough to parse.
+
+The second level of difficulty is making sense of the individual rules:
+individually, they tend to not be too bad, but for some languages, even making
+sense of one rule can be challenging. The following rule from the Calculus of
+Inductive Constructions is a doozy, for instance.
+
+{{< figure src="CIC.png" caption="The `match` inference rule from [Introduction to the Calculus of Inductive Constructions](https://inria.hal.science/hal-01094195/document) by Christine Paulin-Mohring" class="fullwide" >}}
+
+Just look at the metavariables! We have \\(\\textit{pars}\\), \\(t_1\\) through \\(t_p\\), 
+\\(x_1\\) through \\(x_n\\), plain \\(x\\), and at least two other sets of variables. Not
+only this, but the rule requires at least some familiarity with [GADTs](https://en.wikipedia.org/wiki/Generalized_algebraic_data_type) to understand
+completely.
+
+The third level is making sense of how the rules work, _together_. In my
+programming languages class in college, a familiar question was:
+
+> the [Hindley-Milner type system](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system)
+> supports let-polymorphism only. What is it about the rules that implies let-polymorphism,
+> and not any other kind of polymorphism?
+
+If you don't know the answer, or the question doesn't make sense do you, don't
+worry about it -- suffice to say that whole systems of inference rules exhibit
+certain behaviors, and it takes familiarity with several rules to spot these
+behaviors.
+
+### Seeing What Works and What Doesn't
+
+Maybe I'm just a tinker-y sort of person, but for me, teaching inference rules
+just by showing them is not really enough. For instance, let me show you two
+ways of writing the following (informal) rule:
+
+> When adding two expressions, if both expressions are strings, then thse result
+> of adding them is also a string.
+
+There's a right way to write this inference rule, and there is a wrong way.
+Let me show you both, and try to explain the two. First, here's the wrong way:
+
+{{< latex >}}
+\cfrac
+    {x : \text{string} \in \Gamma \quad y : \text{string} \in \Gamma}
+    {\Gamma \vdash x + y : \text{string}}
+{{< /latex >}}
+
+This says that the type of adding two _variables_ of type `string` is still `string`.
+Here, \\(\\Gamma\\) is a _context_, which keeps track of which variable has what
+type. Writing \\(x : \\text{string} \\in \\Gamma\\) is the same as saying
+"we know the variable `x` has type `string`. The whole rule reads,
+
+> If the variables `x` and `y` both have type `string`,
+> then the result of adding these two variables, `x+y`, also has type `string`.
+
+The trouble with this rule is that it only works when adding two variables.
+But `x+x` is not itself a variable, so the rule wouldn't work for an expression
+like `(x+x)+(y+y)`. The proper way of writing the rule is, then, something like
+this:
+
+{{< latex >}}
+\cfrac
+    {\Gamma \vdash e_1 : \text{string} \quad \Gamma \vdash e_2 : \text{string}}
+    {\Gamma \vdash e_1 + e_2 : \text{string}}
+{{< /latex >}}
+
+This rule says:
+
+> If the two subexpressions `e1` and `e2` both have type `string`,
+> then the result of adding these two subexpressions, `e1+e2`, also has type `string`.
+
+Much better! We can apply this rule recursively: to get the type of `(x+x)+(y+y)`,
+we consider `(x+x)` and `(y+y)` as two subexpressions, and go on to compute
+their types first. We can then break `(x+x)` into two subexpressions (`x` and `x`),
+and determine their type separately. Supposing that the variables `x` and `y`
+indeed have the type `string`, this tells us that `(x+x)` and `(y+y)` are both
+string, and therefore that the whole of `(x+x)+(y+y)` is a string.
+
+What I'd really like to do is type the program in question and have the
+computer figure out whether my rules accept or reject this program.
+With my new rules, perhaps I'd get something like this:
+
+{{< figure src="goodrule.png" caption="Verifying the `(x+x)+(y+y)` expression using the good rule" class="fullwide" >}}
+
+On the other hand, since this expression doesn't work with my old rules, maybe
+i wouldn't get a valid type at all:
+
+{{< figure src="badrule.png" caption="Verifying (unsuccessfully) the `(x+x)+(y+y)` expression using the old rule" class="fullwide" >}}
+
+More generally, I want to be able to write down some inference rules, and apply
+them to some programs. This way, I can see what works and what doesn't, and when
+it works, which rules were used for what purposes. I also want to be able to
+try tweaking, removing, or adding inference rules, to see what breaks.
+
+This brings me to the project that I'm trying to show off in this post:
+Bergamot!
+
+### Introducing Bergamot
+
+A certain class of programming languages lends itself particularly well to
+writing inference rules and applying them to programs: logic programming.
+The most famous example of a logic programming language is [Prolog](https://www.swi-prolog.org/).
+In logic programming languages like Prolog, we can write rules describing when
+certain statements should hold. The simplest rule I could write is a fact. Perhaps
+I'd like to say that the number 42 is a "good" number:
+
+```Prolog
+good(42).
+```
+
+Perhaps I'd then like to say that adding two good numbers together creates
+another good number.
+
+```Prolog
+good(N) :- good(A), good(B), N is A+B.
+```
+
+The above can be read as:
+
+> the number `N` is good if the numbers `A` and `B` are good, and `N` is the sum of `A` and `B`.
+
+I can then ask Prolog to give me some good numbers:
+
+```Prolog
+?- good(X)
+```
+
+Prompting Prolog a few times, I get:
+
+```
+X = 42
+X = 84
+X = 126
+X = 168
+```
+
+It's not a huge leap from this to programming language type rules. Perhaps instead
+of something being "good", we can say that it has type `string`. Of course, adding
+two strings together, as we've established, creates another string. In Prolog:
+
+```Prolog
+/* A string literal like "hello" has type string */
+type(_, strlit(_), string).
+/* Adding two string expressions has type string */
+type(Env, plus(X, Y), string) :- type(Env, X, string), type(Env, Y, string).
+```
+
+That's almost identical to our inference rules above, except that it's written
+using code instead of mathematical notation! If we could just take these
+Prolog rules and display them as inference rules, we'd be able to "have our cake"
+(draw pretty inference rules like in the papers) and "eat it too" (run our rules
+on the computer against various programs).
+
+This is where it gets a teensy bit hairy. It's not that easy to embed a Prolog
+engine into the browser; alternatives that I've surveyed are either poorly documented,
+hard to extend, or both. Furthermore, for studying _what each rule was used for_,
+it's nice to be able to see a _proof tree_: a tree made up from the rules that
+we used to arrive at a particular answer. Prolog engines are excellent at
+applying rules and finding answers, but they don't usually provide a way
+to get all the rules that were used, making it harder to get proof trees.
+
+Thus, [Bergamot](https://dev.danilafe.com/Everything-I-Know-About-Types/bergamot-elm)
+is a new, tiny programming language that I threw together in a couple of days.
+It comes as JavaScript-based widget, and can be embedded into web pages like
+this one to provide an interactive way to write and explore proof trees. Here's
+a screenshot of what all of that looks like:
+
+{{< figure src="bergamot.png" caption="A screenshot of a Bergamot widget with some type rules" class="fullwide" >}}
+
+The components of Bergamot are:
+
+* The programming languages, as stated above. This language is a very simple,
+  unification-based logic programming language.
+* A rule rendering system, which takes Prolog-like rules written in Bergamot
+  and converts them into pretty LaTeX inference rules.
+* An Elm-based widget that you can embed into your web page, which accepts
+  Bergamot rule and an input expression, and applies the rules to produce
+  a result (or a whole proof tree!).
+
+Much like in Prolog, we can write Bergamot rules that describe when certain
+things are true. Unlike Prolog, Bergamot requires each rule to have a name.
+This is common practice in programming languages literature (when we talk
+about rules in papers, we like to be able to refer to them by name). Below
+are some sample Bergamot rules, corresponding to the first few inference rules
+in the above screenshot.
+
+```
+TNumber @ type(?Gamma, intlit(?n), number) <-;
+TString @ type(?Gamma, strlit(?s), string) <-;
+TVar @ type(?Gamma, var(?x), ?tau) <- inenv(?x, ?tau, ?Gamma);
+TPlusI @ type(?Gamma, plus(?e_1, ?e_2), number) <-
+    type(?Gamma, ?e_1, number), type(?Gamma, ?e_2, number);
+TPlusS @ type(?Gamma, plus(?e_1, ?e_2), string) <-
+    type(?Gamma, ?e_1, string), type(?Gamma, ?e_2, string);
+```
+
+Unlike Prolog, where "variables" are anything that starts with a capital letter,
+in Bergamot, variables are things that start with the special `?` symbol. Also,
+Prolog's `:-` has been replaced with an arrow symbol `<-`, for reverse implication.
+These are both purely syntactic differences.
+
+#### Demo
+If you want to play around with it, here's an embedded Bergamot widget with
+{{< sidenote "right" "wrong-rule-note" "some rules pre-programmed in." >}}
+Actually, one of the rules is incorrect to my knowledge. Can you spot it?
+Hint: is <code>\x : number. \x: string. x+1</code> well-typed? What does
+Bergamot report? Can you see why?
+{{< /sidenote >}}
+It has two modes:
+
+1. __Language Term__: accepts a rather simple programming language
+   to typecheck. Try `1+1`, `fst((1,2))`, or maybe `(\x : number. x) 42`.
+2. __Query__: it accepts Bergamot expressions to query, similarly to Prolog; try
+   `type(empty, ?e, tpair(number, string))` to search for expressions that have
+   the type "a pair of a number and a string".
+
+{{< bergamot_widget id="widget-one" query="" prompt="PromptConverter @ prompt(type(empty, ?term, ?t)) <- input(?term);" >}}
+section "" {
+    TNumber @ type(?Gamma, intlit(?n), number) <- int(?n);
+    TString @ type(?Gamma, strlit(?s), string) <- str(?s);
+    TVar @ type(?Gamma, var(?x), ?tau) <- inenv(?x, ?tau, ?Gamma);
+    TPlusI @ type(?Gamma, plus(?e_1, ?e_2), number) <-
+        type(?Gamma, ?e_1, number), type(?Gamma, ?e_2, number);
+    TPlusS @ type(?Gamma, plus(?e_1, ?e_2), string) <-
+        type(?Gamma, ?e_1, string), type(?Gamma, ?e_2, string);
+}
+section "" {
+    TPair @ type(?Gamma, pair(?e_1, ?e_2), tpair(?tau_1, ?tau_2)) <-
+        type(?Gamma, ?e_1, ?tau_1), type(?Gamma, ?e_2, ?tau_2);
+    TFst @ type(?Gamma, fst(?e), ?tau_1) <-
+        type(?Gamma, ?e, tpair(?tau_1, ?tau_2));
+    TSnd @ type(?Gamma, snd(?e), ?tau_2) <-
+        type(?Gamma, ?e, tpair(?tau_1, ?tau_2));
+}
+section "" {
+    TAbs @ type(?Gamma, abs(?x, ?tau_1, ?e), tarr(?tau_1, ?tau_2)) <-
+        type(extend(?Gamma, ?x, ?tau_1), ?e, ?tau_2);
+    TApp @ type(?Gamma, app(?e_1, ?e_2), ?tau_2) <-
+        type(?Gamma, ?e_1, tarr(?tau_1, ?tau_2)), type(?Gamma, ?e_2, ?tau_1);
+}
+
+section "" {
+    GammaTake @ inenv(?x, ?tau_1, extend(?Gamma, ?x, ?tau_1)) <-;
+    GammaSkip @ inenv(?x, ?tau_1, extend(?Gamma, ?y, ?tau_2)) <- inenv(?x, ?tau_1, ?Gamma);
+}
+{{< /bergamot_widget >}}
+
+#### Rendering Bergamot with Bergamot
+
+There's something to be said about the conversion between Bergamot's rules,
+encoded as plain text, and pretty LaTeX-based inference rules that the users
+see. Crucially, __we don't want to hardcode how any particular Bergamot
+expression is rendered__. For one, this is a losing battle: we can't possibly
+keep up with all the notation that people use in PL literature, and even if
+we focused ourselves on only "beginner" notation, there wouldn't be one way to do it!
+Different PL papers and texts use slightly different variations of notation.
+For instance, I render my pairs as \\((a, b)\\), but the very first screenshot
+in this post demonstrates a PL paper that writes pairs as \\(\\langle a, b \\rangle\\).
+Neither way (as far as I know!) is right or wrong. But if we hardcode one,
+we lose the ability to draw the other.
+
+More broadly, one aspect about writing PL rules is that _we control the notation_.
+We are free to define shorthands, symbols, and anything else that would make
+reading our rules easier for others. As an example, a paper from POPL22 about
+programming language semantics with garbage collection used a literal trash
+symbol in their rules:
+
+{{< figure src="trashrule.png" caption="A rule that uses a trashcan icon as notation, from [A separation logic for heap space under garbage collection](https://dl.acm.org/doi/10.1145/3498672) by Jean-Marie Madiot and François Pottier" >}}
+
+Thus, what I want to do is __encourage the (responsible) introduction of new notation__.
+This can only be done if Bergamot itself supports custom notation.
+
+When thinking about how I'd like to implement this custom notation, I was imagining
+some sort of templated rule engine, that would define how each term in a Bergamot
+program can be converted to its LaTeX variant. But then I realized: Bergamot
+is already a rule engine! Instead of inventing yet another language or format
+for defining LaTeX pretty printing, I could just use Bergamot. This turned
+out to work quite nicely -- the "Presentation Rules" tab in the demo above
+should open a text editor with Bergamot rules that handle the conversion
+of Bergamot notation into LaTex. Here are some example rules:
+
+```
+LatexPlus @ latex(plus(?e_1, ?e_2), ?l) <- latex(?e_1, ?l_1), latex(?e_2, ?l_2), join([?l_1, " + ", ?l_2], ?l);
+LatexPair @ latex(pair(?e_1, ?e_2), ?l) <- latex(?e_1, ?l_1), latex(?e_2, ?l_2), join(["(", ?l_1, ",  ", ?l_2, ")"], ?l);
+```
+
+If we change the `LatexPair` to the following, we can make all pairs render
+using angle brackets:
+
+```
+LatexPair @ latex(pair(?e_1, ?e_2), ?l) <- latex(?e_1, ?l_1), latex(?e_2, ?l_2), join(["\\langle", ?l_1, ",  ", ?l_2, "\\rangle"], ?l);
+```
+
+{{< figure src="rangle.png" caption="The LaTeX output when angle brackets are used in the rule instead of parentheses." >}}
+
+You can write rules about arbitrary Bergamot terms for rendering; thus, you can
+invent completely new notation for absolutely anything.
+
+### Next Steps
+
+I hope to use Bergamot to write a series of articles about type systems. By
+providing an interactive widget, I hope to make it possible for users to do
+exercises: writing variations of inference rules, or even tweaking the notation,
+and checking them against sets of programs to make sure that they work. Of course,
+I also that Bergamot can be used to explore _why_ an existing set of inference
+rules (such as Hindley-Milner) works. Stay tuned for those!