This is a transcript of a PL Wonks lightning talk.
Ok. So this talk is going to be about providing a toolkit to macro writers in Clojure, to be able to communicate to the type system.
Here’s the setting. On the left, we have the type system. It finds macros it needs to expand, but it has no idea how these macros work — all the type system has is the ability to expand macros, and then make a best-effort on type checking the expansion. On the other side, we have the macro authors, who, sure, are willing to teach the type system how the macro actually works, but, currently, there’s no way to actually do that.
So in this talk, I’m proposing that we provide an extensible interface to Typed Clojure’s internals to help it be more expressive and usable.
And how can Typed Clojure be made more expressive and usable? Well, by provide macros that yield better static type error messages, macros that require less type annotations, and macros that are optimized for type checking performance, rather than runtime performance.
So first, let’s talk about how we can write macros that yield better static type error messages.
Let’s look at this simple when macro — it’s like an if
but the else branch is implicitly nil.
So let’s imagine we’re trying to type check the expanded if
form as a Number.
And we’ve found that the else branch is actually nil. It should
be a Number.
So, what we’d like the type system to do is blame the original
when expression.
But what it actually does is blame the original when macro —
basically blame the macro-writer.
The type system needs more information as to who to blame.
The solution here is to allow macro-writers to provide blame labels
to the type system. For example, in the else branch here,
the red box symbolizes an annotation the macro-writer can use.
It says, if the else branch does not conform to the expected type,
then blame the entire when expression.
Next, to argue that an extensible interface to Typed Clojure’s internals helps make it more expressive and usable, we’re going to look at how we can make macros require less type annotations.
So here’s a for comprehension. It increments '(1 2 3) to
'(2 3 4). You’ll notice there’s two annotations —
one for the input, and one for the output.
How might we eliminate the output annotation, knowing the
output of this for comprehension is very complicated, with
nested loops and local mutation?
To set the stage, let’s say the expected type for this
for comprehension is a sequence of symbols.
That means, the surrounding program expects it to be
sequence of symbols — clearly it’s a sequence
of numbers, so some type error is going to happen.
But, who’s going to be blamed?
Let’s imagine the expansion is a bunch of code, with an increment form somewhere in it.
What we really want to do is propagate this Sym expected
type into this increment form, because this will correctly blame
the responsible user-written code.
And, unsurprisingly, our solution is exactly this: give the macro writer the ability to take an expected type from a type checking run, deconstruct it, and then propagate it to where error messages will be optimized.
And finally, providing an extensible interface to Typed Clojure’s internals helps us write macros that yield simpler checks.
For example, here’s our for comprehension. It doesn’t have
any annotations. How can we get away with this?
Well, we just have a simplified expansion: instead of hundreds of lines of complex code, we have a single function call. Now, we basically have two macros: one optimized for runtime performance, and one optimized for type checking performance.
In an optional type system like Typed Clojure which does not optimize programs, we can keep the runtime-optimized expansion and throw away the type-checking optimized expansion (after we’re done). Clojure programs routinely reload code (and therefore reexpand macros), so this might be a feasible approach for Typed Clojure — perhaps less-so for systems like Typed Racket.
So finally, to conclude, we’re providing an extensible interface to Typed Clojure’s internals to help it be more expressive and more usable.
And how is it more expressive and more usable? Well, we can write macros that have better errors, macros that require less annotations, and macros that expand to code that is faster to type check.
Thanks!