.drone.yml

@@ -9,14 +9,3 @@ steps:
     - pacman -Sy cmake gcc make llvm bison flex gettext --noconfirm
     - cd code/compiler
     - ./test.sh
-  - name: upload-live
-    image: jguyomard/hugo-builder
-    commands:
-    - echo "$CUSTOM_KEY" | ssh-add -
-    - mkdir -p ~/.ssh
-    - echo -e "Host *\n\tStrictHostKeyChecking no\n\n" > ~/.ssh/config
-    - hugo -D --baseUrl "http://danilafe.com:8080"
-    - rsync -rv -e "ssh -p 22" ./public blog-live@danilafe.com:/var/www/blog-live --checksum
-    environment:
-      CUSTOM_KEY:
-        from_secret: live_ssh_key

content/blog/10_compiler_polymorphism.md

@@ -1,11 +1,11 @@
 ---
 title: Compiling a Functional Language Using C++, Part 10 - Polymorphism
-date: 2020-02-29T20:09:37-08:00
+date: 2019-12-09T23:26:46-08:00
 tags: ["C and C++", "Functional Languages", "Compilers"]
 draft: true
 ---
 
-[In part 8]({{< relref "08_compiler_llvm.md" >}}), we wrote some pretty interesting programs in our little language.
+Last time, we wrote some pretty interesting programs in our little language.
 We successfully expressed arithmetic and recursion. But there's one thing
 that we cannot express in our language without further changes: an `if` statement.
 
@@ -49,40 +49,17 @@ set of rules to describe our program's types. One such set of rules is
 the [Hindley-Milner type system](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system),
 which we have previously alluded to. In fact, the rules we came up
 with were already very close to Hindley-Milner, with the exception of two:
-__generalization__ and __instantiation__. It's been quite a while since the last time we worked on typechecking, so I'm going
+__generalization__ and __instantiation__. Instantiation first:
-to present a table with these new rules, as well as all of the ones that we previously used. I will also give a quick
-summary of each of these rules.
 
-Rule|Name and Description
+$$
------|-------
-{{< latex >}}
 \frac
-    {x:\sigma \in \Gamma}
+{\\Gamma \\vdash e : \\sigma \\quad \\sigma' \\sqsubseteq \\sigma}
-    {\Gamma \vdash x:\sigma}
+{\\Gamma \\vdash e : \\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 >}}
+
+Next, generalization:
+$$
 \frac
-    {\Gamma \vdash e_1 : \tau_1 \rightarrow \tau_2 \quad \Gamma \vdash e_2 : \tau_1}
+{\\Gamma \\vdash e : \\sigma \\quad \\alpha \\not \\in \\text{free}(\\Gamma)}
-    {\Gamma \vdash e_1 \; e_2 : \tau_2}
+{\\Gamma \\vdash e : \\forall a . \\sigma}
-{{< /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.

themes/vanilla/assets/scss/style.scss

@@ -149,13 +149,3 @@ a {
 img {
   max-width: 100%
 }
-
-table {
-    @include bordered-block;
-    margin: auto;
-    padding: 0.5rem;
-}
-
-td {
-    padding: 0.5rem;
-}

themes/vanilla/layouts/shortcodes/latex.html

@@ -1,3 +0,0 @@
-$$
-{{ .Inner }}
-$$