Start working on types series?

content/blog/00_types_intro.md

@@ -0,0 +1,89 @@
+---
+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