Notes
2025/11/30
I've recently been thinking about how to add a type system to Kombucha. This has been on the roadmap for a while, even though Kombucha deliberately started its life as a dynamically typed language.
Type systems are notoriously hard to add to a language designed without types in mind, but Kombucha was also meant to feel very light on types and more like a dynamically typed language. Although the pendulum seems to be swinging back in the direction of static types, Kombucha has been very influenced by Clojure and shares Clojure's view that having static types is not a panacea but a tradeoff.
That being said, I've recently been able to clarify the tradeoffs that I want Kombucha to make and they all seem to point to a type system with the following characteristics.
The first reason for wanting a type system is both simple and somewhat unorthodox: I want to ensure that recursion is only possible by using Kombucha's fixed point operator (which is compiled to a special bytecode instruction), not by using implicit recursion, for example through manually constructing a fixed point combinator. A type system is simply the easiest and most boring way to reject implicitly/accidentally recursive programs.
The reason for wanting to reject implicit recursion is two-fold: First of all, I'm not aware of genuinely useful constructions that employ implicit recursion. It's mostly a neat trick, which ends up being much harder to read than using explicit recursion. This might be one of the areas where type systems offer a (very limited) benefit with (almost) no tradeoffs.
Secondly and more importantly, I'm interested in enforcing explicit recursion for implementation reasons: In the presence of partial evaluation, it's extremely helpful to know that unbounded recursion can only occur in the presence of the explicit fixed point operator, because then partial evaluation can evaluate these recursive operations up to a bounded limit.
Types are more interesting from a non-implementation UX perspective though. Most static types systems for functional languages lean into algebraic data types that are explicitly declared and often nominal types where the same type definitions with different names are considered to be distinct types.
I want to explore how close Kombucha can get to feeling like a dynamically typed language while still providing some of the main benefits of a statically typed language. The aim isn't to provide perfect correctness through types, the aim is to get 80% of what static types normally provide while paying only 20% of the annoyance cost of most type systems.
This is why I want a type system that is structural, where two types are considered to be equal if they have the same structure. TypeScript gets this mostly right but ends up with an extremely complicated type system due to having to support anything that JavaScript can express. The basic idea, of leaning heavily on union and intersection types, seems extremely promising though.
The next question is to which degree types should be inferred (instead of having to be explicitly annotated). Most new languages seem to have learned their lesson from Java and do not require every variable to be explicitly annotated. Full type inference, however, while being technically possible in systems such as Hindley-Milner or rank 2 intersection types, is hard to combine with other language features such as subtyping.
Annotating only function parameters and return types seems to be a good balance in practice. This is more challenging in Kombucha, which doesn't have a single privileged construct to create functions, but is still applicable if we require type annotations in all cases where bindings aren't immediately assigned values and would thus have redundant types. This then boils down to only annotating function parameters.
Once type annotations are introduced, especially in the presence of structural types with potentially large unions or intersections, it becomes annoying to repeat the same complicated type over and over again. Type aliases are an obvious solution, but they are non-trivial for two reasons:
A | B | C in the presence of the two aliases T1 = A | B and T2 = B | C. Should the type A | B | C be reported as is, or as T1 | C, or as A | T2?In Kombucha, which doesn't really have the notion of a “top level” block, there's also the issue of scope: If type aliases are supposed to mirror other definitions, they should only be valid within a scope. But then how are type aliases reported if some values with that type alias outlive the scope of the type alias? And where are type aliases allowed to be defined? Only as elements of { ... } blocks?
There is an interesting way in which a type system could make Kombucha's existing syntax simpler: As part of its macro system, Kombucha syntactically distinguishes bindings (which are variables to be bound) from values (variables that are used):
// `foo` is a binding, `bar` is a value
:foo = bar
This creates a lot of noise in Kombucha, because every binding needs to be explicitly marked as a variable-to-be by using the prefix colon notation. (Well, at least the bindings that are not immediately followed by a block. If one of the arguments of a macro is a raw block of the form { ... }, the other arguments can be assumed to be bindings. More details here.)
Bindings are a natural place to put type annotations. In fact, it is fine to allow type annotations only after bindings, because all function parameters and variable definitions use bindings. This makes it possible to get rid of the prefix colon syntax and instead treat every identifier followed by a type annotation as a binding:
// explicit bindings, untyped
:foo = "Hello"
:bar = "World"
// implicit bindings, typed
foo: string = "Hello"
bar: string = "World"
The big drawback is that this would be a throwback to Java days where each variable needs to be annotated. One option would be to use a special syntax to mark the variable type as inferred:
// the types of `foo` and `bar` are inferred
foo: ? = "Hello"
bar: ? = "World"
// or even more succinctly:
foo? = "Hello"
bar? = "World"
But even this feels syntactically heavy. Additionally, Kombucha currently uses postfix colons for keyword lists in function calls, which would conflict with postfix colons for type annotations.
These are just initial sketches of how a type system might fit into Kombucha's design philosophy. The challenge is finding the right balance between static guarantees and dynamic flexibility. But nobody said bolting a type system onto an existing language would be easy, did they?