Unification-free ("keyword") type checking
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. In the following lines of code report I’ve highlighted the modules
responsible for type-checking with a ‡:
$ cloc --by-file src/Grace/*.hs
…
--------------------------------------------------------------------------------
File blank comment code
--------------------------------------------------------------------------------
src/Grace/Infer.hs ‡ 499 334 1696
src/Grace/Type.hs ‡ 96 91 633
src/Grace/Syntax.hs 61 163 543
src/Grace/Parser.hs 166 15 477
src/Grace/Lexer.hs 69 25 412
src/Grace/Normalize.hs 47 48 409
src/Grace/Context.hs ‡ 72 165 249
src/Grace/Import.hs 38 5 161
src/Grace/REPL.hs 56 4 148
src/Grace/Interpret.hs 30 28 114
src/Grace/Pretty.hs 25 25 108
src/Grace/Monotype.hs ‡ 11 48 61
src/Grace/Location.hs 16 15 60
src/Grace/TH.hs 23 32 53
src/Grace/Value.hs 12 53 53
src/Grace/Input.hs 10 8 43
src/Grace/Compat.hs 9 2 32
src/Grace/Existential.hs ‡ 12 23 25
src/Grace/Domain.hs ‡ 4 7 20
--------------------------------------------------------------------------------
SUM: 1256 1091 5297
--------------------------------------------------------------------------------
That’s 2684 lines of code (≈51%) just for type-checking (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 that a compact type checker
is an important foundational step for functional programming to “go
viral” and displace imperative programming. This post outlines one
approach to this problem that I’ve been experimenting with.
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:
… the way it typically works is that it will infer the type of the
function (λx → x) which will be:
… 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:
… 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:
However, managing unification variables like α is a lot
trickier than it sounds. There are multiple unification
algorithms/frameworks in the wild but the problem with all of them is
that you have to essentially implement 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 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. The type checking rules
look like this (you can just gloss over 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.
Surprisingly, you can still type check a lot of code with what’s
left, but you lose two important type inference features if you do
this:
… and I’ll dig into those two issues in more detail.
Inferring lambda argument
types
You lose the ability to infer the type of a function like this one
when you drop support for unification variables:
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 type checking 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 pretty heavily because it’s pretty
reasonable to ask users to provide type annotations for function
definitions and also because there are many situations where we can
infer the expected type of a lambda expression from its immediate
context.
You can allow the user to explicitly supply the type of the
argument
… like this:
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.
Instantiating polymorphic
code
The bigger issue with dropping support for unification variables is:
all user-defined polymorphic functions 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:
… 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 … } 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
optionally, turn these built-in functions into keywords or
language constructs
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 or language 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 this type:
ifThenElse : ∀(a : Type) → Bool → a → a → a
Rather, 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 create a polymorphic function
like this one:
let twice = λ(a : Type) → λ(x : a) → [ x, x ]
in twice (List Bool) (twice Bool true)
That’s not very ergonomic to define and use, but we also can’t
reasonably expect our programming language to provide a
twice built-in function. However, our 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 polymorphic code 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 (or keyword or language
construct).
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”.
Leaning on polymorphism via keywords and language constructs would
actually make them more comfortable using polymorphism instead of trying
to teach them how to produce and consume user-defined 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” can potentially occupy a “low
tech” 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.
There’s also variation on this idea which Verity Scheel has been
exploring, which is to provide userland support for defining new
functions with special type-checking rules and there’s a post from her
outlining how to do that:
User
Operators with Implicits & Overloads