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.

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

5 Responses to Staging is Simpler than Type Checking

  1. Pingback: Types of discontent: a tale of how and what | werglog ii

  2. naasking says:

    Is compilation guaranteed to terminate?

    • dmbarbour says:

      Awelon’s compile-time is Turing complete. The equivalent of `forever = (λx.(x x) λx.(x x))` is pretty much `forever = [dup apply] [dup apply] apply`. In this sense, compilation is not guaranteed to terminate. It can run ‘forever’.

      OTOH, I would certainly place a quota on how much space and effort is spent trying to compile a program. Therefore, in practice, compilation always terminates. There are many advantages to having the Turing complete element be the compile-time rather than the runtime, such as: we don’t have any half-completed IO or negotiations left in limbo status. And it’s easier to offload the compilation to a parallel service. Developers are free to think inconsistent thoughts, so long as they lead to a consistent artifact. (As PLT HULK says: IT BETTER IF YOU TYPE SYSTEM AM TURINGS COMPLETE RATHER THAN YOU LANGUAGE!!!)

      I have mixed feelings about a non-terminating compilation, but I don’t have mixed feelings about the expressiveness and simplicity it offers.

      • Sandro says:

        Well, in practice every computer will eventually break down, so there really are no such things as non-terminating programs. It seems quite difficult to set a practical limit on space or time used during compilation. How could you possibly gauge it reliably?

        Have you considered some sort of type-based termination analysis, like sized types?

      • dmbarbour says:

        Fortunately, in a distributed RDP system, there is an easy way to gauge how much effort should be expended on computing a function: just take the expected latency for the behavior, then add a little based on anticipation and expected stability. That’s it.

        If clients wish to compute painfully expensive functions, they can be politely asked to use a little indirection through an intermediate ‘compiler’ service. One idea I like is to just ask clients to provide their own quota – perhaps in terms of how much they’re willing to be charged for a service.

        A thought: in practice, a compilation that performs some exponential search on a large constraint set, or that naively computes a large fibonacci number, is not better than one that computes forever. The main advantage of a terminating language is not that it results in more practical programs. Rather, a language that guarantees termination is more likely to avoid accidentally creating a long-running program.

        I have considered size-based types and a few other ideas, but I didn’t really like how they limited expressiveness. E.g. if I want to model aspect-oriented advice in the named stacks along with explicit join-points `"foo" signalAOP`, this can easily result in recursion unless developers are disciplined to avoid join points in their AOP advice. But if I try a termination analysis, it becomes very difficult to even begin modeling AOP.

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