Strong Types, Weak Types
I love the way that programming languages make my brain feel, work and tick.
Programming is really just a conversation with the computer. The tools we
use to program, with varying degrees of success and autonomy, improve the flow
of this conversation.
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.
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
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.
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.
Strong Types
Weak Types, Free Types
close
talking