A type system is good when it not only guardrails you from doing the wrong thing, but reminds you to do the right thing. A type system is excellent when it guides you toward doing the right thing without you having to tell it what you wanted.
Here are some examples of type systems I like and love:
Java: It's very hard to compile any Java at all. Because it's so strict about the types. If someone gives you a PayPal API JAR, you plug it in and say "oh, this #pay method takes a Recipient, an Amount, and a Details object. I better fill those in." If you don't provide exactly those three, you don't get to pay anyone.
C#: Instead of having to type out Map<String, Integer> recipients = new HashMap<>() like in Java, you can just let recipients, much like auto in C++. Inferring your type at creation is great. Less typing, I can already tell what the thing is.
JS Flow: JavaScript is the loosest (baylor inserts joke here) language known to man, besides maybe Lisp. See the wat talk. 1 Facebook engineers discovered it was such garbage that many of their dev hours were spent debugging type errors at runtime that weren't type errors at compile time. Like, you tried to add two strings, and you traced it up through fourteen different classes that managed to add "16" and 42 and resulted in "1642". Flow looks at the garbage code I wrote and tells me what I can do with it. For example:
function doTaxes(amount, rate) { submitToIrs("matt", amount * rate + processing_fee) }
In that example, I'm multiplying amount with rate and processing_fee. That means they're all numbers, and that means doTaxes takes two arguments, both of which are numbers. If I ever use "doTaxes" with a string, ANYWHERE in my program, it will infer that something's wrong. And I didn't write a single type! It's fixing my shit without me telling it what's wrong.
OCaml: Flow was built out of OCaml, an ungodly-fast language for everything it does. It compiles fast and it has an incredibly strict but stupid easy type system. Here's an example of how OCaml made my day:
I said "hey, I have a list of numbers, and I want you to turn the first N into a string." So I wrote these commands (pseudocode): function stringify(stuff, count): stuff -> List.take(count) -> List.map(string_of_int) -> String.join(",")
Here are its rules:
- all input and output types must match up
- string_of_int only works on strings, and it outputs ints
- all lists are made up of exactly ONE type of thing, no more
So, it now knows:
- Function returns a string, because
- String.join operates on a list of strings, and
- List.map(string_of_int) only works on a list of ints, and
- List.take(count) takes a number, works on any list and returns a list of the same type, and so
- stuff MUST be a list of strings, and count MUST be an int!
I typed NO types there, yet that program figured out exactly what I intended. If I used string_of_float, it'd know I meant a list of floats, not ints.
Type systems are at their peak strength when they not only prevent your errors, but infer your uses and empower you to write correct code quickly. If you get a chance, try one of these out. They're really fun.