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

Add some more text to polymorphism post
All checks were successful
continuous-integration/drone/push Build is passing
Details

Browse Source
This commit is contained in:
Danila Fedorin 2020-03-09 22:30:27 -07:00
parent 1abc13b20f
commit 45bc113e3f
1 changed files with 21 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
content/blog/10_compiler_polymorphism.md
View File

@ -37,11 +37,11 @@ This is because, for this to work, both of the following would need to hold (bor
some of our notation from the [typechecking]({{< relref "03_compiler_typechecking.md" >}}) post):
{{< latex >}}
\text{if} : \text{Int} \rightarrow \text{Int}
\text{if} : \text{Bool} \rightarrow \text{Int} \rightarrow \text{Int} \rightarrow \text{Int}
{{< /latex >}}
{{< latex >}}
\text{if} : \text{Bool} \rightarrow \text{Bool}
\text{if} : \text{Bool} \rightarrow \text{Bool} \rightarrow \text{Bool} \rightarrow \text{Bool}
{{< /latex >}}
But using our rules so far, such a thing is impossible, since there is no way for
@ -70,7 +70,7 @@ Rule|Name and Description
\frac
{\Gamma, x:\tau \vdash e : \tau'}
{\Gamma \vdash \lambda x.e : \tau \rightarrow \tau'}
{{< /latex >}}| __Abs__: If the body \\(e\\) of a lambda abstraction \\(\\lambda x.e\\) is of type \\(\\tau'\\) when \\(x\\) is of type \\(\\tau\\) then the whole lambda abstraction is of type \\(\\tau \\rightarrow \\tau'\\).
{{< /latex >}}| __Abs__: If the body \\(e\\) of a lambda abstraction \\(\\lambda x.e\\) is of type \\(\\tau\'\\) when \\(x\\) is of type \\(\\tau\\) then the whole lambda abstraction is of type \\(\\tau \\rightarrow \\tau\'\\).
{{< latex >}}
\frac
{\Gamma \vdash e : \tau \quad \text{matcht}(\tau, p_i) = b_i
@ -81,7 +81,7 @@ Rule|Name and Description
{{< latex >}}
\frac{\Gamma \vdash e : \sigma \quad \sigma' \sqsubseteq \sigma}
{\Gamma \vdash e : \sigma'}
{{< /latex >}}| __Inst (New)__: If type \\(\\sigma'\\) is an instantiation of type \\(\\sigma\\) then an expression of type \\(\\sigma\\) is also an expression of type \\(\\sigma'\\).
{{< /latex >}}| __Inst (New)__: If type \\(\\sigma\'\\) is an instantiation of type \\(\\sigma\\) then an expression of type \\(\\sigma\\) is also an expression of type \\(\\sigma\'\\).
{{< latex >}}
\frac
{\Gamma \vdash e : \sigma \quad \alpha \not \in \text{free}(\Gamma)}
@ -96,7 +96,20 @@ represents one (hence, "mono-"), concrete type. This is obvious in the case
of \\(\\text{Int}\\) and \\(\\text{Int} \\rightarrow \\text{Bool}\\), but
for \\(a \\rightarrow b\\) things are slightly less clear. Does it really
represent a single type, if we can put an arbtirary thing for \\(a\\)?
The answer is "no". The way it is right now, \\(a\\) is still an
unknown, yet concrete thing. Once we find \\(a\\) and put it in,
that's it. If only there was a way to say, "this is the type
for any \\(a\\)"...
The answer is "yes"! Although \\(a\\) is not currently known, it stands
in place of another monotype, which is yet to be determined.
So, how do we represent polymorphic types, like that of \\(\\text{if}\\)?
We borrow some more notation from mathematics, and use the "forall" quantifier:
{{< latex >}}
\text{if} : \forall a \; . \; \text{Bool} \rightarrow a \rightarrow a \rightarrow a
{{< /latex >}}
This basically says, "the type of \\(\\text{if}\\) is \\(\\text{Bool} \\rightarrow a \\rightarrow a \\rightarrow a\\)
for all possible \\(a\\)". This new expression using "forall" is what we call a type scheme, or a polytype \\(\\sigma\\).
For simplicity, we only allow "forall" to be at the front of a polytype. That is, expressions like
\\(a \\rightarrow \\forall b \\; . \\; b \\rightarrow b\\) are not valid polytypes as far as we're concerned.
It's key to observe that the majority of the typing rules in the above table use monotypes (\\(\\tau\\)). Only
two rules seem to mention \\(\\sigma\\): __Inst__ and __Gen__.