Source-Stable Uniqueness

Live programming, continuous deployment, orthogonal persistence, debugging – a quality these have in common is that we want state to remain stable across external interference, i.e. so we don’t lose important work. One mechanism to achieve this is to externalize state, e.g. keep it in a database, or carefully save and restore in a manner that won’t break across version changes. But many developers dislike external state: in many cases it is nice to know we have exclusive control over state, or that we can hide implementation details (like how state is organized) from other subprograms. Fortunately, linear or uniqueness types are simple, powerful tools to regain exclusivity and implementation hiding.

But uniqueness and linear types don’t automatically promise stability across code changes. A naive application of uniqueness types might simply assign each ‘new’ state a unique, incremental name (1, 2, 3, 4, etc.). But this assignment would not be stable to changes that inject stateful code, or rearrange code, or change how many names a subprogram uses. We need to do better.

The simplest basis for stable names I know is the filesystem-tree. So that is what I use.

The uniqueness source, U!, models a directory structure. Developers can fork a new uniqueness source – a new subdirectory – but it must be explicitly named. Further, upon doing so, that name cannot be reused by the parent directory.

fork :: (Text * U!)~>((U! * U!') | NameAlreadyUsedError)
new :: ((Text * Model) * U!) ~> ((State of Model * U!') | NameAlreadyUsedError)

The forked subdirectory structure ensures that subprograms do not interfere with one another, essentially ‘chrooting’ each subprogram. The Text naming each subdirectory provides the stability – i.e. each subprogram is uniquely named in source, and unless those names change the program will be stable to reorganization or injecting new subprograms.

Note: It would not be difficult to represent fork/new in the type system, i.e. to statically enforce uniqueness. Haskell, C++, C#, all have expressive enough type systems to do it… but we really need linear or affine types for U!.

There are a couple remaining issues.

First, “upgrades” to the state models: implementation hiding doesn’t help if we get chained to the past. Fortunately, this can be addressed if our `Model` for state can explicitly contain information on how to update/convert from prior state models, and each model includes a version identifier.

Second, extension, introspection, and observation: it is sometimes useful to bypass implementation-hiding in a secure way, i.e. so that the larger subprogram can extend subprograms in ways the original developers did not foresee. This might be achieved by introducing weak identifiers to reach into subprograms. These might be observer-only, or allow constrained interference based on the state model.

forkWeak :: (Text * U!) ~> (UW * U!)

With forkWeak one would not be able to interfere with parent or sibling processes because one doesn’t have the parent’s uniqueness source. But one could extend, audit, etc. the subprograms, and debugging would have a more formal explanation within the language.

In Awelon, I will use a uniqueness source, primarily in a static manner, to uniquely bind external state to subprograms at compile-time. I plan to support the sort of extensibility I mentioned here. Awelon programmers will thus achieve all the convenience of ‘local state’ (such as potential to embed state directly in a live programming ‘canvas’) without any of the poison.

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 )

Twitter picture

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

Facebook photo

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

Google+ photo

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

Connecting to %s