Substructural Types in ABC

Awelon Bytecode (ABC) has two operators, `k` and `f`, to support modeling of substructural constraints. In ABC, `k` will mark a block no-drop (relevant), and `f` will mark it no-copy (affine). If both marks are applied, the block is effectively linear. These properties can be enforced dynamically if necessary (i.e. halt the program upon attempted violation), but the intention is that they should (as much as possible) be checked statically.

A ‘block’ is simply a first-class function in ABC. Though, unlike first-class functions in many languages, a block in ABC always has a serializable form as a finite sequence of ABC – e.g. `[rwrzw+l]` will add two numbers on the current stack of AO’s standard environment. The primary operations on blocks are to compose two blocks, and to apply a block to a value.

o :: (y→z) * ((x→y) * e) → (x→z) * e -- compose (concatenate blocks)
$ :: (x→y) * (x * e) → (y * e)  -- apply block to just `x`; hides `e`
k :: (x→y) * e → (x→y)' * e -- mark block no-drop (relevant)
f :: (x→y) * e → (x→y)' * e -- mark block no-copy (affine)
^ :: (Copyable x) ⇒ x * e → x * (x * e) -- copy
% :: (Droppable x) ⇒ x * e → e -- drop

Sadly, I don’t have a good pseudo-type-descriptor notation for affine and relevant attributes at the moment. Suggestions are welcome.

Anyhow, the `no-copy` property simply means that the copy operator `^` may not be applied to the value. And the `no-drop` property means that `%` cannot be applied. If we mark a first-class addition function relevant, it would serialize simply as `[rwrzw+l]k`. When composing blocks, the composite inherits the no-drop and no-copy properties from the operands, i.e. if we compose affine with relevant the result is linear. The only way to remove a relevant or linear block from the environment is to apply it using `$`.

Why Substructural Types?

Substructural properties are very expressive for enforcing various kinds of structured behavior independently of a structured syntax. This is a useful separation of concerns, which leads to simpler code and reasoning.

By ‘structured behavior’ I mean for example enforcing that some operation occurs ‘at least once’ or ‘at most once’ or ‘exactly once’ or ‘before/after/between some other operations’. A typical example might be enforcing that a resource (e.g. an open file handle) is released exactly once and not used after release. But we can look at much richer examples, e.g. protocols, games, trade models, or workflows.

Conventional languages have a relatively rigid structured syntax. Fortunately, clever developers have consistently been able to leverage this structure to enforce, or at least discipline, higher level structured behaviors. For example, if we want to enforce that a file is released, we might develop a `withFile` function of (pseudo-Haskell) form:

withFile :: (MonadIO m) ⇒ (FileHandle → m a) → (FilePath → m a)

And this `withFile` function will acquire the file resource, apply the given function, then release the file resource. We could also develop a variation with MonadException to properly bracket the action for a monad that models exceptions.

Unfortunately, the `withFile` behavior is still not entirely safe! In `withFile action “foo.txt”`, our `action` might fork another thread to process the handle, or install a callback or return a closure or exception that contains the handle. In these cases, we might accidentally use the file handle even after the file has been released. The `withFile` pattern requires some discipline to use correctly, and implementation knowledge of the `action`, both of which tax our limited mental budgets.

So what can we do?

Well, one option is to develop a syntax – or EDSL (e.g. a monad or category) – that can control aliasing and enforce safe use of the file handle and similar `(Acquire Use* Release)` pattern resources. My intuition is that this wouldn’t be especially difficult for a single resource at a time – e.g. executing `action` within some variation of the StateT or ReaderT monad transformer should work well enough. Leveraging algebraic effects (or heterogeneous lists, or dependent types) we might effectively mix operations on multiple resources.

Developing an EDSL or structured syntax takes its own form of discipline, but it only needs to happen once per resource-pattern. It’s a decent approach if you wish to pursue it in a closed system. However, it can be difficult to integrate such an EDSL with independently developed frameworks.

Substructural types offer a simple – almost simplistic – alternative that greatly reduces the need for structure in the syntax. If we want an `(Acquire Use* Release)` pattern, we can almost model this directly. Example API:

type File (affine)
type OpenFile (linear)
type Command (regular)
acquire :: File → OpenFile
use :: OpenFile → Command → (OpenFile * Result)
release :: OpenFile → File

With this API, we can easily reason that an open file cannot be forgotten, that it is either closed or accessible. More importantly, our reasoning is context-free, beyond assuming that our context understands and enforces substructural types. We aren’t constrained structurally – e.g. we can easily use an OpenFile together with callbacks and coroutines or mashup with other ad-hoc resources, so long as the protocols are compatible. Additionally, we can reason that a file is not used by more than one thread, assuming we constrain how the `File` type is acquired in the first place (e.g. via a FileSystem object).

In ABC, objects such as files would be modeled using blocks, to which we can pass messages/commands. When serialized, an open file might look like: `[{openFile:42}]kf`. Text within {} braces is called ‘capability text’ and cannot be forged from within ABC. In open systems, capability text would generally be encrypted or include an HMAC to ensure security.

Files have a relatively simple, albeit common, life cycle pattern.

But much richer workflows, protocols, even games are possible. Substructural types combined with basic structured types and value sealing (or ADTs) are capable of enforcing any behavior protocol a context-free grammar can describe. If we also have dependent types, we can address context-sensitive behavior patterns. Of course, substructural types don’t hinder modeling of monads, categories, EDSLs, etc., which still serve a useful role for staged computing.

Substructure for Concurrency

ABC is a non-strict, implicitly concurrent language/bytecode. Relevantly, if you apply some ABC of the form:

-- apply two functions in parallel! (cf. '***' in Control.Arrow)
rzwz$wzwr$wl :: ((x1→y1)*(x2→y2)) * ((x1*x2) * e)  → ((y1*y2)*e)

Then we can compute y1 and y2 independently and in parallel, even if the functions are effectful. This property is also called causal commutativity – i.e. two operations commute if they don’t have a direct data dependency. Substructural types in ABC serve a significant role in ensuring deterministic behavior, by partitioning resources so that parallel subprograms never operate on the same resource. A rich resource partitioning model can be expressed using substructural types.

This isn’t a new idea. Other languages with similar properties include ParaSail, Clean, and Rust, and the languages that influenced them.

ABC also requires a related property for any effects model, which I call spatial idempotence: if the same function is applied twice to the same argument, it must return the same result and have no additional effect. Mathematical idempotence: ∀f . f f = f. Spatial idempotence: ∀f . dup [f] apply swap [f] apply = [f] apply dup. Together, spatial idempotence and causal commutativity offer ABC many of the equational reasoning benefits of pure code. (Basically, I get everything but dead-code elimination: I cannot eliminate a potentially effectful application simply because I ignore the result.) However, in practice, it is not easy to enforce spatial idempotence for arbitrary side-effects. Substructural types also play a role here: the spatial idempotence constraint cannot be violated (and is thus satisfied) if we forbid ‘dup’ for effects on otherwise problematic resources. Substructural types are, hence, essential if ABC is to work with conventional imperative effects.

(ABC is designed primarily for a new paradigm, RDP, for which spatial idempotence and causal commutativity are far more natural. Requiring these properties universally – even for programs in the imperative paradigm – is a boon for independent optimizers and analysis tools.)

Linear Structure for Simplified Memory Management

Memory is also a resource. Some people have pursued linear types to help control use of memory resources, e.g. to eliminate need for garbage collection without creating an undue burden of detail and discipline on the developer. Henry Baker’s paper on Lively Linear Lisp comes to mind, as does the Cyclone language with reification of memory regions.

Simplified memory management is NOT a significant motivation for ABC’s linear structure. But, as an additional benefit, it isn’t bad. 🙂

If ABC’s copy operator `^` is implemented using a deep-copy under the hood, then we really can eliminate garbage, and ABC’s primitive functions can be implemented using mutators. If copy is instead implemented using an aliased reference, then we’ll still need garbage collection and more conventional allocation of persistent data structures. I’m interested in exploring mixed/hybrid approaches based on global program analysis, and also the possibility of using separate heaps whenever I parallelize large computations.

ABC (and the thin human language layered above it, AO) tend to encourage linear programming idioms, minimizing use of copy and drop and favoring moves and data shufflers. That said, it isn’t especially difficult to statically optimize copy and drop, e.g. by eliminating dead copies.

As an aside: structural typing lends itself more readily than nominative typing to substructural constraints. If we have generic nominative types like `struct Point[a] { x : a, y : a, z : a }`, it becomes difficult to pick it apart to operate on just `x` or just the `x y` pair. Structural types allow us to pick apart objects, operate on the pieces, and reassemble them, maintaining substructural properties at every intermediate step – i.e. correctness by construction instead of by analysis. Similar can be said for parameters to functions, and why tacit programming tends to serve well for substructural types.