From 96545a899f6bceacd88e50627f917749611372be Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 13 May 2024 18:33:30 -0700 Subject: [PATCH] Update "compiler: typechecking" to new math delimiters Signed-off-by: Danila Fedorin --- content/blog/03_compiler_typechecking.md | 72 ++++++++++++------------ 1 file changed, 36 insertions(+), 36 deletions(-) diff --git a/content/blog/03_compiler_typechecking.md b/content/blog/03_compiler_typechecking.md index 49a5620..53e9993 100644 --- a/content/blog/03_compiler_typechecking.md +++ b/content/blog/03_compiler_typechecking.md @@ -159,8 +159,8 @@ the form: \frac{A_1 \ldots A_n} {B_1 \ldots B_m} {{< /latex >}} -This reads, "given that the premises \\(A\_1\\) through \\(A\_n\\) are true, -it holds that the conclusions \\(B\_1\\) through \\(B\_m\\) are true". +This reads, "given that the premises \(A_1\) through \(A_n\) are true, +it holds that the conclusions \(B_1\) through \(B_m\) are true". For example, we can have the following inference rule: @@ -173,18 +173,18 @@ For example, we can have the following inference rule: Since you wear a jacket when it's cold, and it's cold, we can conclude that you will wear a jacket. -When talking about type systems, it's common to represent a type with \\(\\tau\\). +When talking about type systems, it's common to represent a type with \(\tau\). The letter, which is the greek character "tau", is used as a placeholder for some __concrete type__. It's kind of like a template, to be filled in with an actual value. When we plug in an actual value into a rule containing -\\(\\tau\\), we say we are __instantiating__ it. Similarly, we will use -\\(e\\) to serve as a placeholder for an expression (matched by our -\\(A\_{add}\\) grammar rule from part 2). Next, we have the typing relation, -written as \\(e:\\tau\\). This says that "expression \\(e\\) has the type -\\(\\tau\\)". +\(\tau\), we say we are __instantiating__ it. Similarly, we will use +\(e\) to serve as a placeholder for an expression (matched by our +\(A_{add}\) grammar rule from part 2). Next, we have the typing relation, +written as \(e:\tau\). This says that "expression \(e\) has the type +\(\tau\)". Alright, this is enough to get us started with some typing rules. -Let's start with one for numbers. If we define \\(n\\) to mean +Let's start with one for numbers. If we define \(n\) to mean "any expression that is a just a number, like 3, 2, 6, etc.", we can write the typing rule as follows: @@ -206,30 +206,30 @@ Now, let's move on to the rule for function application: This rule includes everything we've said before: the thing being applied has to have a function type -(\\(\\tau\_1 \\rightarrow \\tau\_2\\)), and +(\(\tau_1 \rightarrow \tau_2\)), and the expression the function is applied to -has to have the same type \\(\\tau\_1\\) as the +has to have the same type \(\tau_1\) as the left type of the function. It's the variable rule that forces us to adjust our notation. Our rules don't take into account the context that we've already discussed, and thus, we can't bring in any outside information. Let's fix that! It's convention -to use the symbol \\(\\Gamma\\) for the context. We then -add notation to say, "using the context \\(\\Gamma\\), -we can deduce that \\(e\\) has type \\(\\tau\\)". We will -write this as \\(\\Gamma \\vdash e : \\tau\\). +to use the symbol \(\Gamma\) for the context. We then +add notation to say, "using the context \(\Gamma\), +we can deduce that \(e\) has type \(\tau\)". We will +write this as \(\Gamma \vdash e : \tau\). But what __is__ our context? We can think of it as a mapping from variable names to their known types. We can represent such a mapping using a set of pairs -in the form \\(x : \\tau\\), where \\(x\\) represents +in the form \(x : \tau\), where \(x\) represents a variable name. -Since \\(\\Gamma\\) is just a regular set, we can -write \\(x : \\tau \\in \\Gamma\\), meaning that -in the current context, it is known that \\(x\\) -has the type \\(\\tau\\). +Since \(\Gamma\) is just a regular set, we can +write \(x : \tau \in \Gamma\), meaning that +in the current context, it is known that \(x\) +has the type \(\tau\). Let's update our rules with this new addition. @@ -283,19 +283,19 @@ Let's first take a look at the whole case expression rule: This is a lot more complicated than the other rules we've seen, and we've used some notation that we haven't seen before. Let's take this step by step: -1. \\(e : \\tau\\), in this case, means that the expression between `case` and `of`, is of type \\(\\tau\\). -2. \\(\\text{matcht}(\\tau, p\_i) = b\_i\\) means that the pattern \\(p\_i\\) can match a value of type -\\(\\tau\\), producing additional type pairs \\(b\_i\\). We need \\(b\_i\\) because a pattern -such as `Cons x xs` will introduce new type information, namely \\(\text{x} : \text{Int}\\) and \\(\text{xs} : \text{List}\\). -3. \\(\\Gamma,b\_i \\vdash e\_i : \\tau\_c\\) means that each individual branch can be deduced to have the type -\\(\\tau\_c\\), using the previously existing context \\(\\Gamma\\), with the addition of \\(b\_i\\), the new type information. -4. Finally, the conclusion is that the case expression, if all the premises are met, is of type \\(\\tau\_c\\). +1. \(e : \tau\), in this case, means that the expression between `case` and `of`, is of type \(\tau\). +2. \(\text{matcht}(\tau, p_i) = b_i\) means that the pattern \(p_i\) can match a value of type +\(\tau\), producing additional type pairs \(b_i\). We need \(b_i\) because a pattern +such as `Cons x xs` will introduce new type information, namely \(\text{x} : \text{Int}\) and \(\text{xs} : \text{List}\). +3. \(\Gamma,b_i \vdash e_i : \tau_c\) means that each individual branch can be deduced to have the type +\(\tau_c\), using the previously existing context \(\Gamma\), with the addition of \(b_i\), the new type information. +4. Finally, the conclusion is that the case expression, if all the premises are met, is of type \(\tau_c\). -For completeness, let's add rules for \\(\\text{matcht}(\\tau, p\_i) = b\_i\\). We'll need two: one for +For completeness, let's add rules for \(\text{matcht}(\tau, p_i) = b_i\). We'll need two: one for the "basic" pattern, which always matches the value and binds a variable to it, and one for a constructor pattern, that matches a constructor and its parameters. -Let's define \\(v\\) to be a variable name in the context of a pattern. For the basic pattern: +Let's define \(v\) to be a variable name in the context of a pattern. For the basic pattern: {{< latex >}} \frac @@ -303,7 +303,7 @@ Let's define \\(v\\) to be a variable name in the context of a pattern. For the {\text{matcht}(\tau, v) = \{v : \tau \}} {{< /latex >}} -For the next rule, let's define \\(c\\) to be a constructor name. The rule for the constructor pattern, then, is: +For the next rule, let's define \(c\) to be a constructor name. The rule for the constructor pattern, then, is: {{< latex >}} \frac @@ -312,8 +312,8 @@ For the next rule, let's define \\(c\\) to be a constructor name. The rule for t {{< /latex >}} This rule means that whenever we have a pattern in the form of a constructor applied to -\\(n\\) variable names, if the constructor takes \\(n\\) arguments of types \\(\\tau\_1\\) -through \\(\\tau\_n\\), then the each variable will have a corresponding type. +\(n\) variable names, if the constructor takes \(n\) arguments of types \(\tau_1\) +through \(\tau_n\), then the each variable will have a corresponding type. We didn't include lambda expressions in our syntax, and thus we won't need typing rules for them, so it actually seems like we're done with the first draft of our type rules. @@ -399,8 +399,8 @@ we're binding is the same as the string we're binding it to We now have a unification algorithm, but we still need to implement our rules. Our rules usually include three things: an environment -\\(\\Gamma\\), an expression \\(e\\), -and a type \\(\\tau\\). We will +\(\Gamma\), an expression \(e\), +and a type \(\tau\). We will represent this as a method on `ast`, our struct for an expression tree. This method will take an environment and return @@ -413,7 +413,7 @@ to a type. So naively, we can implement this simply using an `std::map`. But observe that we only extend the environment in one case so far: a case expression. In a case expression, we have the base -envrionment \\(\\Gamma\\), and for each branch, +envrionment \(\Gamma\), and for each branch, we extend it with the bindings produced by the pattern match. Each branch receives a modified copy of the original environment, one that @@ -459,7 +459,7 @@ We start with with a signature inside `ast`: ``` virtual type_ptr typecheck(type_mgr& mgr, const type_env& env) const; ``` -We also implement the \\(\\text{matchp}\\) function +We also implement the \(\text{matchp}\) function as a method `match` on `pattern` with the following signature: ``` virtual void match(type_ptr t, type_mgr& mgr, type_env& env) const;