blog-static/content/blog/bergamot/index.md

---
title: "Bergamot: Exploring Programming Language Inference Rules"
date: 2023-12-22T18:16:44-08:00
tags: ["Project", "Programming Languages"]
description: "In this post, I show off Bergamot, a tiny logic programming language and an idea for teaching inference rules."
bergamot:
    render_presets:
        default: "lc.bergamot"
---

### 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:
although they tend to not be too bad, 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 operands, if both operands are strings, then the 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" >}}

To fully understand how the rule works to check a big expression like the above
sum, I'd need to see the recursion we applied a couple of paragraphs ago. My
ideal tool would display this too. For simplicity, I'll just show the output
for `(1+1)+(1+1)`, sidestepping variables and using numbers instead. This just
saves a little bit of space and visual noise.

{{< figure src="goodrulerec.png" caption="Verifying the `(1+1)+(1+1)` expression using the good rule" class="fullwide" >}}

On the other hand, since the sum of two `x`s and two `y`s 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 language, 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" query="" prompt="type(empty, TERM, ?t)" >}}
section "" {
    TNumber @ type(?Gamma, lit(?n), number) <- num(?n);
    TString @ type(?Gamma, lit(?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 hope that Bergamot can be used to explore _why_ an existing set of inference
rules (such as Hindley-Milner) works. Stay tuned for those!