Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Proofread and publish bergamot post

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-12-22 22:15:17 -08:00
parent b001bba3b8
commit 16086e79b0
2 changed files with 15 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

BIN
content/blog/bergamot/goodrulerec.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 134 KiB

23
content/blog/bergamot/index.md
View File

@ -1,7 +1,6 @@
--- ---
title: "Bergamot: Exploring Programming Language Inference Rules" title: "Bergamot: Exploring Programming Language Inference Rules"
date: 2023-12-22T18:16:44-08:00 date: 2023-12-22T18:16:44-08:00
draft: true
tags: ["Project", "Programming Languages"] tags: ["Project", "Programming Languages"]
description: "In this post, I show off Bergamot, a tiny logic programming language and an idea for teaching inference rules." description: "In this post, I show off Bergamot, a tiny logic programming language and an idea for teaching inference rules."
--- ---
@ -26,7 +25,7 @@ that's all there is to it. I'll steal an example from another one of my posts on
We can read this as "__if__ I'm allergic to cats, and my friend has a cat, __then__ 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". I will not visit my friend very much".
In the field of programming languages, _inference rules_ are everywhere. In the field of programming languages, inference rules are everywhere.
Practically any paper I read has a table that looks something like this: 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" >}} {{< 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" >}}
@ -44,7 +43,7 @@ If you don't know what they mean, or if you're still getting used to them, symbo
in judgements are difficult enough to parse. in judgements are difficult enough to parse.
The second level of difficulty is making sense of the individual rules: 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 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 sense of one rule can be challenging. The following rule from the Calculus of
Inductive Constructions is a doozy, for instance. Inductive Constructions is a doozy, for instance.
@ -73,7 +72,7 @@ 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 just by showing them is not really enough. For instance, let me show you two
ways of writing the following (informal) rule: ways of writing the following (informal) rule:
> When adding two expressions, if both expressions are strings, then thse result > When adding two operands, if both operands are strings, then the result
> of adding them is also a string. > of adding them is also a string.
There's a right way to write this inference rule, and there is a wrong way. There's a right way to write this inference rule, and there is a wrong way.
@ -88,7 +87,7 @@ Let me show you both, and try to explain the two. First, here's the wrong way:
This says that the type of adding two _variables_ of type `string` is still `string`. 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 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 type. Writing \\(x : \\text{string} \\in \\Gamma\\) is the same as saying
"we know the variable `x` has type `string`. The whole rule reads, "we know the variable `x` has type `string`". The whole rule reads,
> If the variables `x` and `y` both have type `string`, > If the variables `x` and `y` both have type `string`,
> then the result of adding these two variables, `x+y`, also has type `string`. > then the result of adding these two variables, `x+y`, also has type `string`.
@ -122,7 +121,15 @@ 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" >}} {{< 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 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: 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" >}} {{< figure src="badrule.png" caption="Verifying (unsuccessfully) the `(x+x)+(y+y)` expression using the old rule" class="fullwide" >}}
@ -209,7 +216,7 @@ a screenshot of what all of that looks like:
The components of Bergamot are: The components of Bergamot are:
* The programming languages, as stated above. This language is a very simple, * The programming language, as stated above. This language is a very simple,
unification-based logic programming language. unification-based logic programming language.
* A rule rendering system, which takes Prolog-like rules written in Bergamot * A rule rendering system, which takes Prolog-like rules written in Bergamot
and converts them into pretty LaTeX inference rules. and converts them into pretty LaTeX inference rules.
@ -342,5 +349,5 @@ 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 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, 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, 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 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! rules (such as Hindley-Milner) works. Stay tuned for those!