Lambda the Ultimate

A Generic Type-and-Effect System

Type-and-effect systems are a natural approach for statically reasoning about a program's execution. They have been used to track a variety of computational effects, for example memory manipulation, exceptions, and locking. However, each type-and-effect system is typically implemented as its own monolithic type system that hard-codes a particular syntax of effects along with particular rules to track and control those effects. We present a generic type-and-effect system, which is parameterized by the syntax of effects to track and by two functions that together specify the effect discipline to be statically enforced. We describe how a standard form of type soundness is ensured by requiring these two functions to obey a few natural monotonicity requirements. We demonstrate that several effect systems from the literature can be viewed as instantiations of our generic type system. Finally, we describe the implementation of our type-and-effect system and mechanically checked type soundness proof in the Twelf proof assistant.

Things really seem to be heating up in both the type-and-effects world and the mechanized metatheory world (but then, long-time LtU readers will expect me to claim that, won't they)? Of course, I also have my usual question as to what aspects of Twelf these researchers found helpful to their constructions vs. those of Coq.

Although my motivation is financial systems, I use the example of computer games to make the discussion appeal to a wider audience.

Assume there is an on-line video game which has tens of millions of users. The game is some sort of strategy game with armies, battles, shootouts, etc. Although most players control everything manually, the game provides a way for players to script their actions. For example, a script could tell three soldiers to spread out in a triangle whenever they see a certain monster. Another script could have the workers automatically produce new soldiers as old one die out.

In this scenario, it makes sense to provide a proprietary, domain specific, scripting language that lets players cause all kinds of mayhem with virtual guns, but doesn't allow formatting the local disk drive.

As the game becomes more popular, some players demand more features in the scripting language. They wish to do monte-carlo simulation to figure out the possible outcomes of an attack. They wish to buy third-party scripts and integrate them into their own scripts, etc.

The game writers decide that they should create a general purpose language. They write their game engine in this general purpose language and accept scripts in the same general purpose language. This allows a community to grow around the language, with nice tools, libraries, compiler/interpreter optimizations, etc. However, this language must have the ability to control what these 'injected' scripts can do. Obviously these scripts can't modify the game engine, itself, they can't access the local disk, they can't create data-structures that eat up all the memory, they can't hog all the cpu, etc.

What kind of language is this? What real-world examples are there that do this or what papers describe such systems?

To partially answer this: the most obvious example is Java and its applet infrastructure. Applet writers embed their programs in web-pages, and don't generally have the ability to access random parts of the local disk, nor do they have the ability to open any tcp/ip ports. Applets, however, don't describe how they can be embedded into a general purpose server--their interaction is strictly defined for a browser and nothing else (as far as I know).

Lisp/Scheme system provide the ability to change running code. The clojure folks have an amazing (to me) example where a programmer telnets into his server and changes a servlet as it is serving pages to users. Other languages provide the ability to interact with the server: Erlang and Java (via osgi) come to mind. However, these interactions don't necessarily happen in a safe enough manner. They are certainly not designed to host little programs from millions of users whose competence and ethics may vary.

Haskell provides a way to keep pure code separate from code with side-effects. Perhaps the server only accepts pure Haskell code, thereby ensuring users don't do any I/O. However, Haskell also desn't have a good way of 'dynamically loading' code (hs-plugin is not very pleasant to use). I may wish to stop users from doing disk I/O, but they shouldn't have to jump through hoops to generate random numbers or mutate local state.

It seems to me that the right language to allow such a system would have the ability to control effects: but do so at a very granular level: permission for non-deterministic code, mutable state, I/O, etc. need to be controlled separately. How would one ensure that CPU time or memory is used fairly? How could the server writers make sure use scripts actually terminate (no infinite loops or recursions, beyond the global event loops which exists as long as the game continues)?

Can type/effect systems solve this? Is this better handled by virtual machines or run-time checks?

Other examples where such a system can be useful:
-Financial exchanges which let people submit little programs, rather than single commands to buy/sell securities.
-Car computer systems which let drivers embed their programs to enhance the dashboard
-General programming languages which let users provide their own implementation of interfaces (such as Comparable in Java), but ensure that these implementation don't have access to disk/networks, etc.