Alternative to Type Systems - Draft

This page is a Draft

This page is about Clojure, a dynamically typed language that I don't hate to work in. How could that be?

I'll be talking about 2 things Clojure has: a library called Spec, and the REPL.

REPL

Clojure is a Lisp, and Lisps have a unique runtime model. Rather than being compiled in one big step, a binary being spat out, and you running that, Lisp code is loaded piecemeal. Clojure code is made of forms, like (def x 42), or (println "Hello, Internet"). These forms are read in, then they're evaluated, they return a result, that result is printed, and then the process repeats (in a loop!).

Quite importantly, this can happen whenever, not just at startup. You can re-evaluate half your program while its running and make it do new things!

These forms aren't even compiled at all when you evaluate them. Why would they be, just call the println function or define the variable directly. More sophisticated things will compiled, but these can just be run immediately.

The whole "catch things at compiletime" is kind of a moot point in Lisp, because Lisp doesn't have a compiltime. Even if you ahead-of-time compile the whole program before running it, you're actually just running the whole program and compiling it at the same time (things like your main function won't be invoked, but everything else will!).

Want to test if something works? Just evaluate it.

But what if you want to catch errors that are trivial to statically analyze, and you can't even wait to hit one keybinding in your editor to run it! Linters can catch most of these errors anyway, because type checkers don't do anything that any other static analysis tool couldn't... because they're just static analysis tools. The difference is that in Clojure, functions don't have "correct types" to pass, they take data of any type. For code with type hints though, for calls to Java, or for calls to functions that have an obvious type (like +), linters can catch these problems.

There is one hitch, and that's that there's a form for storing code without evaluating it: fn. (fn [] (+ 1 true)) stores code with a type error to be run later. Here, the function needs to be compiled so that it can be efficiently run later, and + doesn't check the static type of its arguments, so this call will compile just fine.

Okay, well, the linter will also catch that. Lets do (fn [] (+ 1 (read-string "true"))). read-string can return anything, and + only works on numbers. Of course a statically typed language wouldn't let you compile this, you'd have to cast the result to Number... Which is exactly what + does anyway when you call it, but ignoring all that, this code will compile and it will fail when its run!

Well, of course, you could just put another set of parens around this function and call it and see that it won't work, so lets make a scenario where that's not possible:

(def maybe-fine-function
  (fn [arg1]
    (+ 1 (read-string arg1)))

Here we go, now we truly have no idea whether this code will work because it depends on input that we don't have yet. Now we would have to run the function to test it out! Fortunately, this is also possible.

We even have a system in programming to call functions with all kinds of stuff, and ensure that they return the results that we expect them to, which is testing. Testing is another way to do this same thing. Call code, see what it does.

That's cool but also all extremely obvious. My point is that working in the REPL is actually smoother than writing code in statically typed languages, as you will get told off faster. I don't think most people like writing tests, and these systems both try to improve this.

So if you can just run code, what does static typing give you?

I think:

• Data modeling
• Documentation
• Assurance

There are these other things as well:

• Performance, though JITs mean dynamic languages can have equal or better performance than static ones. Hotspot is insane. In environments with constrained memory, you'd have to trade compute for this. CPUs will also predict branches for you, but you might lose out elsewhere.
• Autocomplete, go-to-definition, etc., dynamic languages can do all of this just fine, I'll talk a little bit more about that later
• Abstraction is less real as it is still dependent on discipline. Most statically typed languages let you make named/identifiable implementations of abstractions, which you have to make sure don't leak anywhere. If you keep the implementation private, you don't have this problem, but of course you don't need types to do that.
• Data modeling, this is really just a language thing independent of static types, but you you often find data modeling coupled with static types. It can be fully independent though as you'll see with Spec.
• Formal verification, but this that's outside the scope of what I do
• Refactoring (I will talk about this later)

Spec

Beyond this, Clojure has tools for validating.

Clojure doesn't use slotted data¹, we use hashmaps. This means you have to check whether keys are there when you're using a map.

In practice, you can just return a garbage result, or call into a function that will throw when you give it your bad data, and just leave validation to the top level.

Spec is quite good at this. You can create a spec for data, and validate against it. You can take any spec and generate 500 values that conform to that spec, pass them to your functions, and test that they do what you expect them to!

Or just:

(defn foo [{::keys! [x y z]}])

foo will then throw if it isn't passed a map with ::x ::y and ::z as keys.

More trivial static analysis, you can find references of those keys, and even go to definition if you (s/def ::x ...) somewhere. That also means you can rename them!

Data modeling

Clojure is extremely good at this

• Spec, functions, etc.

Documentation

Same thing, both keys! and full on specs describe the shape of data and what kind of data functions take.

Assurance

I would like to rename this bullet point to "False assurance". We're in computer science, not computer mathematics. Well some of us are in computer mathematics, but most of us aren't. I wouldn't argue against typing as a means of formal verification, because I don't know anything about it.

The wonderful https://zipsegv.net said something online that gave me a chuckle, it was along the lines of "If you had a giant vat of acid, wouldn't you put a guard rail around it?". I get the premise here, but this is really what static typing feels like to me lol. I'm glad its proven that if I try to walk into the vat of acid its not going to work, but like... No! What!? I would put an impenetrable wall around the vat of acid, and guard the door that locks it! I'd only allow trusted people in that room, and only let them go in if they had a proper reason! I'd surveil it 24/7 to make sure nobody went near it, I'd perform regular security checks to make sure it wasn't being accessed, I'd make mandatory training for everyone who works in the same building, I'd put up signs warning people "DO NOT GO NEAR, THERE IS A GIANT VAT OF ACID AND IF YOU FALL INTO IT YOU WILL DIE"! I'd move as much of my stuff away from it and into a safer part of the building as I could! I'm not a nuclear engineer, I don't know what safety measures go into that kinda stuff, but I'm damn sure its not a guard rail!

If you'd say that seems completely unrelated to whether there's a guardrail there or not, I'd say yeah! It is! If someone said "yep, we have a guardrail, our acid vat is proven to be secure", I would run the other way! If you can't do all those things I said, then I'd say you shouldn't be synthesizing vat-quantities of acid. And nobody's going to make sure you're doing things right. I do hope there are laws around nuclear power plants, but there aren't laws around software like this yet. Not until someone falls into the acid and dies a gruesome death and the world takes notice.