Lambda the Ultimate

Sorry for the long post. This is really a pretty simple idea, but I want to make sure I’m explaining it correctly. I don’t have a background in programming language theory, so I find I have to describe my motivation to communicate this idea to people who do. Skip everything except the idea and the questions if you’d like.

Idea

The idea is to allow trusted code to restrict what global variables untrusted code can access. Every top-level module and procedure would be a global variable, and every side effect would require access to some global variable, so we could effectively sandbox code and control side effects this way. It seems to me that this could be enforced with a statically checkable type system. Could it not?

Motivation

I’m interested in languages that help programmers enforce the principle of least authority. One such language, E (www.erights.org), is basically Java without global variables. That means an object cannot import anything from the Java API; everything has to be passed to it as a reference. One parent object starts out with access to everything and delegates authority to objects as it needs to by passing references.

Some other languages take an approach similar to E’s, allowing the programmer to sandbox code by restricting but not eliminating the ability to access global variables. Lua and Python sandboxes can be built this way:

Lua Sandboxes

And Racket does something similar:

Racket Sandboxes

I think the approach that Racket and Lua take is more natural, since it is a little cumbersome to pass a reference whenever you want to do something. (E also tries to allow for secure distributed computing, so that approach might not make sense for E.) All of these approaches share two properties: they are strong enough to run untrusted code, and they work at runtime. Python and Lua modify dictionaries that code uses to look up global variables, and the Racket sandbox restricts the evaluator’s access to read certain files, which prevents it from importing certain modules.

Monads and effect types are also strong enough to allow running untrusted code, but they are statically checkable. Code operating in a particular monad will never be able to break out of that monad and do something that monad cannot do. Both monads and effect types, however, seem difficult for programmers to manage.

The idea above essentially combines the natural approach of Lua and Racket with a static type-checking system.

Response so Far

I sent a message to bitc-dev, basically asking about applying this idea to BitC. Jonathan Shapiro was kind enough to respond. Here is the thread:

BitC thread

I didn’t want to take up too much space on the BitC list, but I’m not sure why effects couldn’t be scoped the way I’ve mentioned. I’m interested in a fuller answer from anyone who is interested.

He mentioned that a higher-order language would present some complications. A procedure f that is passed another procedure g as a parameter and calls it would have to add all of the variables referenced by g to its effect type. That would be tricky because the inferred type of f would depend on what g a caller was using. Everything is still decidable, but I don’t have any experience with compiler design, so I don’t know how practically difficult it would be to implement this type system efficiently. It seems like a solvable problem.

He also pointed out that my idea would pose a problem for separate compilation of modules: if we linked in a compiled object file containing method definitions, we would lose information about the global variables that those methods had accessed. I personally don’t mind the idea of requiring everyone to include source code (or a compiler-generated proof?) along with their modules, but I wonder if this would slow down compilation. Again, I don’t have the expertise to say.

Questions

I'm wondering,

1. Has something like this been done before? In particular, I'm very interested to know if a language exists that has implemented the idea above with a type system.
2. Could this idea be enforced with a type system in a fast compiler?
3. How difficult would it be to extend a compiler for Racket, OCaml, or some other language to incorporate this idea into its type-checking system?
4. Suggestions for further reading would be appreciated.

Thanks for your thoughts!