Staging is Simpler than Type Checking

I’m taking an unusual approach to types with Awelon, one that I hope will work better than traditional approaches. Instead of “type checking”, every Awelon program represents a compile-time program. If this compile-time program completes without errors, then the runtime behavior will be type safe.

The runtime behavior of Awelon is described by an arrow representing a reactive demand programming behavior. If you aren’t familiar with arrows, the TLDR concept of arrows is: “Oh, someone formalized box-and-wire programming. Meh.” Arrows are more expressive than simple pipelines since we can branch dataflows and recombine them, and arrows are quite useful for many problems. But, as a general purpose programming model, arrows tend to have the same weakness of box-and-wire paradigms: they become very unwieldy for certain real-world problems or at large scales. It’s all those little exceptions and messy real-world problems – configuration tweaks, singleton hub-nodes, and shotgun policies – that make a mess of the grand pipe-dream.

Fortunately, compile-time metaprogramming can enable these box-and-wire paradigms (minus the boxes and wires) to scale much larger. The more painful non-local wiring logic can be automated, and hub nodes are easily integrated without messy wire crossings. Configuration details can be represented as scoped environment variables, enabling different configurations for different subprograms.

What Awelon does is use its compile-time metaprogram as an implicit typecheck.

Awelon’s compile-time behavior is similar to (but completely different from) FORTH, Factor, and other concatenative languages. Developers do manipulate a stack of objects: they can add text and numbers or blocks of code, and operate on them in all the expected ways. If developers wish, they can use a number and iterate a function that many times. But there are also ‘runtime’ typed values – e.g. for future signals representing time-varying mouse position. Developers can operate on future signals, e.g. by specifying how they will be handled, or applying functions to combine or transform them. But the result of these operations are not visible to developers.

In addition to simple numbers, text, simple blocks, and runtime values, Awelon supports more exotic types, mostly at compile-time. There is the uniqueness source. There can be unique values constructed from this source – e.g. sealer/unsealer pairs that operate at compile-time, or GUIDs. There will be affine, relevant, and linear types to help model requirements and responsibilities. I am considering fractional and negative types to model promises or futures (if I can figure out how to model them without hindering visualization; maybe as a growing set of type-constraints).

A rather interesting property of RDP and Awelon is that runtime values have spatial-temporal information: every runtime signal has a partition (a logical location) and a latency value (a relative time that the signal becomes available). To combine two runtime signal values – e.g. to test mouse position against a window’s box size and location – requires that the signals have the same time and space coordinates. These partitions can also be used as a basis for security. Some partitions provide ambient authority. Some support capability-security by generally being confined but where some sealed behaviors can reach into the parent ambient partition. Some partitions may truly be confined, to enforce isolation if we want it. (Awelon will not do ‘sandboxes’, i.e. partitions with a limited subset of ambient authority. Those are just horrible.) An interesting feature I’m considering is latency-constraints in the type model: e.g. capabilities that expire if they’re not used within so many milliseconds. This could be useful for controlling how distributed systems communicate, how code is moved.

Awelon is very richly typed. Anyhow, Awelon’s “type checker” is simply the execution of this compile-time program. The compile-time is picky about types, is relatively simplistic, and doesn’t perform any coercions. But, if no errors are raised, and if the compile-time program terminates, the result will be a safe runtime behavior. This is safety by construction.

Fortunately, for the sanity of developers, Awelon does support type introspection, so it is possible to create programs that adapt to their inputs. With careful use of fractional types, it may also be possible to adapt to output types.

Unlike FORTH and most concatenative languages, Awelon’s compile time is effect-free and has a very rich ‘environment’ type. There is a stack. But Awelon also provides a whole set of named stacks that provide scoped configuration variables, singletons or hubs, compile-time databases, separate tasks or workflows, and so on. Awelon can easily represent ad-hoc complex structures – e.g. multi-media documents, diagrams, DSLs, ADTs, objects, zippers, lenses, and traversals – in its compile-time behavior. (Since it’s all in the compile-time, it is also readily visualized or rendered by an IDE.)

Runtime Flexibility and Types

Another issue with arrows is that they’re inflexible at runtime. There are ways to regain flexibility, such as:

• collection-oriented behaviors, i.e. applying a single arrow to each element in a runtime vector or set
• dynamic behaviors, i.e. providing an arrow as a runtime input to specify the runtime behavior of a static arrow

I wonder, in practice, whether these are truly needed. A great deal of flexibility can be achieved using static structures – e.g. using four tiling layers and a fixed set of tiles, SNES developers create very dynamic user interfaces. Further, RDP is carefully designed for runtime update: when we need more ‘flexibility’ it would often be easy to achieve it by extending the program code.

OTOH, RDP is also designed so that dynamic behaviors are updated just the same as their host application in a staged, metacircular manner. I see no reason to waste that. For Awelon, I plan to support both collection-oriented and dynamic behaviors. (Static collection-oriented behaviors need no extra support, so primitives only address the dynamic vectors or sets.) Dynamic behaviors in Awelon are second-class – very constrained on their input and output types. But even with those limits, they are potentially quite useful.

One feature Awelon lacks under its current design is the inability to prove a dynamic block will have the right type for a dynamic behavior without actually executing the associated compile-time code. We have safety-by-construction, but we don’t have safety-before-construction that can be validated without basically repeating the construction. I have a few ideas, but I am still thinking about how to best address this.