From 8e550dc982e731c3fdab270313ce7474d4f0b000 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 27 Jun 2022 19:38:58 -0700 Subject: [PATCH] Start working on types series? --- content/blog/00_types_intro.md | 89 ++++++++++++++++++++++++++++++++++ 1 file changed, 89 insertions(+) create mode 100644 content/blog/00_types_intro.md diff --git a/content/blog/00_types_intro.md b/content/blog/00_types_intro.md new file mode 100644 index 0000000..d4ba237 --- /dev/null +++ b/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.