Notes
2026/05/13
I have a lot of respect for statically typed languages, and yet the languages I've been prototyping have mostly been dynamically typed. Not because I find static types useless, quite the opposite. As a user of a programming language, I want static types. But as a designer of a language, I really avoid type systems.
I can finally pinpoint why I dislike type systems so much, and it's not that I dislike using them or object to them in principle. I'm not even that interested in the ultra-dynamic shenanigans of languages like Smalltalk, Self, Io, Ruby, etc. What I've always disliked about type systems is that they are the ultimate nerdsnipe in language design, because they are almost by definition never done, never good enough, they can always only ever be approximations of what you really want your language to express without it being rejected by the type checker.
As someone who is extremely tempted by the siren call of perfect abstractions and pure foundational calculi, maybe type systems are a drug that I don't want to allow myself to touch. In fact, I would argue that the entire field of PLT has become an opium den of type theory, because soundness proofs and operational semantics have nowadays become the only acceptable way to do PLT, with very few exceptions. (It helps that type theory comes with an appealing mathematical veneer.)
(I could bring this back to Wittgenstein, so of course I will, and hand-wave away all the details: Type systems are the ultimate Modernist idea, because they are built on the belief that the only way to reason about language is in terms of a split between object language and meta language. This split, as the story goes, keeps everything well-founded, because you never talk about things on the same level, which would of course lead to ugly inconsistency through self-reference. Instead, everything can be traced back to a level below. The medieval order is never disrupted, because our systems remain transcendent, they are always dependent on some outer principle to imbue them with meaning. In the old days we identified this principle with the divine, in our more enlightened times we talk about the ideal realm of mathematical Platonism, of “truth”. But it's still fundamentally a divine principle, it's still transcendence in action, it's still open to Nietzschean/Wittgensteinian disruption.)
Back to what we actually care about: Building a language. I've been thinking about lexical scopes for effects for a while. I firmly believe that the principle of least power is under-appreciated in language design and I would like my language to be less powerful if given the choice, until I can find a very compelling case for why more power is needed.
The choice of language is a common design choice. The low power end of the scale is typically simpler to design, implement and use, but the high power end of the scale has all the attraction of being an open-ended hook into which anything can be placed: a door to uses bounded only by the imagination of the programmer.
I'm going to come back to effects in a second, but let me go on a quick detour: I've been thinking about static checks that are deliberately less complicated than type systems but that nevertheless provide interesting static restrictions, almost “for free” in the language design space. (Well, nothing is ever really free, but let's say with very few tradeoffs.) Here's an example: Checking statically that all of your variables are lexically bound and thus can be resolved does not require anything resembling a type system, makes compilation much more efficient, and only restricts a language by throwing out the most extreme form of dynamism, namely dynamically constructing variable names and looking them up in the environment. I would consider such a static check to be almost a no-brainer, because it keeps 99% of the dynamism that you ever care about when writing programs while catching annoying typos at compile time instead of runtime. What are other examples of such non-type-system-but-still-static checks?
I can think of a few other examples: Checking the arity of functions statically restricts a language in an extremely minimal way (it does require something that is already almost type-system like) but catches annoying runtime errors. Statically checking mutability annotations in an imperative language seems like another candidate. Checking substructural properties in general might be another candidate, because it ends up being pretty simple if you don't need to care about reference lifetimes. Are there other examples?
I have always described Kombucha as dynamically typed and I would be extremely surprised if anyone disagreed with this description. But Kombucha very deliberately tracks variable scopes lexically and statically and doesn't provide a way to dynamically construct a variable name or an effect name. All strings are interned and all scopes are statically clear, in contrast to e.g. Lisps. But where do you draw the line between these “light” static checks and a real type system? Would checking arity statically count as a type system? Where do “simple” static checks end and type systems begin?