content/blog/00_types_intro.md

@@ -1,89 +0,0 @@
----
-title: "Everything I Know About Types: Introduction"
-date: 2022-06-26T18:36:01-07:00
-tags: ["Type Systems", "Programming Languages"]
-draft: true
----
-
-I am in love with types and type systems. They are, quite probably,
-my favorite concept in the world. Most of us mere
-mortals use types as a way to make sure we aren't writing
-bad code - they help us catch things that are certainly wrong,
-such as dividing a string by a number, or calling a method
-on an object that doesn't exist. Types, however, can do
-a lot more than that. In languages with particularly
-powerful type systems, like Idris or Coq, you can prove
-facts about your program, confirming, for instance,
-that a function doesn't loop infinitely and eventually
-returns a result. More generally, some powerful systems
-can be used in place of Zermelo-Frankel set theory as
-foundations for _all of mathematics_. There's a lot of depth to types.
-
-A lot of the fascinating ideas in type systems are contained
-in academic writing, rather than "real-world" programming
-languages. This, unfortunately, makes them harder to access - 
-the field of programming languages isn't exactly known
-for being friendly to newbies. I want to introduce these fascinating
-ideas to you, and I want to prove to you that these ideas are _not_
-"academic autofellatio" -- they have practical use. At the
-same time, I want to give you the tools to explore programming
-languages literature yourself. The notation in the field seemed
-to me to be scary and overwhelming at first, but nowadays my eyes
-go straight to the equations in PL papers. It's not that scary
-once you get used to it, and it really does save a lot of ambiguity.
-
-So I am going to try to opt for a hybrid approach. My aim is to explore
-various ideas in programming languages, starting from the absolute
-basics and working my way up to the limits of what I know. I will
-try to motivate each exploration with examples from the real world,
-using well-known typed languages, perhaps TypeScript, Java, C++, and Haskell.
-At the same time, I will build up the tools to describe type systems
-mathematically, the way it's done in papers.
-
-Before all of that, though, I want to go slightly deeper into the
-motivation behind type systems, and some reasons why I find them
-so interesting.
-
-### The Impossibility of Knowing
-Wouldn't it be nice if there was a programming language that could
-know, always and with complete certainty, if you wrote bad code?
-Maybe it screams at you, like the [skull of regret](https://imgur.com/gallery/vQm8O).
-Forgot to increment a loop counter? _AAAA!_ Flipped the arguments to a function?
-_AAAA!_ Caused an infinite loop? _AAAAAAA!_ No mistake escapes its all-seeing
-eye, and if your code compiles, it's always completely correct. You
-might think that this compiler only exists in your mind, but guess what? You're right.
-
-The reason, broadly speaking, is [Rice's theorem](https://en.wikipedia.org/wiki/Rice%27s_theorem).
-It states that any interesting question about a program's behavior is impossible to answer.
-We can't determine for sure whether or not any program will run infinitely, or if it will
-throw an exception, or do something silly. It's just not possible. We're out of luck.
-
-In software, though, there's a bit of discrepancy between theory and practice. They
-say that computer scientists love dismissing problems as NP-hard, while working
-software engineers write code that, while not fast in the general case, is perfectly
-adequate in the real world. What I'm trying to say is: a theoretical restriction,
-no matter how stringent, shouldn't stop us from trying to find something "good enough in practice".
-
-This is where types come in. They are decidedly not magic - you can't do anything
-with a type system that violates Rice's theorem. And yet, modern type systems
-can reject a huge number of incorrect programs, and at the same time allow
-most "correct-looking" programs through. They can't eliminate _all_ errors,
-but they can eliminate _a lot_ of them.
-
-Moreover, this sort of checking is _cheap_. For example, [Algorithm J](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Algorithm_J),
-which is used to typecheck polymorphic functional programs, has a "close to linear"
-complexity in terms of program size. This is a huge jump, taking us from "undecidable" to
-"efficient". Once again, approximations prevail. What we have is a fast and
-practical way of catching our mistakes.
-
-### Types for Documentation and Thought
-To me, type systems aren't only about checking if your program is correct;
-they're also about documentation. This way of viewing programs comes to
-me from experience with Haskell. In Haskell, the compiler is usually able to
-check your program without you ever having to write down any types. You
-can write your programs, like `length xs + sum xs`, feel assured that what
-you wrote isn't complete nonsense. And yet, most Haskell programmers
-(myself included) _do_ write the types for all of their functions, by hand.
-How come?
-
-The answer is that types can tell you what your code does.

content/blog/10_compiler_polymorphism.md

@@ -58,7 +58,7 @@ __generalization__ and __instantiation__. It's been quite a while since the last
 to present a table with these new rules, as well as all of the ones that we
 {{< sidenote "right" "rules-note" "previously used." >}}
 The rules aren't quite the same as the ones we used earlier;
-note that \\(\sigma\\) is used in place of \\(\tau\\) in the first rule,
+note that \(\sigma\) is used in place of \(\tau\) in the first rule,
 for instance. These changes are slight, and we'll talk about how the
 rules work together below.
 {{< /sidenote >}} I will also give a quick