Notes
2026/09/13

Type systems as user-defined libraries

I've been wondering whether it would be possible to implement a type system fully on top of comptime evaluation, in such a way that the type system is defined by the user, as a comptime check for an otherwise dynamic language. First of all, here's what this wouldn't do: Being optional and user-defined, such a type system wouldn't speed up the language implementation. But it could catch type errors at compile time and improve tooling support. TypeScript is a language that seems to do pretty well with that sort of tradeoff (then again, a lot of effort has gone into making JS fast even in the absence of types).

Here's the basic idea: Let's treat type annotations in the language as values and let's do type checking by comptime evaluating our program with these annotation values, effectively doing a sort of abstract interpretation. Implementing a type system would come down to defining how the primitive parts of the language evaluate annotation values.

// The part after `:` is simply a value that gets passed to the type checker:
add(x: Int, y: Int) = {
    x + y
}

// this should produce a type error:
add(1, "two")

So in a function definition such as add(x: Int, y: Int) = { ... } we would literally call the function add with the two keywords Int and Int as its arguments. If add calls other user-defined functions, these would in turn be called with these values, but in the above case we merely call the built-in +. How does addition know how to handle the keywords Int and Int? Through user-defined definitions for how the “type system” is supposed to handle the built-in parts of the language.

The definition of (a part of) the “type system” would then look as follows:

+(x, y) = {
    match [x, y] [
        [Int, Int] => { Int }
        [x, y] => { error("expected two ints") }
    ]
}

Since such a type system is entirely user-defined, there is no guarantee that the type checker “makes sense”. It would for example be possible to define the check for +(x, y) in such a way that two strings are accepted, even if the built-in addition of the language doesn't know how to handle such an addition and would fail at runtime.

The upshot is that it's also possible to check more sophisticated properties, such as by defining addition over a type such as PositiveInt or making sure that numbers are only divided by NonZeroInt. Since “type checking” is really just abstract evaluation at compile time, it's entirely up to a user to decide which properties need to be checked (and it's also their responsibility to ensure that a type system is sound).

Where can type annotations be placed? A colon followed by a type can only be used after bindings, in other words wherever new variables come into scope, for example in function definitions, let statements, and patterns in general. (This means that a function's return type can be annotated as part of naming the function as a binding, or as part of assigning an anonymous function to a variable.)

What happens when type annotations are missing? Since there is no way to evaluate the function by itself without any types as arguments, it will simply not be type-checked by itself and instead be fully instantiated as its body wherever it is used (and where concrete types are available), effectively monomorphizing the function at comptime. There is thus no type inference and no guarantee that all functions or definitions will be type-checked. The advantage (besides being simple) is that a monomorphized function can have a much more precise type without requiring any form of polymorphism on the level of types.

twice(x) = {
    match (type(x)) [
        Int => { x + x }
        Str => { concat(x, x) }
        _ => { error("expected either int or string") }
    ]
}

// this works:
int_twice: Int = twice(2)
str_twice: Str = twice("foo")

The above can be checked without any problems, because twice(Int) evaluates to Int while twice(Str) evaluates to Str, without the need for an intersection type like (Int -> Int) & (Str -> Str) which would add considerable complexity to the type system.

If the burden of checking each monomorphized instance of twice independently becomes too much, we can always opt for a simpler type system with less precision, for example by introducing union types and giving twice the type (Int | Str) -> (Int | Str). This would then only check twice_typed once and memoize its type, at the cost of having to choose the less precise union type:

// same as twice but with type annotations:
twice_typed(x: Int | Str): Int | Str = {
    twice(x)
}

// this fails the type check:
int_twice_typed: Int = twice_typed(2)
str_twice_typed: Str = twice_typed("foo")

// but this looser type checks fine:
int_twice_typed: Int | Str = twice_typed(2)
str_twice_typed: Int | Str = twice_typed("foo")

To be clear, I'm not advocating for privileging union types in any way. The operator | would just be an infix function like any other and it's the job of the type system (well, the pluggable functions) to give it meaning, which also means that soundness depends on how the “type system” is defined. It's possible to write an unsound type system and that's fine.

There also needs to be a way to lift literals such as 5 or "foo" into types, so that something like x: Int = 5 can be type-checked. Perhaps it would even be possible to simply use an override for the existing type function for it? (An override of type would have to both lift literals into types and also properly type the usage of type at runtime, so that e.g. type(Int) returns the type Tag(Int), which at runtime is just the tag Int.)

The user-defined functions that make up the “type system” would then be simply nothing more than a different “standard library”, which does abstract evaluation at compile time. But the compile time machinery is not special in any way. All the primitive functions can be redefined simply because the same is true for the language even in the absence of type annotations. But the way function calls work cannot be redefined, for example. A function call in the type system is simply a comptime-evaluated call.

This has implications for recursion: A type system can't just evaluate calls that involve recursion, because it has to evaluate-to-type-check both arms of a conditional, which would immediately lead to non-termination for most recursively defined functions. This is why all recursion must flow through fix, an explicit fixed point combinator, which can then be redefined by the user as part of the type system like any other built in primitive.

This requires a “mini type system” that merely disallows implicit recursion, or perhaps we could simply accept that anything involving implicit recursion might lead to non-termination during type-checking. Either way, making recursion flow through an explicit fixed point combinator could be a desirable trait even in the absence of a type system.