Add warning about evaluation model.

content/blog/haskell_lazy_evaluation/index.md

@@ -103,6 +103,17 @@ needed to compute the final answer can exist, unsimplified, in the tree.
 Why don't we draw a few graphs to get familiar with the idea?
 
 ### Visualizing Graphs and Their Reduction
+__A word of caution__: the steps presented below may significantly differ
+from the actual graph reduction algorithms used by modern compilers.
+In particular, this section draws a lot of ideas from Simon Peyton Jones' book,
+[_Implementing functional languages: a tutorial_](https://www.microsoft.com/en-us/research/publication/implementing-functional-languages-a-tutorial/).
+However, modern functional compilers (i.e. GHC) use a much more
+complicated abstract machine for evaluating graph-based code,
+based on -- from what I know -- the [spineless tagless G-machine](https://www.microsoft.com/en-us/research/wp-content/uploads/1992/04/spineless-tagless-gmachine.pdf).
+In short, this section, in order to build intuition, walks through how a functional program
+evaluated using graph reduction _may_ behave; the actual details
+depend on the compiler. 
+
 Let's start with something that doesn't have anything fancy. We can
 take a look at the graph of the expression:
 

content/blog/typesafe_interpreter_revisited.md

@@ -361,7 +361,7 @@ I think this is a good approach. Should we want to add more types to our languag
 lists, and so on, we will be able to extend our `decEq` approach to construct more complex equality
 proofs, and keep the `typecheck` method the same. Had we not used this approach,
 and instead decided to pattern match on types inside of `typecheck`, we would've quickly
-found that this only works for types with finitely many values. When we add polymorphic tuples
+found that this only works for languages with finitely many types. When we add polymorphic tuples
 and lists, we start being able to construct an arbitrary number of types: `[a]`. `[[a]]`, and
 so on. Then, we cease to be able to enumerate all possible pairs of types, and require a recursive
 solution. I think that this leads us back to `decEq`.

content/blog/typesafe_interpreter_tuples.md

@@ -1,8 +1,7 @@
 ---
 title: Meaningfully Typechecking a Language in Idris, With Tuples
-date: 2020-08-11T19:57:26-07:00
+date: 2020-08-12T15:48:04-07:00
 tags: ["Idris"]
-draft: true
 ---
 
 Some time ago, I wrote a post titled

themes/vanilla/assets/scss/code.scss

@@ -28,6 +28,7 @@ pre code {
         border: $code-border;
         display: block;
         overflow: auto;
+        margin-bottom: 1rem;
 
         td {
             padding: 0;