Add more content to part 12 of compiler series

content/blog/12_compiler_let_in_lambda/index.md

@@ -81,5 +81,21 @@ polymorphic__. Remember the note in
 [let-polymorphism](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Let-polymorphism)? This is it: we're allowing polymorphic variable bindings,
 but only when they're bound in a `let/in` expression (or at the top level).
 
-The principles demonstrated by the last two snippets mean that compiling `let/in`
+The principles demonstrated by the last two snippets mean that compiling `let/in` expressions, at least with the power we want to give them, will require the same kind of dependency analysis we had to go through when we implemented polymorphically typed functions. That is, we will need to analyze which functions calls which other functions, and typecheck the callees before the callers. We will continue to represent callee-caller relationships using a dependency graph, in which nodes represent functions, and an edge from one function node to another means that the former function calls the latter. Below is an image of one such graph:
-expressions, at least with the power we want to give them 
+
+{{< figure src="fig_graph.png" caption="Example dependency graph without `let/in` expressions." >}}
+
+Since we want to typecheck callees first, we effectively want to traverse the graph in reverse
+topological order. However, there's a slight issue: a topological order is only defined for acyclic graphs, and it is very possible for functions in our language to mutually call each other. To deal with this, we have to find groups of mutually recursive functions, and and treat them as a single unit, thereby eliminating cycles. In the above graph, there are two groups, as follows:
+
+{{< figure src="fig_colored_ordered.png" caption="Previous depndency graph with mutually recursive groups highlighted." >}}
+
+As seen in the second image, according to the reverse topological order of the given graph, we will typecheck the blue group containing three functions first, since the sole function in the orange group calls one of the blue functions.
+
+Things are more complicated now that `let/in` expressions are able to introduce their own, polymorphic and recursive declarations. However, there is a single invariant we can establish: function definitions can only depend on functions defined at the same time as them. That is, for our purposes, functions declared in the global scope can only depend on other functions declared in the global scope, and functions declared in a `let/in` expression can only depend on other functions declared in that same expression. That's not to say that a function declared in a `let/in` block inside some function `f` can't call another globally declared function `g` - rather, we allow this, but treat the situation as though `f` depends on `g`. In contrast, it's not at all possible for a global function to depend on a local function, because bindings created in a `let/in` expression do not escape the expression itself. This invariant tells us that in the presence of nested function definitions, the situation looks like this:
+
+{{< figure src="fig_subgraphs.png" caption="Previous depndency graph augmented with `let/in` subgraphs." >}}
+
+In the above image, some of the original nodes in our graph now contain other, smaller graphs. Those subgraphs are the graphs created by function declarations in `let/in` expressions. Just like our top-level nodes, the nodes of these smaller graphs can depend on other nodes, and even form cycles. Within each subgraph, we will have to perform the same kind of cycle detection, resulting in something like this:
+
+{{< figure src="fig_subgraphs_colored_all.png" caption="Augmented dependency graph with mutually recursive groups highlighted." >}}