local-expand variants

[gelisam]

I now realize that #117, #119, #216, #232, #228, #229, and this concrete use-case for local-expand all fit together into a master plan, a sequence of features which each build on the previous one:

1. local-transformation macros
2. global-transformation macros
3. local-expand-to-functor
4. local-expand-problem
5. local-expand-monad

I will attempt to explain those features in the context of a running example, a DSL for specifying routes in an http server, in the style of servant:

(routes
  -- GET /tasks/1234
  -- get details about a specific task
  (:>
    "tasks"
    (capture [task-id TaskId])
    (GET Task))

  -- GET /tasks
  -- list all the tasks
  (:>
    "tasks
    (GET (List Task)))

  -- GET /tasks/completed
  -- list all the completed tasks
  (:>
    "tasks
    "completed"
    (GET (List Task)))

  -- GET /tasks/todo
  -- list all the tasks which are not yet completed
  (:>
    "tasks
    "todo"
    (GET (List Task)))

  -- POST /complete?task-id=1234
  -- mark a specific task as completed
  (:>
    "complete"
    (query-param [task-id TaskId])
    (POST Unit)))

local-transformation macros

:> is a local-transformation macro, it takes n path components and expands into n-1 applications of a binary operator:

(:>
  "tasks
  "todo"
  (GET (List Task)))
=>
(binary-:> 
  "tasks"
  (binary-:>
    "todo"
    (GET (List Task))))

It is a local transformation in the sense that it merely reorganizes its input sub-terms while leaving the sub-terms untouched and unobserved.

global-transformation macros

Let's look at a global transformation next. Suppose the implementation of the http server looks at each route from top to bottom, and that a common bug is that the /tasks/:task-id route is listed before the /tasks/completed route, and therefore when the server receives a request for /tasks/completed, it incorrectly attempts to parse the string "completed" as a task id. Then it would make sense to define a global-routes macro which looks at all the routes defined within its body, spots the conflicts, and reorders them to avoid the bug:

(global-routes
  (binary-:> "tasks"
    (binary-:> (capture [task-id TaskId])
      (GET Task)))
  (binary-:> "tasks"
    (binary-:> "completed"
      (GET (List Task)))))
=>
(routes
  (binary-:> "tasks"
    (binary-:> "completed"
      (GET (List Task))))
  (binary-:> "tasks"
    (binary-:> (capture [task-id TaskId])
      (GET Task))))

This is a global transformation because global-routes had to examine the details of its sub-terms in order to find the conflicts. In general, a global transformation typically examines its entire input, and thus expects that entire input to have a specific shape; here, global-routes expects each route to be constructed via nested binary-:> applications, not via the n-ary :>. That restricted shape is inconvenient.

local-expand-to-functor

The next step is to eliminate that inconvenience by allowing local-transformation macros to collaborate with the global-transformation macro. The idea is that custom-core-routes specifies that it expects binary-:>, not :>, which tells the expander to expand :> but not binary-:>. This way, the user can use the nice :> syntax while the custom-core-routes implementation can parse the simple binary-:> syntax.

(custom-core-routes
  (:>
    "tasks"
    (capture [task-id TaskId])
    (GET Task))
  (:>
    "tasks"
    "completed"
    (GET (List Task))))
=>
(custom-core-routes
  (binary-:> "tasks"
    (binary-:> (capture [task-id TaskId])
      (GET Task)))
  (binary-:> "tasks"
    (binary-:> "completed"
      (GET (List Task)))))
=>
(routes
  (binary-:> "tasks"
    (binary-:> "completed"
      (GET (List Task))))
  (binary-:> "tasks"
    (binary-:> (capture [task-id TaskId])
      (GET Task))))

One way to implement custom-core-routes is via local-expand, by having custom-core-routes traverse its input and call local-expand whenever it encounters :> or any other symbol it does not recognize. I propose a fancier solution: custom-core-routes should instead call local-expand-to-functor, a polymorphic Macro action which in this case returns a (MyCore Syntax). One of the constructors of MyCore is my-binary-:>. Inside the body of custom-core-routes, the local-transformation macros are given the option of returning a (MyCore Syntax) value instead of returning a Syntax. For example, the binary-:> macro uses the my-binary-:> constructor.

The reason the type is (MyCore Syntax) and not just MyCore is two-fold:

1. it allows the expander to maintain hygiene by flipping the scopes on those Syntax values, and
2. it is a convenient type for the common case in which custom-core-routes recursively calls local-expand-to-functor on the Syntax values in order to obtain a fully-expanded (Fix MyCore).

The local-transformation macro should use (which-problem) to check if a (MyCore Syntax) value is expected, because the only place where the expander knows what to do with that value is in the outermost macro of the Syntax expanded by local-expand-to-functor. The (MyCore Syntax) is constructed in the same phase as the local-expand-to-functor call site which matches on that value, so this is effectively a dynamically-typed call with extra steps.

At that call site, custom-core-routes matches on a finite number of core cases (the MyCore constructors), and gives them meaning by transforming them into e.g. the Syntax for a function which receives a request and the implementation of an http handler, and chooses whether to call that handler or move on to the next route.

local-expand-problem

In some circumstances, we don't want a closed set of core cases, we want an open set to which other libraries can contribute. For example, capture and query-param are only two of many ways one might parse part of an http request for routing purposes, and it would be nice to be able to add more ways to parse routes without having to modify the library which implements the global-transformation macro.

If this was Haskell, then instead of a MyCore datatype, we would define a newtype wrapper around a function type (-> Bool Identifier Identifier (-> Bool Identifier Identifier Syntax) Syntax Syntax), and we would establish a convention explaining what such a function must do:

• the Bool indicates whether we're still parsing the path components or if we are now parsing the query parameters,
• the first Identifier argument is the name of the http handler, a function which receives all the values parsed from the route and returns the response,
• the second Identifier argument is the name of the part of the http request which remains to be parsed,
• the (-> Bool Identifier Identifier Syntax) argument is the success continuation,
• the Syntax argument is the failure continuation,
• the output Syntax should be code which parses part of the http request and either calls the success continuation or the failure continuation.

Since this is Klister, not Haskell, and we are not merely calling a function, we are making an indirect call via the expander, we must use a slightly different approach. Instead of a function from an input type to an output type, the global-transformation macro's module should define a custom Problem constructor (which must thus be an open type) wrapping the input type and specifying the output type (which is Syntax in this case, but could be something like (MyCore Syntax) as well).

Then, instead of hardcoding capture and query-param as the only two valid possibilities, the library would export those as two example macros which solve that Problem, and document how other libraries can do the same. custom-problem-routes would construct the appropriate continuations, wrap them in that Problem constructor, and pass it (and the syntax which might contain (capture [task-id TaskId]) or a library-provided alternative) to local-expand-problem. It would receive the output, in this case a Syntax, and use it to construct its own output, perhaps a function which takes an HList of handlers and an http request and calls the right one.

local-expand-monad

In Haskell, it is also very common for this kind of newtype to wrap a function which returns a monadic action. For example, if we implement a custom type system which uses its own MyType instead of Klister's Type, then the local-transformation macros might want to unify two MyType values or create new unification variables. Or, in our running example, maybe the library wants to provide a monadic API for consuming the next path component, so that under the hood it generates the code which examines the right part at runtime, without having to burden the implementation of the alternative-to-capture with the details.

It would thus make sense to have an expand-to-monad variant whose Problem specifies the input type, the output type, and the monad (which must support liftMacro) which the local-transformation macro is allowed to use.

[gelisam]

Here are some notes from a discussion with @david-christiansen about the above.

Scope

Mu'

One problem with the solution so far is that if the global-transformation macro encounters an error while processing a (Fix MyCore), then there won't be a Syntax around to attach to the error message, so its location will not be very helpful to the user. One solution would be to use this Mu1 instead of Fix:

(datatype (Mu1 f)
  (mk-mu1 Syntax (f (Mu1 f))))

If I remember correctly, you gave the following definition instead:

(datatype (Mu2 f)
  (mk-mu2 (f (Either Syntax (Pair Syntax (Mu2 f))))))

Which makes sense as an intermediate structure when the global-transformation macro is still in the process of expanding the Syntax objects at the leaves into f constructors.

open / close

We said that it would be annoying for users to manipulate values of type (Mu1 MuCore), but that perhaps Klister can provide a nicer API for values of this shape if we expect them to be common. In fact, we already have such a type, Syntax, which is secretly

(datatype Syntax
  (mk-Syntax Loc ScopeSet (Syntax-Contents Syntax)))

The API we have chosen for that type is

(the (-> Syntax (Syntax-Contents Syntax))
     open-syntax)
(the (-> Syntax Syntax (Syntax-Contents Syntax) Syntax)
     close-syntax)

which has room to improve (recursive matching will be easily solved with a macro, but having to specify the source location and scope set on every Syntax-Contents is unavoidably painful) but is much better than what we had before. So perhaps we could have

(the (-> (Mu1 f) Syntax)
     syntax-annotation)
(the (-> (Mu1 f) (f (Mu1 f)))
     open-mu1)
(the (-> Syntax (f (Mu1 f)) (Mu1 f))
     close-mu1)

Then once we find API improvements for open-syntax and close-syntax, they should hopefully carry over to open-mu1 and close-mu1.

[gelisam]

stuck macros

Since the goal is to give the programmer the expressive power to implement exotic type systems, it would be nice to provide support for Klister's own brand of exotism: stuck macros. We would like the global-transformation macro to be able to define a data constructor for Problem named my-expression which wraps a MyType, for the local-transformation macro to do a my-type-case on that MyType value, and to get stuck until some other task resolves the outermost type constructor.

We don't currently have a way for the global-transformation macro to spawn tasks, but we do plan to add more ways for macros to get stuck than just type-case. To implement type classes, we plan to implement something like a Map from identifier to instance. I imagine that such a Map could be used to implement a my-case-type which gets stuck.

[gelisam]

quadratic cost

the quadratic cost of local-expand

One issue which plagues Racket's local-expand is its quadratic cost. I always forget what is causing this quadratic cost, so I want to write it down in a separate section.

local-expand itself is linear: it traverses its entire input syntax object in order to expand everything inside it, from the root to the leaves.

The quadratic cost comes from the fact that local-expand is likely to be called n times on the same sub-tree. One reason is that macros tend to call themselves recursively. For example, maybe global-routes works as follows, by grouping the routes with the same head together and calling itself recursively on the tails:

(global-routes
  (binary-:> "tasks"
    (binary-:> (capture [task-id TaskId])
      (GET Task)))
  (binary-:> "tasks"
    (binary-:> "completed"
      (GET (List Task)))))
=>
(helper
  (binary-:> "tasks"
    (global-routes
      (binary-:> (capture [task-id TaskId])
        (GET Task))
      (binary-:> "completed"
        (GET (List Task))))))
=>
(helper
  (binary-:> "tasks"
    (routes
      (binary-:> "completed"
        (GET (List Task)))
      (binary-:> (capture [task-id TaskId])
        (GET Task)))))
=>
(routes
  (binary-:> "tasks"
    (binary-:> "completed"
      (GET (List Task))))
  (binary-:> "tasks"
    (binary-:> (capture [task-id TaskId])
      (GET Task))))

So if the route ending in (GET Task) has length n, the custom-core-routes version of that would end up calling local-expand on sub-trees containing (GET Task) n times.

The other reason is that program can contain multiple nested macro calls, so if n of them are implemented by calling local-expand, they might end up expanding the innermost sub-tree n times. For example, helper above is clearly calling local-expand in order for the global-routes call it contains to expand to routes.

the linear cost of local-expand-to-functor

The semantics of local-expand is that it recursively expands a Syntax from the root to the leaves, resulting in a Syntax which only contains special forms. This takes linear time, which becomes quadratic if there are n calls.

The semantics of local-expand-to-functor is that it expands the outermost macro application to a (MyCore Syntax), while leaving the sub-trees untouched (they are the Syntax elements of the functor). It does not recur down to the leaves. This takes constant time, so if there are n calls, the overall cost is linear, not quadratic.

with a directly-accessible Syntax, invariants must be re-checked

There is a second reason why local-expand has a quadratic cost. In the process of expanding a term from the root to the leaves, Racket's local-expand also scope-checks the term. It takes a possibly ill-scoped term as input, and produces a well-scoped term as output.

Racket's Syntax is a directly-accessible type, meaning it's an ordinary, non-opaque datatype which can be deconstructed using pattern-matching and reconstructed in a different arrangement. Therefore, the caller is free to rearrange this well-scoped output term into an ill-scoped term. So when an outer global-transformation macro receives that possibly-ill-scoped term and calls local-expand on it, local-expand has to re-traverse the entire term.

with a directly-accessible MyCore, invariants must be re-checked

While local-expand-to-functor by itself doesn't traverse the entire Syntax, suppose that the local-transformation macro and the outer global-transformation macro are trying to collaborate by producing and consuming a MyCore which satisfies some invariants. If MyCore is directly accessible, then the inner global-transformation macro might break that invariant, so the outer global-transformation macro should recheck it. If checking the invariant costs O(n) and there are O(n) nested global-transformation macros, then the overall cost is quadratic.

with an opaque MyCore, invariants don't have to be re-checked

MyCore is an ordinary datatype, so the usual solution applies: one module provides the local-transformation macro, the outer global-transformation macro, the MyCore type, but not the MyCore data constructors. Thus, the inner global-transformation macro, which is defined outside of that module, cannot manipulate the MyCore value and thus cannot break the invariant.

This solves the performance issue, but the downside of this approach is that the inner global-transformation macro cannot manipulate the MyCore value, thus limiting expressivity. Can we have our cake and eat it too?

with a partially-opaque Syntax, invariants can be re-checked quickly

Klister's Syntax is not a directly-accessible datatype, it uses the open/close API we described above:

(the (-> Syntax (Syntax-Contents Syntax))
     open-syntax)
(the (-> Syntax Syntax (Syntax-Contents Syntax) Syntax)
     close-syntax)

This API makes it possible to manipulate Syntax values as if they were directly-accessible. At the same time, it makes a type-level distinction between the otherwise-isomorphic types Syntax and (Syntax-Contents Syntax): a Syntax is guaranteed to satisfy the internal invariants, while (Syntax-Contents Syntax) does not.

This makes it possible for the invariant to be re-checked for cheap whenever close-syntax is called: the (Syntax-Contents Syntax) value contains some Syntax children which already satisfy the internal invariants, and there are many invariants for which it suffices to check the boundary between the parent and the children, without having to re-traverse the entire tree. The same trick can be used with MyCore if it is given an open/close API.

bottom-up invariants checking

For example, suppose we want our MyCore terms to be well-scoped. The normal way to check that a term is well-scoped is to start with an empty context, to add bound variables to that set when we go under a binder, and to check that every variables we encounter is within that set of variables which are known to be in-scope.

(datatype MyCore
  (var String) 
  (app MyCore MyCore)
  (lam String MyCore))

-- (-> MyCore Boolean)
(defun well-scoped? (e0)
  (let loop ([in-scope (nil)]
             [e e0])
    (case e
      [(var x)
       (elem? x in-scope)]
      [(app e1 e2)
       (and (loop in-scope e1)
            (loop in-scope e2))]
      [(lam x body)
       (loop (cons x in-scope) body)])))

The above algorithm proceeds from the outside in, but with close-my-core, we start from already-checked children and we want to add-and-check a parent, so we have to proceed from the inside out. So instead of guaranteeing that a MyCore term is well-scoped, we will instead incrementally calculate the set of free variables, and then at the top level we can check that the set is empty.

(datatype (MyCore-Contents A)
  (var String)
  (app A A)
  (lam String A))
(datatype MyCore
  (mk-my-core
    (List String)  -- free variables
    (Fix MyCore-Contents))

-- (-> MyCore Boolean)
(defun well-scoped? (e)
  (case e
    [(mk-my-core (nil) _)
     (true)]
    [_
     (false)]))

-- (-> (MyCore-Contents MyCore) MyCore)
(defun close-my-core (contents)
  (match contents
    [(var x)
     (mk-my-core
       (nil)
       (mk-fix (var x)))]
    [(app (mk-my-core vars1 fix-e1)
          (mk-my-core vars2 fix-e2))
     (mk-my-core
       (append vars1 vars2)
       (mk-fix (app fix-e1 fix-e2)))]
    [(lam x (mk-my-core vars fix-e))
     (mk-my-core
       (filter (/= x) vars)
       (lam fix-e))]))

Similarly, if we want our terms to be well-typed, we cannot lookup a variable in a context to find its type, we must instead build a context containing all the free variables and the type they were used as. This necessarily requires unification, even if the language's context only has monotypes, because the bottom-up algorithm doesn't have access to that context to look up that monotype. This means that the type of close-my-core must be (-> (MyCore-Contents MyCore) (Unify MyCore)) instead of (-> (MyCore-Contents MyCore) MyCore).

For languages with rank 1 universally-quantified types, which already require unification, the situation is more complicated. The bottom-up algorithm doesn't have access to the context to look up if a variable has a universally-quantified type, so it cannot instantiate the universality-quantified variable to a new unification variable at each use site. It has to account for both the monotype case and the universally-quantified case. It can do so by creating a new unification variable for each use site, and storing the list of all the unification variables which have been created for a given variable. If it later turns out it's a monotype (e.g. the variable is bound by a lambda), unify all those unification variables together. If it later turns out it's a known universally-quantified type (e.g. a top-level definition with the type signature id :: forall a. a -> a), then once for each use site in the list (e.g. (id :: ?1) "hello"), instantiate the universality-quantified variable to a new unification variable (e.g id :: ?2 -> ?2) and unify the resulting monotype with the use site's unification variable (e.g. ?1 ~ ?2 -> ?2). Generalization isn't too hard either.

It is reassuring that impending an efficient type checker is possible, but since creating custom typed DSLs is likely to be very common in Klister, it makes sense to go the extra mile and attempt to make it easy.

[gelisam]

LF

Beluga

The Beluga programming language is also focused on letting the programmer define a custom typed DSL and then manipulate its well-typed terms. It would thus make sense to take some inspiration from it.

First, a short note about the difference between Beluga and Klister, so we understand which parts make sense to borrow and which parts don't. In both languages, the phase 1 code manipulates phase 0 terms. In Beluga, the phase 1 type system guarantees that all phase 0 terms are well-typed. In Klister, a Syntax value is allowed to contain malformed, ill-scoped, and ill-typed code, and the mistake will be caught while phase 1 runs rather than when phase 1 is type-checked.

To complete the picture, in a dynamically-typed language, the mistake would be caught when phase 0 runs, at runtime. These are three points on a spectrum where errors are caught later and later but the programmer has less and less onerous obligations towards the compiler, with Klister occupying a sweet spot between two extremes.

Anyway, in Beluga, the AST of the phase 0 terms, their types, and their typing rules are all defined via the LF syntax:

tp : type.
tm : tp -> type.

% types
unit_tp : tp.
arr : tp -> tp -> tp.

% terms and their typing rules
unit_tm : tm unit_tp.
app : tm (arrow A B) -> tm A -> tm B.
lam : (tm A -> tm B) -> tm (arr A B).

Beluga then uses those LF rules to guarantee that a constant like [ |- app unit_tm unit_tm ] is rejected when phase 1 is compiled. Similarly, a phase 1 function like the following should also be rejected, because it attempts to construct that same ill-typed term from smaller pieces.

let apply_unit_to_unit
  : [ |- tm unit_tp ]
 -> [ |- tm unit_tp ]
 -> [ |- tm unit_tp ]
  = fn unit1
 => fn unit2
 => case unit1 of
      [ |- UNIT1 ] =>
        case unit2 of
          [ |- UNIT2 ] =>
            [ |- app UNIT1 UNIT2 ]

let nonsense
  : [ |- tm unit_tp ]
  = apply_unit_to_unit
      [ |- unit_tm ]
      [ |- unit_tm ]

typechecker from LF

Again, in Beluga, that function is rejected when phase 1 is type-checked, whereas in Klister, we would like the corresponding code to fail when phase 1 runs.

(meta
  -- (-> MyCore MyCore (Unify MyCore))
  (defun apply-unit-to-unit (unit1 unit2)
    (close-my-core (app unit1 unit2)))

  -- (Unify MyCore)
  (define nonsense
    (do unify-monad
      (<- unit1 (close-my-core unit-tm))
      (<- unit2 (close-my-core unit-tm))
      (pure (apply-unit-to-unit unit1 unit2))))

This can be achieved in the way we described in the previous section: by having close-my-core type-check the term being constructed in a bottom-up way.

(datatype MyType
  -- unit_tp : tp.
  (unit-tp)
  -- arr : tp -> tp -> tp.
  (arr MyType MyType)
  -- unification variable
  (uni-tp UniVar))
(datatype (MyCore-Contents A)
  -- unit_tm : tm _.
  (unit-tm)
  -- app : tm _ -> tm _ -> tm _.
  (app A A)
  -- lam : (_ -> tm _) -> tm _.
  (lam String A)
  -- variable
  (var String))
(datatype MyCore
  (mk-my-core
    (Map String MyType)
    MyType
    (MyCore-Contents MyCore)))

-- new-univar :: (Unify MyType)
-- unify :: (-> MyType MyType (Unify Unit))
-- unify-vars :: (-> (Map String MyType) (Map String MyType) (Unify (Map String MyType)))

-- (-> (MyCore-Contents MyCore) (MyMonad MyCore))
(define (close-my-core contents) 
  (case contents
    -- unit_tm : tm unit_tp.
    [unit-tm
     (pure (mk-my-core empty-map unit-tp unit-tm))]
    -- app : tm (arrow A B) -> tm A -> tm B.
    [(app (mk-my-core fun-vars fun-tp fun-tm)
          (mk-my-core arg-vars arg-tp arg-tm))
     (do unify-monad
       (<- tpA (new-univar))
       (<- tpB (new-univar))
       (unify fun-tp (arr tpA tpB))
       (unify arg-tp tpA
       (<- vars (unify-vars fun-vars arg-vars))
       (pure (mk-my-core tpB vars (app fun-tm arg-tm))))]
    -- lam : (tm A -> tm B) -> tm (arr A B).
    [(lam x (mk-my-core body-vars body-tp body-tm))
     (do unify-monad
       (<- tpA (new-univar))
       (<- tpB (new-univar))
       (unify-vars (singleton-map x tpA) body-vars)
       (unify body-tp tmB)
       (pure (mk-my-core (Map.delete x body-vars) (arr tpA tpB) (lam body-tm))))]))

This code closely corresponds to the LF definition, but is much longer. In order to simplify the programmer's life, it thus seems plausible that we can write a macro which takes an LF definition as input and produces the typechecker above as output.