There's an old Twitter thread of mine that I completely forgot about until my girlfriend was asking me about how to significantly simplify implementing a typechecker. This is something I've been meaning to turn into a blog post at some point so I figured I'd write up a quick first draft on Cohost.

Lean type checkers

From my perspective, one of the biggest open problems in implementing programming languages is how to add a type system to the language without significantly complicating the implementation.

For example, in my tutorial Fall-from-Grace implementation the type checker logic accounts for over half of the code. I've highlighted below the modules responsible for type-checking:

$ wc -l src/Grace/*.hs
      43 src/Grace/Compat.hs
     486 src/Grace/Context.hs      # Type-checking module
      31 src/Grace/Domain.hs       # Type-checking module
      60 src/Grace/Existential.hs  # Type-checking module
     204 src/Grace/Import.hs
    2529 src/Grace/Infer.hs        # Type-checking module
      61 src/Grace/Input.hs
     172 src/Grace/Interpret.hs
     506 src/Grace/Lexer.hs
      91 src/Grace/Location.hs
     120 src/Grace/Monotype.hs     # Type-checking module
     504 src/Grace/Normalize.hs
     658 src/Grace/Parser.hs
     158 src/Grace/Pretty.hs
     208 src/Grace/REPL.hs
     767 src/Grace/Syntax.hs
     108 src/Grace/TH.hs
     820 src/Grace/Type.hs         # Type-checking module
     118 src/Grace/Value.hs
    7644 total

And, believe me, I tried very hard to simplify the type-checking code.

This is the reason why programming language implementers will be pretty keen to just not implement a type-checker for their language, and that's how we end up with a proliferation of untyped programming languages (e.g. Godot or Nix), or ones that end up with a type system bolted on long after the fact (e.g. TypeScript or Python). You can see why someone would be pretty tempted to skip implementing a type system for their language (especially given that it's an optional language feature) if it's going to balloon the size of their codebase.

So I'm extremely keen on implementing a "lean" type checker that has a high power-to-weight ratio. I also believe this is an important foundational step for functional programming to "go viral" and displace imperative programming.

Unification

The thing that bloats the size of most type-checking implementations is the need to track unification variables. These variables are placeholders for storing as-yet-unknown information about something's type.

For example, when a functional programming language infers the type of something like this Grace expression:

(λx → x) true

… the way it typically works is that it will infer the type of the function (λx → x) which will be:

λx → x : α → α

… where α is a unification variable (an unsolved type). So you can read the above type annotation as saying "the type of λx → x is a function from some unknown input type (α) to the same output type (α).

Then the type checker will infer the type of the function's input argument (true) which will be:

true : Bool

… and finally the type checker will combine those two pieces of information and reason about the final type like this:

• the input to the function (true) is a Bool
• therefore the function's input type (α) must also be Bool
• therefore the function's output type (α) must also be Bool
• therefore the entire expression's type is Bool

… which gives the following conclusion of type inference:

(λx → x) true : Bool

However, managing unification variables like α is a lot trickier than it sounds. There are multiple unification algorithms/frameworks in the wild but the problem that all of them share is that they all require you to implement what is essentially a bespoke logic programming language (with all of the complexity that entails). Like, geez, I'm already implementing a programming language and I don't want to have to implement a logic programming language on top of that just to power my type-checker.

So there are a couple of ways I've been brainstorming how to address this problem and one idea I had was: what if we could get rid of unification variables altogether?

Deleting unification

Alright, so this is the part of the post that requires some familiarity/experience with implementing a type-checker. If you're somebody new to programming language theory then you can still keep reading for the vibes or whatever but this is where I have to assume some prior knowledge otherwise this post will get way too long.

The basic idea is that you start from the "Complete and Easy" bidirectional type checking algorithm which is a type checking algorithm that does use unification variables¹ but is simpler than most type checking algorithms. Those rules look like this (I don't really expect you to read through them):

Now, delete all the rules involving unification variables. Yes, all of them. That means that all of the type-checking judgments from Figures 9 and 10 are gone and also quite a few rules from Figure 11 disappear, too.

What's left? Surprisingly, still a lot! But you lose two important type inference features if you do this:

• you can no longer infer the types of lambda arguments

  For example, you can no longer infer the type of a function like this one:

  λx → x == False
  

  Normally, a type checker that supports unification can infer that the above function has type Bool → Bool, but (in general) a type checker can no longer infer that when you drop unification variables from the implementation.

  This loss is not too bad (in fact, it's a pretty common trade-off proposed in the bidirectional typechecking literature) because you can make up for it in a few ways (all of which are easy and efficient to implement in a type checker):

  • You can allow the input type to be inferred if the lambda is given an explicit type annotation, like this:

    λx → x == False : Bool → Bool
    

    More generally, you can allow the input type to be inferred if the lambda is checked against an expected type (and a type annotation is one case, but not the only case, where a lambda is checked against an expected type). We're going to lean on this option pretty heavily.

  • You can allow the user to explicitly supply the type of the argument

    … like this:

    λ(x : Bool) → x == False
    

    This is how Dhall works, although it's not as ergonomic.

  • You can allow the input type to be inferred if the lambda is applied to an argument

    This is not that interesting, but I'm mentioning it for completeness. The reason it's not interesting is because you won't often see expressions of the form (λx → e) y in the wild, because they can more idiomatically be rewritten as let x = y in e.

• you would now need to automatically instantiate polymorphic functions

  What this means is that all user-defined polymorphic functions would now require explicit type abstraction and explicit type application, which is a major regression in the type system's user experience.

  For example, in a language with unification variables you can write the polymorphic identity function as:

  λx → x
  

  and use it like this:

  let id = λx → x
  in  (id true, id 1)
  

  … but when you drop support for unification variables then you have to do something like this:

  let id = λ(a : Type) → λ(x : a) → x
  in  (id Bool true, id Natural 1)
  

  Most programmers do NOT want to program in a language where they have to explicitly manipulate type variables in this way. In particular, they really hate explicit type application. For example, nobody wants to write:

  map { x : Bool, … large record type … } Bool (λr → r.x) rs
  

  So we need to figure out some way to work around this limitation.

The trick

However, there is a solution that I believe gives a high power-to-weight ratio, which I will refer to as "keyword" type checking:

• add a bunch of built-in functions

  Specifically, add enough built-in functions to cover most use cases where users would need a polymorphic function.

• add special type-checking rules for those built-in functions when they're fully saturated with all of their arguments

  These special-cased type-checking rules would not require unification variables.

• still require explicit type abstraction when these built-in functions are not fully saturated

  Alternatively, you can require that built-in polymorphic functions are fully saturated with their arguments and make it a parsing error if they're not.

• still require explicit type abstraction and explicit type application for all user-defined (i.e. non-builtin) polymorphic functions

I'll give a concrete example: the map function for lists. In many functional programming languages this map function is not a built-in function; rather it's defined within the host language as a function of the following type:

map : ∀(a b : Type) → (a → b) → List a → List b

What I'm proposing is that the map function would now become a built-in function within the language and you would now apply a special type-checking rule when the map function is fully saturated:

Γ ⊢ xs ⇒ List a   Γ ⊢ f ⇐ a → b
───────────────────────────────
Γ ⊢ map f xs ⇐ List b

In other words, we're essentially treating the map built-in function like a "keyword" in our language (when it's fully saturated). Just like a keyword, it's a built-in language feature that has special type-checking rules. Hell, you could even make it an actual keyword construct (e.g. a list comprehension) instead of a function call.

I would even argue that you should make each of these special-cased builtin-functions a keyword or a language construct instead of a function call (which is why I call this "keyword type checking" in the first place). When viewed through this lens the restrictions that these polymorphic built-in functions (A) are saturated with their arguments and (B) have a special type checking judgment are no different than the restrictions for ordinary keywords or language constructs (which also must be saturated with their arguments and also require special type checking judgments).

To make an analogy, in many functional programming languages the if/then/else construct has this same "keyword" status. You typically don't implement it as a user-space function of three arguments:

ifThenElse : ∀(a : Type) → Bool → a → a → a

… but instead you define if as a language construct and you also add a special type-checking rule for if:

Γ ⊢ b ⇐ Bool   Γ ⊢ x ⇒ a   Γ ⊢ y ⇐ a
────────────────────────────────────
Γ ⊢ if b then x else y ⇒ a

… and what I'm proposing is essentially greatly exploding the number of "keywords" in the implementation of the language by turning a whole bunch of commonly-used polymorphic functions into built-in functions (or keywords, or language constructs) that are given special type-checking treatment.

For example, suppose the user were to write a function like:

let twice = λ(a : Type) → λ(x : a) → [ x, x ]

in  twice (List Bool) (twice Bool true)

… that would still not be very ergonomic and (in my opinion) it's not reasonable for the language to provide a twice built-in function. However, the language could provide a generally useful replicate builtin function (like Haskell's replicate function):

replicate : ∀(a : Type) → Natural → a → List a

… with the following type-checking judgment:

Γ ⊢ n ⇐ Natural   Γ ⊢ x ⇒ a
───────────────────────────
Γ ⊢ replicate n x ⇒ List a

… and then you would tell the user to use replicate directly instead of defining their own twice function:

replicate 2 (replicate 2 true)

… and if the user were to ask you "How do I define a twice synonym for replicate 2" you would just tell them "Don't do that. Use replicate 2 directly."

Conclusion

This approach has the major upside that it's much easier to implement a large number of keywords than it is to implement a unification algorithm, but there are other benefits to doing this, too!

• It discourages complexity and fragmentation in user-space code

  Built-in polymorphic functions have an ergonomic advantage over user-defined polymorphic functions because under this framework type inference works better for built-in functions. This creates an ergonomic incentive to stick to the "standard library" of built-in polymorphic functions, which in turn promotes an opinionated coding style across all code written in that language.

  You might notice that this approach is somewhat similar in spirit to how Go handles polymorphism which is to say: it doesn't handle user-defined polymorphism well. For example, Go provides a few built-in language features that support polymorphism (e.g. the map data structure and for loops) but if users ask for any sort of user-defined polymorphism then the maintainers tell them they're wrong for wanting that. The main difference here is that (unlike Go) we do actually support user-defined polymorphism; it's not forbidden, but it is less ergonomic than sticking to the built-in utilities that support polymorphism..

• It improves error messages

  When you special-case the type-checking logic you can also special-case the error messages, too! With general-purpose unification the error message can often be a bit divorced from the user's intent, but with "keyword type checking" the error message is not only more local to the problem but it can also suggest highly-specific tips or fixes appropriate for that built-in function.

• It can in some cases more closely match the expectations of imperative programmers

  What I mean is: most programmers coming from an imperative and typed background are used to languages where (most of the time) polymorphism is "supported" via built-in language constructs and keywords and user-defined polymorphism might be supported but considered "fancy". Expanding a functional programming language's built-in support for polymorphic utilities and constructs would actually make them more comfortable using polymorphism instead of trying to teach them how to produce and consume user-space polymorphic functions.

  For example, in a lot of imperative languages the idiomatic solution for how to do anything with a list is "use a for loop" where you can think of a for loop as a built-in keyword that supports polymorphic code. The functional programming equivalent of "just use a for loop" would be something like "just use a list comprehension" (where a list comprehension is a "keyword" that supports polymorphic code that we can give special type checking treatment).

That said, this approach is still more brittle than unification and will require more type annotations in general. The goal here isn't to completely recover the full power of unification but rather to get something that's not too bad but significantly easier to implement.

I think this "keyword type checking" approach has the potential to be an interesting point in the type checking design space for functional programming languages that need to have efficient and compact implementations (e.g. for ease of embedding). Also, this can potentially provide a stop-gap solution for novice language implementers that want some sort of a type system but they're not willing to commit to implementing a unification-based type system.

1. I believe some people might take issue with calling these unification variables because they consider bidirectional typechecking as a distinct framework from unification. Moreover, in the original bidirectional type checking paper they're called "unsolved" variables rather than unification variables. However, I feel that for the purpose of this post it's still morally correct to refer to these unsolved variables as unification variables since their usage and complexity tradeoffs are essentially identical to unification variables in traditional unification algorithms.

You're thinking of the Grace browser:

… and this is the talk you're probably thinking of:

I also wrote a blog post about it, too:

I name all my programming languages (Morte, Dhall, Fall-from-Grace) after characters from my favorite video game: PlaneScape: Torment

I've been slowly trying to popularize what I call content-oriented programming languages (a term I made up for lack of a better term), but very few people are familiar with the concept, so I wanted to explain the idea behind these types of programming languages as concisely as possible in this post.

Consider the following functional program written in Haskell syntax:

-- Increment a number
increment
    :: Int
    -- ^ Number to increment
    -> Int
increment x = x + 1

-- Double a number
double x = x * 2

-- Double and then increment a number
composite x = increment (double x)

You look at that program and what you probably think is something like:

Those are three pure functions (increment, double, and composite) waiting to be incorporated into a larger program that will eventually interface with the outside world in some way (e.g. a command-line application or web server)

But what if I told you that the above program WAS the interface with the outside world?

For example, imagine if I handed you a compiler that took the above program and generated three command-line tools (named increment, double, and composite), complete with --help output:

$ increment --help
Usage: increment -x Int

  Increment a number

Available options:
  --help  Show this help text
  -x      Number to increment

… and when you use them they work the way you expect:

$ double -x 4
8

$ increment -x 8
9

$ composite -x 4
9

You wouldn't have to "wrap" these pure function in a command-line interface because they ARE the command-line interface. They already have all the information necessary to generate the executable.

In most other programming languages, if you wanted to wrap these pure functions in a command-line interface you'd add a whole bunch of noisy wrapper code to interface with the outside world and that wrapper code is a giant distraction from what the code is actually doing. The compiler for my programming language can handle that for me because it already has all that information it needs to do so.

Moreover, we can convert this same trio of functions to other interfaces. For example, instead of compiling those three functions to three command-line tools I could instead compile them to three JSON-based HTTP services and do stuff like this:

$ curl https://double.example.com --data '{ x: 4 }'
8

$ curl https://increment.example.com --data '{ x: 8 }'
9

$ curl https://composite.example.com --data '{ x: 4 }'

The same three functions (the "content") can be "presented" in multiple ways, such as by compiling to command-line tools or HTTP services. By separating the "content" from the "presentation" we simplify our code and allow the same code to be used in multiple contexts. Plus it's just so much simpler to boot (no need to mess with CLI libraries or HTTP libraries).

If you want to see a particularly compelling example of a non-trivial "presentation" layer you should check out my Grace browser which converts pure functions to web forms.