Bring in more theme updates

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-09-15 16:28:07 -07:00
parent 3e46ff8be6
commit 324fa948e6
9 changed files with 53 additions and 46 deletions

View File

@ -6,7 +6,12 @@ series: "Everything I Know About Types"
draft: true
bergamot:
render_presets:
default: "lc.bergamot"
default: "bergamot/rendering/lc.bergamot"
presets:
intro:
prompt: "type(TERM, ?t)"
query: ""
file: "intro.bergamot"
---
I am in love with types and type systems. They are, quite probably,
@ -171,12 +176,6 @@ to the tool than to type theory itself; I will denote these exercises as such wh
possible. Also, whenever the context of the exercise can be loaded into
Bergamot, I will denote this with a play button.
{{< bergamot_preset name="intro-preset" prompt="type(TERM, ?t)" >}}
TNumber @ type(lit(?n), number) <- num(?n);
TPlusI @ type(plus(?e_1, ?e_2), number) <-
type(?e_1, number), type(?e_2, number);
{{< /bergamot_preset >}}
{{< bergamot_exercise label="bergamot; sample exercise" preset="intro-preset" id="exercise-2" >}}
{{< bergamot_exercise label="bergamot; sample exercise" preset="intro" id="exercise-2" >}}
Try typing `1+1` into the input field!
{{< /bergamot_exercise >}}

View File

@ -0,0 +1,3 @@
TNumber @ type(lit(?n), number) <- num(?n);
TPlusI @ type(plus(?e_1, ?e_2), number) <-
type(?e_1, number), type(?e_2, number);

View File

@ -0,0 +1,19 @@
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);

View File

@ -6,7 +6,21 @@ series: "Everything I Know About Types"
draft: true
bergamot:
render_presets:
default: "lc.bergamot"
default: "bergamot/rendering/lc.bergamot"
presets:
notation:
prompt: "type(TERM, ?t)"
query: ""
file: "notation.bergamot"
string:
prompt: "type(TERM, ?t)"
query: "\"hello\"+\"world\""
file: "string.bergamot"
conversion:
prompt: "type(TERM, ?t)"
query: ""
file: "conversion.bergamot"
---
It's finally time to start looking at types. As I mentioned, I want
@ -114,11 +128,7 @@ Another consequence of this is that not everyone agrees on notation; according
to [this paper](https://labs.oracle.com/pls/apex/f?p=LABS:0::APPLICATION_PROCESS%3DGETDOC_INLINE:::DOC_ID:959),
27 different ways of writing down substitutions were observed in the POPL conference alone.
{{< bergamot_preset name="notation-preset" prompt="type(TERM, ?t)" >}}
TNumber @ type(lit(?n), number) <- num(?n);
{{< /bergamot_preset >}}
{{< bergamot_exercise label="bergamot; tweaking notation" preset="notation-preset" id="exercise-1" >}}
{{< bergamot_exercise label="bergamot; tweaking notation" preset="notation" id="exercise-1" >}}
Bergamot, the interactive tool I've developed for doing exercises, supports
customizing the notation for rules. Try changing the \(:\) symbol to
the \(\sim\) symbol (denoted in latex as `\sim`).
@ -317,13 +327,7 @@ This rule is read as follows:
> If \(e_1\) and \(e_2\) have type \(\text{string}\), then \(e_1+e_2\) has type \(\text{string}\).
{{< bergamot_preset name="string-preset" prompt="type(TERM, ?t)" query="\"hello\"+\"world\"">}}
TNumber @ type(lit(?n), number) <- num(?n);
TPlusI @ type(plus(?e_1, ?e_2), number) <-
type(?e_1, number), type(?e_2, number);
{{< /bergamot_preset >}}
{{< bergamot_exercise label="bergamot; adding rules for strings" preset="string-preset" id="exercise-2" >}}
{{< bergamot_exercise label="bergamot; adding rules for strings" preset="string" id="exercise-2" >}}
Try writing the Bergamot rules that correspond to the inference rule for strings
above. I've provided the rules for numbers; the rules for strings should be quite
similar.
@ -384,29 +388,7 @@ 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="type(TERM, ?t)" >}}
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" >}}
{{< bergamot_exercise label="advanced; a taste of conversions" preset="conversion" 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.

View File

@ -0,0 +1 @@
TNumber @ type(lit(?n), number) <- num(?n);

View File

@ -0,0 +1,3 @@
TNumber @ type(lit(?n), number) <- num(?n);
TPlusI @ type(plus(?e_1, ?e_2), number) <-
type(?e_1, number), type(?e_2, number);

View File

@ -5,7 +5,7 @@ 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"
default: "bergamot/rendering/lc.bergamot"
---
### Inference Rules and the Study of Programming Languages

@ -1 +1 @@
Subproject commit dee7579b2956fda6ca64819fa7d08b2832a235a9
Subproject commit 3a281dfa8aff1ac87d33d8f5ffcfc0a931a9656a