Strong Types, Weak Types

Strong Types

When I'm using a language like Rust, Haskell or ML, my conversation with the computer is honestly frustrating. It feels a lot like talking to that brilliant friend who always has a leg up on you, but in an intimidating rather than an accessible way; the system you're talking to has all the answers, and though you're not reasonably expected to hold your understanding of all of them in your head, you're expected to accomodate them when the computer uses those rules to validate your work. You're talking to someone who knows all the rules, and - especially when learning - you only know some of them. The computer screams at you when your impression of the rules doesn't align with theirs, even if you weren't informed of those rules beforehand, so you're prevented from trying things out before you can learn why those decisions are poor.

The pain of this experience is multiplied when using interactive theorem provers based on type theory, like Lean or Coq. Suddenly you have this arcane system of dependent typing rules, and you're to defeat them using a series of tactics - macros for proof strategies obscuring their details, their thoughts and feelings.

These perspectives have their places. If I'm working on a large system with multiple people, I'll never be able to hold the whole program, with all of its rules and conventions and idiosyncracies, in my brain, and having the system provide me all of these arcane error messages at runtime is a terrible experience; I can't possibly debug and derive all of the work that my coworkers have constructed.

This is precisely why management structures often administer practices at scale; just like some procedure like lean six sigma or something, types allow us to apply structure to the code, administering rules that impact the way that others are able to interact with the code. In this way, types allow us to facilitate conversations with one another in a way prose can't; if I don't follow the rules of a Haskell program, the system will tell me, reminding me that this type is maintaining this rule in this position and that I must follow it or the system won't even accept my work. Comments can't provide this level of interactivity - no matter how much prose I write, nothing but a type will allow the computer to tell someone else that they aren't following the rules I've put in place when I left the codebase.

Once you understand the rules, there is ideally this feeling of immersion with your computer - you're telling it exactly what it wants as the model living in your brain molds perfectly to the model projected by the machine, and you update your model seamlessly as you absorb more and more of the codebase isnto your mind. The complexity and ruleset is entirely captured in the types and invariants of the system.

Unfortunately, to get to this point requires a significant amount of effort and labor - it's really difficult to learn to understand the rules of an incredibly complex system! - and up until, and even when you've reached that point and have to pursue some update, you can continue to run into new rulesets that you have to update your priors with; changing the world you have to navigate and understand as you integrate the code of others, whether libraries or new parts of the codebase. High school debate, with its thinly veiled ad homenim attacks and strawman arguments and strangely radical frameworks, was less frustrating than navigating the intricacies of many a Haskell library.

Weak Types, Free Types

In stark contrast to the discipline of types, lisp has no rules. You can tell the computer what you want, no matter how crazy, and it'll just happen. Write some parentheses, pass some functions as arguments, construct something at the nth level of abstraction and it'll be callable five functions down the stack without having to accomodate or constrain it with any system of types.

Lisp and C (through Zig, my chosen successor to the language) both feel this way, but on different axes. Lisp has an incredibly simple ruleset through which you can do anything. Common Lisp has been stable for fourty years (before Linux!), has trivial compatibility with C libraries and native code, and can do anything at any level of abstraction; you don't have to think about

This feels a bit like perfecting a home-cooked meal. The recipe goes out the window, the rules are completely arbitrary, and you're throwing spices into the mix as you go - "let's try some coriander! how about using caar instead of caddr here?" - as you have a natural conversation with your tool; no constraints, just you and your craft.

There is almost this feeling of immersion with your computer

close

Ultimately, one feels adversarial while the other feels generative; programming against a strongly typed system feels like an argument where you can blame their rules or blame yourself, while programming in a lisp runs you into errors that are entirely of your own design. The former allows you to utilize a system, constructing a debate in which you compromise your model of the world with theirs until you meld into some system amenable to both ideas. The latter leaves you no such framework; it's entirely up to you to set up the guardrails, establish the framework, and set up the principles under which we construct our programming environment and world, and as such the fault is only with the model you've constructed yourself when things break down. Holding and owning this complete model is such a beautiful thing.

talking

Programming is a conversation, and when you speak to your computer and language and libraries you're talking to the people of the past who have written the code, the libraries, the operating system, the *everything* for you. Good or bad, interacting with a computer allows you to interact with everyone who's built this tower of abstractions that gets you to this point. Building more systems allows you to talk to more people. Daily I have conversations with McCarthy, with Manolios, with Stallman, with Pottering (maybe unfortunately), through the systems of theirs that I make considerable use of.