diff --git a/content/blog/10_compiler_polymorphism.md b/content/blog/10_compiler_polymorphism.md index 01ef7ef..d52a709 100644 --- a/content/blog/10_compiler_polymorphism.md +++ b/content/blog/10_compiler_polymorphism.md @@ -55,9 +55,34 @@ summary of each of these rules. Rule|Name and Description -----|------- -$$\\frac{x:\\sigma \\in \\Gamma}{\\Gamma \\vdash x:\\sigma}$$| __Var__: If the variable \$$x\$$ is known to have some polymorphic type \$$\\sigma\$$ then an expression consisting only of that variable is of that type. -$$\\frac{\\Gamma \\vdash e\_1 : \\tau\_1 \\rightarrow \\tau\_2 \\quad \\Gamma \\vdash e\_2 : \\tau\_1}{\\Gamma \\vdash e\_1 \\; e\_2 : \\tau\_2}$$| __App__: If an expression \$$e\_1\$$, which is a function from monomorphic type \$$\\tau\_1\$$ to another monomorphic type \$$\\tau\_2\$$, is applied to an argument \$$e\_2\$$ of type \$$\\tau\_1\$$, then the result is of type \$$\\tau\_2\$$. -$$\\frac{\\Gamma, x:\\tau \\vdash e : \\tau'}{\\Gamma \\vdash \\lambda x.e : \\tau \\rightarrow \\tau'}$$| __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'\$$. -$$\\frac{\\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 }$$ | __Case__: This rule is not part of Hindley-Milner, and is specific to our language. If the expression being case-analyzed is of type \$$\\tau\$$ and each branch \$$(p\_i, e\_i)\$$ is of the same type \$$\\tau\_c\$$ when the pattern \$$p\_i\$$ works with type \$$\\tau\$$ producing extra bindings \$$b\_i\$$, the whole case expression is of type \$$\\tau\_c\$$. -$$\\frac{\\Gamma \\vdash e : \\sigma \\quad \\sigma' \\sqsubseteq \\sigma}{\\Gamma \\vdash e : \\sigma'}$$| __Inst (New)__: If type \$$\\sigma'\$$ is an instantiation of type \$$\\sigma\$$ then an expression of type \$$\\sigma\$$ is also an expression of type \$$\\sigma'\$$. -$$\\frac{\\Gamma \\vdash e : \\sigma \\quad \\alpha \\not \\in \\text{free}(\\Gamma)}{\\Gamma \\vdash e : \\forall a . \\sigma}$$| __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 >}} +\frac + {x:\sigma \in \Gamma} + {\Gamma \vdash x:\sigma} +{{< /latex >}}| __Var__: If the variable \$$x\$$ is known to have some polymorphic type \$$\\sigma\$$ then an expression consisting only of that variable is of that type. +{{< latex >}} +\frac + {\Gamma \vdash e_1 : \tau_1 \rightarrow \tau_2 \quad \Gamma \vdash e_2 : \tau_1} + {\Gamma \vdash e_1 \; e_2 : \tau_2} +{{< /latex >}}| __App__: If an expression \$$e\_1\$$, which is a function from monomorphic type \$$\\tau\_1\$$ to another monomorphic type \$$\\tau\_2\$$, is applied to an argument \$$e\_2\$$ of type \$$\\tau\_1\$$, then the result is of type \$$\\tau\_2\$$. +{{< latex >}} +\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 >}} +\frac + {\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 } +{{< /latex >}}| __Case__: This rule is not part of Hindley-Milner, and is specific to our language. If the expression being case-analyzed is of type \$$\\tau\$$ and each branch \$$(p\_i, e\_i)\$$ is of the same type \$$\\tau\_c\$$ when the pattern \$$p\_i\$$ works with type \$$\\tau\$$ producing extra bindings \$$b\_i\$$, the whole case expression is of type \$$\\tau\_c\$$. +{{< 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 >}} +\frac + {\Gamma \vdash e : \sigma \quad \alpha \not \in \text{free}(\Gamma)} + {\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. diff --git a/themes/vanilla/layouts/shortcodes/latex.html b/themes/vanilla/layouts/shortcodes/latex.html new file mode 100644 index 0000000..c2a7716 --- /dev/null +++ b/themes/vanilla/layouts/shortcodes/latex.html @@ -0,0 +1,3 @@ +$$+{{ .Inner }} +$$