Update type rules, get pattern matching defined

This commit is contained in:
Danila Fedorin 2019-08-25 01:37:24 -07:00
parent 0d275844d4
commit ac589a8b0a

View File

@ -240,7 +240,7 @@ that These rules leave out the process
of unification altogether: we use unification to find
types that satisfy the rules.
#### Checking More Expressions
#### Checking Case Expressions
So far, we've only checked types of numbers, applications, and variables.
Our language has more than that, though!
@ -254,24 +254,23 @@ where we will introduce new variables into the context, and
also a place where we will need several rules.
Let's first take a look at the whole case expression rule:
{{< todo >}} Double check squiggly notation. {{< /todo >}}
$$
\\frac
{\\Gamma \\vdash e : \\tau \\quad \\tau | p\_i \\leadsto b\_i \\quad \\Gamma,b\_i \\vdash e\_i : \\tau\_c}
{\\Gamma \\vdash e : \\tau \\quad \\text{matcht}(\\tau, p\_i) = b\_i \\quad \\Gamma,b\_i \\vdash e\_i : \\tau\_c}
{\\Gamma \\vdash \\text{case} \\; e \\; \\text{of} \; \\\{ (p\_1,e\_1) \\ldots (p\_n, e\_n) \\\} : \\tau\_c }
$$
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. \\(\\tau | p\_i \\leadsto 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
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 \\(\\tau | p\_i \\leadsto 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 it to the variable, and one
for a constructor pattern, that matches a constructor and its parameters.
@ -279,13 +278,21 @@ Let's define \\(v\\) to be a variable name in the context of a pattern. For the
$$
\\frac
{}
{\\tau | v \\leadsto \\\{v : \\tau \\\}}
{\\text{matcht}(\\tau, v) = \\\{v : \\tau \\\}}
$$
{{< todo >}} consult pierce. {{< /todo >}}
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:
$$
\\frac
{}
{}
{\\Gamma \\vdash c : \\tau\_1 \\rightarrow ... \\rightarrow \\tau\_n \\rightarrow \\tau}
{\\text{matcht}(\\tau, c \; v\_1 ... v\_n) = \\{ v\_1 : \\tau\_1, ..., v\_n : \\tau\_n \\}}
$$
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.
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.
{{< todo >}}Cite 006_hindley_milner on implementation of bind. {{< /todo >}}.