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

Update "compiler: typechecking" to new math delimiters

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-13 18:33:30 -07:00
parent 6ef5ae2394
commit 96545a899f
1 changed files with 36 additions and 36 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

72
content/blog/03_compiler_typechecking.md
View File

@ -159,8 +159,8 @@ the form:
\frac{A_1 \ldots A_n} {B_1 \ldots B_m} \frac{A_1 \ldots A_n} {B_1 \ldots B_m}
{{< /latex >}} {{< /latex >}}
This reads, "given that the premises \\(A\_1\\) through \\(A\_n\\) 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". it holds that the conclusions \(B_1\) through \(B_m\) are true".
For example, we can have the following inference rule: 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 Since you wear a jacket when it's cold, and it's cold, we can conclude
that you will wear a jacket. 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 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 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 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 \(\tau\), we say we are __instantiating__ it. Similarly, we will use
\\(e\\) to serve as a placeholder for an expression (matched by our \(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, \(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 written as \(e:\tau\). This says that "expression \(e\) has the type
\\(\\tau\\)". \(\tau\)".
Alright, this is enough to get us started with some typing rules. 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.", "any expression that is a just a number, like 3, 2, 6, etc.",
we can write the typing rule as follows: 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: This rule includes everything we've said before:
the thing being applied has to have a function type 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 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. left type of the function.
It's the variable rule that forces us to adjust our notation. It's the variable rule that forces us to adjust our notation.
Our rules don't take into account the context that we've Our rules don't take into account the context that we've
already discussed, and thus, we can't bring already discussed, and thus, we can't bring
in any outside information. Let's fix that! It's convention in any outside information. Let's fix that! It's convention
to use the symbol \\(\\Gamma\\) for the context. We then to use the symbol \(\Gamma\) for the context. We then
add notation to say, "using the context \\(\\Gamma\\), add notation to say, "using the context \(\Gamma\),
we can deduce that \\(e\\) has type \\(\\tau\\)". We will we can deduce that \(e\) has type \(\tau\)". We will
write this as \\(\\Gamma \\vdash e : \\tau\\). write this as \(\Gamma \vdash e : \tau\).
But what __is__ our context? We can think of it But what __is__ our context? We can think of it
as a mapping from variable names to their known types. We as a mapping from variable names to their known types. We
can represent such a mapping using a set of pairs 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. a variable name.
Since \\(\\Gamma\\) is just a regular set, we can Since \(\Gamma\) is just a regular set, we can
write \\(x : \\tau \\in \\Gamma\\), meaning that write \(x : \tau \in \Gamma\), meaning that
in the current context, it is known that \\(x\\) in the current context, it is known that \(x\)
has the type \\(\\tau\\). has the type \(\tau\).
Let's update our rules with this new addition. 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 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: 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\\). 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 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 \(\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}\\). 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 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. \(\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\\). 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 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. 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 >}} {{< latex >}}
\frac \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 \}} {\text{matcht}(\tau, v) = \{v : \tau \}}
{{< /latex >}} {{< /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 >}} {{< latex >}}
\frac \frac
@ -312,8 +312,8 @@ For the next rule, let's define \\(c\\) to be a constructor name. The rule for t
{{< /latex >}} {{< /latex >}}
This rule means that whenever we have a pattern in the form of a constructor applied to 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\\) \(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. 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, 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. 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 We now have a unification algorithm, but we still
need to implement our rules. Our rules need to implement our rules. Our rules
usually include three things: an environment usually include three things: an environment
\\(\\Gamma\\), an expression \\(e\\), \(\Gamma\), an expression \(e\),
and a type \\(\\tau\\). We will and a type \(\tau\). We will
represent this as a method on `ast`, our struct represent this as a method on `ast`, our struct
for an expression tree. This for an expression tree. This
method will take an environment and return 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 using an `std::map`. But observe
that we only extend the environment in one case so far: that we only extend the environment in one case so far:
a case expression. In a case expression, we have the base 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 we extend it with the bindings produced by
the pattern match. Each branch receives a modified the pattern match. Each branch receives a modified
copy of the original environment, one that 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; 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: as a method `match` on `pattern` with the following signature:
``` ```
virtual void match(type_ptr t, type_mgr& mgr, type_env& env) const; virtual void match(type_ptr t, type_mgr& mgr, type_env& env) const;