strong-types-weak-types

I love the way that programming languages make my brain feel, work andtick.

Programming is really just a conversation with the computer. The toolswe use to program, with varying degrees of success and autonomy, improvethe flow of this conversation.

Strong Types

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

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

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

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

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

Unfortunately, to get to this point requires a significant amount ofeffort and labor - it's really difficult to learn to understand therules of an incredibly complex system! - and up until, and even whenyou've reached that point and have to pursue some update, you cancontinue to run into new rulesets that you have to update your priorswith; changing the world you have to navigate and understand as youintegrate the code of others, whether libraries or new parts of thecodebase. High school debate, with its thinly veiled ad homenim attacksand strawman arguments and strangely radical frameworks, was lessfrustrating 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 cantell the computer what you want, no matter how crazy, and it'll justhappen. Write some parentheses, pass some functions as arguments,construct something at the nth level of abstraction and it'll becallable five functions down the stack without having to accomodate orconstrain it with any system of types.

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

This feels a bit like perfecting a home-cooked meal. The recipe goes outthe window, the rules are completely arbitrary, and you're throwingspices into the mix as you go - "let's try some coriander! how aboutusing caar instead of caddr here?" - as you have a natural conversationwith 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 whereyou can blame their rules or blame yourself, while programming in a lispruns you into errors that are entirely of your own design. The formerallows you to utilize a system, constructing a debate in which youcompromise your model of the world with theirs until you meld into somesystem amenable to both ideas. The latter leaves you no such framework;it's entirely up to you to set up the guardrails, establish theframework, and set up the principles under which we construct ourprogramming environment and world, and as such the fault is only withthe model you've constructed yourself when things break down. Holdingand owning this complete model is such a beautiful thing.

talking

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

Revisions
DateHash
2023-02-22
Navigation
Previoustalks
Nextclothing
Uppages