Notes
2025/12/28
Continuing my initial thoughts on Kombucha's type system, I've been thinking more about how to build a type system that targets a slightly different point in the design space than most other languages:
I want to build a type system that is radically simple and gives me some static guarantees while getting out of my way so that the language still feels dynamically typed.
Most modern languages use type systems that are either extremely sophisticated (both in terms of implementation and use) or simple but restrictive (in the sense that they rely on nominal types and rarely support a combination of parametric polymorphism and subtyping).
Instead, I want something that feels closer to TypeScript: A type system that provides some static guarantees and catches most type errors, but without requiring nominal types and data type declarations. However, in contrast to TypeScript I don't want to support the maximum amount of dynamism and I want a type system that is much simpler to implement.
Recursive data types, such as cons lists or trees, need to be supported, so I need recursive types. Equi-recursive types are elegant but more complex in terms of implementation, which I would like to avoid. However, iso-recursive types require explicit fold / unfold operations, which are hard to insert automatically in the absence of nominal types and data type definitions.
I'm still wondering whether there is a notion that is of use in dynamic languages and that corresponds to iso-recursive types, so that fold / unfold would feel less like pointless ceremony and more like saying something meaningful? Is there value in distinguishing “folded” and “flat” data in a dynamically typed language?
I was originally planning to support both union types and (restricted) intersection types, but intersection types get complicated really fast. Maybe union types are enough? They are conceptually much simpler, well understood (and liked) in TypeScript, and much easier to implement.
Also, they are perfect for a type system that should feel structural (at the cost of being less precise), because they always allow you to “throw away” information and talk about a combination of base types.
Parametric polymorphism (in other words, generics) adds a lot of complexity to a type system, starting with the need to unify type variables and generalize them to a type scheme at the right points. Ad-hoc polymorphism (in the style of type classes / traits) or bounded polymorphism (combining generics with subtyping) add even more complexity and subtle interactions.
Is it possible to sidestep this complexity completely, while still being able to type polymorphic functions like map and filter? Zig's approach of using comptime evaluation is unorthodox but interesting: Instead of trying to prove that a function is well-typed for all possible cases (using type variables), the function can be monomorphized using comptime evaluation and is then checked at each call site.
Comptime evaluation would also nicely solve the need for type aliases without requiring a new mini language: Instead, type aliases are just functions that are evaluated at compile time and that return types (without type aliases and without type variables).
Using comptime as a replacement for these advanced type system features might sometimes be less efficient (because it requires checking a type at several call sites), but then again HM type inference has exponential time complexity in the worst case as well. Who knows, the added overhead of comptime monomorphization might not matter that much in practice.
Using comptime to evaluate away polymorphism before type checking is a hack, but it sounds like a hack that is worth exploring.