---
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.