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

Start working on explanations in Part 10 of Compiler series

Browse Source
This commit is contained in:
Danila Fedorin 2020-03-06 17:54:22 -08:00
parent 79ef221820
commit d8d1aa66e6
1 changed files with 13 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
content/blog/10_compiler_polymorphism.md
View File

@ -87,3 +87,16 @@ Rule|Name and Description
{\Gamma \vdash e : \sigma \quad \alpha \not \in \text{free}(\Gamma)} {\Gamma \vdash e : \sigma \quad \alpha \not \in \text{free}(\Gamma)}
{\Gamma \vdash e : \forall \alpha . \sigma} {\Gamma \vdash e : \forall \alpha . \sigma}
{{< /latex >}}| __Gen (New)__: If an expression has a type with free variables, this rule allows us generalize it to allow all possible types to be used for these free variables. {{< /latex >}}| __Gen (New)__: If an expression has a type with free variables, this rule allows us generalize it to allow all possible types to be used for these free variables.
Here, there is a distinction between different forms of types. First, there are
monomorphic types, or __monotypes__, \\(\\tau\\), which are types such as \\(\\text{Int}\\),
\\(\\text{Int} \\rightarrow \\text{Bool}\\), \\(a \\rightarrow b\\)
and so on. These types are what we've been working with so far. Each of them
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\\)"...