Lightweight Staged Programming for Awelon

Multi-stage programming is essentially disciplined partial evaluation, a widely useful optimization technique especially in context of DSLs. By ‘disciplined’ I mean programmers can comprehend and control when computations occur, and statically debug staging errors. This is valuable for avoiding hidden performance regressions.

Yesterday, I was inspired and found a simple way to support multi-stage programming in Awelon by introducing two annotations:

[F](now) == [F]     iff [F] doesn't contain (now)
[F](later)          masks F from analysis by (now)

For Awelon, partial evaluation is simplified by lack of entanglement with variable environments and local rewrite semantics.  Hence annotations do not need to drive partial evaluation. They only offer means to declare requirements and debug errors – provide some discipline. I can separately develop models (DSLs, monads, etc.) for convenient multi-stage programming.

The (now) annotation is essentially an assertion that peeks deep into otherwise opaque representations. The (later) annotation enables abstraction of staging requirements and working with more than two stages. Global function definitions should be implicitly staged, such that unmasked (now) indicates static evaluation in that context, and we can safely assume named functions are statically stage safe after compilation.

These annotations can be checked dynamically, but it’s feasible to statically compute whether runtime staging will be correct, assuming we know the arities of all the things. Our inferred types would need to record for each input whether any (now) annotation will be exposed due to partial evaluation if just that many inputs are provided.

Aside: Use of (now) and (later) is inspired from temporal logic. Temporal logic is a a natural fit for multi-stage programming, but I think most languages wouldn’t support such a lightweight adaptation.

This entry was posted in Language Design. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s