From ed4fcf5e9d5c2e27a8dfb7571f656c8b7091b9ce Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Wed, 27 Dec 2023 23:31:28 -0800
Subject: [PATCH] Start explaining exercises in types intro.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 content/blog/00_types_intro.md | 39 ++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)

diff --git a/content/blog/00_types_intro.md b/content/blog/00_types_intro.md
index 2835bf6..db1fa57 100644
--- a/content/blog/00_types_intro.md
+++ b/content/blog/00_types_intro.md
@@ -6,6 +6,9 @@ series: "Everything I Know About Types"
 draft: true
 ---
 
+{{< katex_component_js >}}
+{{< bergamot_js_css >}}
+
 I am in love with types and type systems. They are, quite probably,
 my favorite concept in the world. Most of us mere
 mortals use types as a way to make sure we aren't writing
@@ -141,3 +144,39 @@ understanding how to use a crate; check out the
 [documentation page for `Vec`](https://doc.rust-lang.org/std/vec/struct.Vec.html), for instance.
 Documentation of Elm packages always lists functions' types (see [documentation for `Parser`](https://package.elm-lang.org/packages/elm/parser/latest/Parser), for example). Even C++ type signatures
 listed by Doxygen can be quite useful; I, for one, got a lot out of the [LLVM documentation](https://llvm.org/doxygen/classllvm_1_1IRBuilderBase.html).
+
+### Exercises, Bergamot and You
+One of the reasons I love the [Software Foundations](https://softwarefoundations.cis.upenn.edu/)
+series are the exercises. They are within the text, and they are machine-checked:
+if you use a computer tool to work through the tasks, and verify that you did
+them correctly. I hope to do something similar. Exercises will look something
+like this:
+
+{{< bergamot_exercise label="sample exercise" id="exercise-1" >}}
+Here I tell you to do something that I believe would be instructive.
+{{< /bergamot_exercise >}}
+
+To achieve my ideal of interactive exercises, I developed a tool called Bergamot.
+It's a tiny little programming language for writing _inference rules_, which are an invaluable tool
+in a type theorist's toolbox. I introduced the tool in [a separate post on this
+site]({{< relref "bergamot" >}}). Throughout this series, I'll be using Bergamot
+for exercises and mild amounts of interactive content. This is completely optional:
+My aim is to make everything I write self-contained and useful without various
+tools. However, I think that having a way to interactively play with inference
+rules is conducive to learning the concepts.
+
+The unfortunate problem with making a tool for exercises is that you also need
+to teach others how to use the tool. Some exercises will be more specific
+to the tool than to type theory itself; I will denote these exercises as such where
+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="PromptConverter @ prompt(type(?term, ?t)) <- input(?term);" >}}
+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" >}}
+Try typing <code>1+1</code> into the input field!
+{{< /bergamot_exercise >}}