Proposal: a macro DSL based on bidirectional type checking #61

Hackett's goal has always been for "types and macros to be able to cooperate and communicate with each other". Today, however, Hackett macros are written using syntax-parse's DSL, which makes it easy to write a macro which alters its output depending on the syntactic categories of its inputs, not their types. This proposal introduces a monadic DSL which makes it easy for the macro to depend on the type of its inputs, without unnecessarily forcing the type-checker to commit to a type for all of the inputs before expanding the macro.

Design goals

1. It should be possible for a macro to ask the type-checker for the inferred type of an input and/or its output.
2. It should be possible for a macro to tell the type-checker about the expected type of an input and/or its output.
3. The implementation should not use backtracking.

Unification API

When implementing type inference using unification, the important primitive operations are:

1. newSVar : (Solver SVar): create a new solver variable about which nothing is known yet.
2. unify : {TypeExp -> TypeExp -> (Solver Unit)}: unify two type expressions, each of which may contain some solver variables.
3. readSVar : {SVar -> (Solver TypeExp)}: look up a solver variable to obtain a type expression which may contain some solver variables; in the worst case, the entire expression may itself be a solver variable, in which case we learn nothing.

The core idea of this proposal's DSL is to expose those primitives to the macro implementation, so that it can use readSVar to inspect types, and unify to tell the type-checker about expected types. However, exposing readSVar directly (or equivalently, allowing the macro to call the type checker on a term) is problematic, because how much information we get from readSVar depends on which other expressions the type checker has already visited. Moreover, what should the macro implementation do in the worst case in which readSVar doesn't reveal any new information?

Stuck macros

Here's how I propose to solve both problems at once: instead of giving back an entire type expression containing everything we currently know about the type variable, readSVar should always return a type expression in which only the outermost type constructor is known, and all its arguments (if any) are solver variables. Let's call that variant readSVar'. If the outermost type constructor isn't yet known, readSVar' cannot return yet, so the macro expansion remains stuck until more information is obtained, by visiting and type checking other expressions (which can involve expanding other macros, which might also get stuck). If some macros are still stuck after everything is visited, then type checking fails with an "ambiguous type" error for that solver variable.

This way, the order in which the type checker visits the expressions doesn't affect the output of readSVar': either the outermost type constructor is uniquely determined, in which case the macro will receive that value (perhaps after being stuck and resumed), or two different unification calls give conflicting information for that type constructor, in which case type checking is going to fail with a type error anyway. This is similar to the way in which concurrent programs which only communicate via IVars are guaranteed to give a deterministic answer even though the order in which the threads are scheduled isn't deterministic.

Pattern matching

Repeatedly calling readSVar' in order to expand the outermost type constructor, then second outermost type constructor, etc., can be quite tedious. Let's provide a nicer API based on pattern-matching: type-pattern matching.

In the same way that ordinary pattern-matching expands to a tree of nested case statements, type-pattern matching can be desugared to a tree in which each node calls readSVar' and then examines the resulting type constructor using a case statement. The subtle relationship between the order of the type-patterns and the order in which the readSVar' calls are made (which determine the behaviour of the type checker) is the same as the relationship between the order of ordinary patterns and the order in which inputs are forced by a pure function.

One important difference between ordinary pattern-matching and type-pattern matching is the case in which a case statement with a single alternative is generated: for ordinary pattern-matching, the input is forced and then an exception is raised if the result doesn't match the pattern. For type-pattern matching, we could similarly call readSVar' and then fail with a type error if the outermost constructor doesn't match the pattern. But we can do better: we can unify the input (a solver variable) with the pattern!

Unifying SVars in context

The macro implementation should definitely receive an SVar representing the type of its output, so it can give the type checker some information (via unify) about the type of the expression it plans to produce before the macro is done producing that expression. In particular, providing this information before the macro becomes stuck might help type inference succeed more often.

Which other SVars should we provide to the macro implementation? When type-checking an expression such as (f x), we create one solver variable for f, one solver variable for x, and one solver variable for (f x). So when expanding the macro application (my-macro (f x)), we might naively think of providing the macro implementation with one solver variable for f, one solver variable for x, one solver variable for (f x), and one solver variable for (my-macro (f x)). That would be a mistake, because the macro is free to rearrange and duplicate those components arbitrarily, and it's this rearranged term which needs one solver variable per sub-term, not the input term.

Another difficulty is that an API in which macros can ask about the type of arbitrary expressions encourages a counter-productive style in which the macro asks a lot of questions about expressions without providing much information in return, thereby accidentally hurting type inference.

My proposed solution to both problems in an alternate API in which the only way to ask about the type of a target expression is to put this expression in a bigger expression which the macro implementation promises has the same type as the expression which the macro will output. This is done via a preliminary-output : {Syntax -> (Solver Unit)} command, where the syntax object may contain type annotations in which the type expression contains SVars. The command adds the syntax object to the type checker's list of expressions to visit, so that when readSVar' causes the control to return to the type checker, there is some hope for it to infer some information about the SVars in those type annotations.

Some macros may still wish to delay choosing their output type until they have learned the type of a few target expressions. This can still be done using this API, by using unsafe-coerce! or undefined! around their target expression to ensure that the output type remains unconstrained. However, due to the stigma around those partial functions, macro implementer will be encouraged to only do that if that's what they really want to do, and so in the common case the macro implementer will write an example output containing the target expression, thereby helping type inference.

Summary

A macro is implemented as a function of type {Syntax -> (Solver Syntax)}. The usual syntax-parse mechanism can be used to determine what to do with the input syntax object. If at some point the macro wants to get some information from the type checker, it must first create a solver variable, then it must use that solver variable in a type annotation inside an example output expression, then it must pattern-match on the solver variable in order to force type inference to find some information about the solver variable, or fail trying. Each time an example output is given, its type is unified with the type of the macro's call site (and thus with all the previous example outputs as well), thereby giving some important information for type inference. Eventually, the macro returns its final output, whose type is again unified with the earlier preliminary outputs.