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

Start explaining exercises in types intro.

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-12-27 23:31:28 -08:00
parent 8742c6e7b9
commit ed4fcf5e9d
1 changed files with 39 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

39
content/blog/00_types_intro.md
View File

@ -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 >}}