diff --git a/content/blog/bergamot/index.md b/content/blog/bergamot/index.md index a46fcde..47215f6 100644 --- a/content/blog/bergamot/index.md +++ b/content/blog/bergamot/index.md @@ -36,9 +36,9 @@ 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\\)). +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. @@ -49,8 +49,8 @@ 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 +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. @@ -85,8 +85,8 @@ Let me show you both, and try to explain the two. First, here's the wrong way: {{< /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 +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`, @@ -301,8 +301,8 @@ 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\\). +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.