Lambda the Ultimate

...is very much in the question of how to do object-capability security a là E in a sufficiently expressive statically-typed language these days. My dream language would be something like a capability-secure Acute, except with syntax that won't scare C++/Java/C# programmers away. This is why I'm so interested in Tim Sweeney's work and so curious as to how he might be addressing security in it, since he made no mention of security in his "The Next Mainstream Programming Language" presentation. Tim, any comments? :-)

It's possible to have a "statically typed E" right now given this appropriate type system for first-class messages:

http://www.eros-os.org/pipermail/e-lang/2005-June/010711.html

I think that's plausible. But I also doubt it's an obvious or trivial undertaking[*]. It'd be especially cool if such an efforts also tried to fold in insights from Oleg and Shan's "Lightweight Static Capabilities". If anyone would like to try defining such a language, I'd be happy to help.

[*]In particular, AFAICT, the type system described in Shroff and Smith's Type Inference for First-Class Messages with Match-Functions, either by itself or in combination with Lightweight Static Capabilities, is still not be expressive enough to allow the membrane pattern.

(Not that I actually understand either one. I'm still a lightweight when it comes to type theory formalisms.)

I'm keenly interested in attempting to implement the membrane pattern as widely as possible. My short list of targets would be:

• MetaOCaml
• O'Caml leveraging "Lightweight Static Capabilities"
• Scala, either via metaprogramming or the moral equivalent of "Lightweight Static Capabilitites"
• Haskell, presumably leveraging "Lightweight Static Capabilities"
• Oz, in the guise of Oz-E

It seems to me extremely fortuitous that we have Mark Miller, Oleg Kiselyov, Peter Van Roy, and many other folks who, while not the authors of the systems and/or papers in question, are nevertheless expert in the use of programming languages to solve such thorny problems here on LtU. Can we somehow make a cross-language LtU project of this—kind of our own ICFP challenge? I think we'll learn a tremendous amount about the relationship among metaprogramming, static typing, and dynamic typing, as well as increasing the community's understanding of object-capability security, and even winding up with multiple implementations of some core technology. I literally can't think of anything else I'd rather be doing right now. Is anyone else interested?

Mark, FWIW, a year ago I was in your shoes. Let me highly recommend working through Pierce's "Types and Programming Languages," referenced on the Getting Started thread along with many other excellent recommendations. TAPL absolutely accomplished a 180° shift in my understanding of types and their relationship to programming, with LtU itself playing an invaluable supporting role. The next head-expander I recommend might be Coq'Art. It's extremely formal (naturally; it's about theorem proving, after all) but surprisingly accessible, even playful in places. Highly recommended, especially since you can (and should, IMHO) download the version of Coq used in the text and get your hands dirty.

Is it legit to have functions that yield messages (with a phantom type used to check who it's OK to send the message to) which can then be sent with the expectation of yielding a result? I'd probably end up implementing the object model along similar lines in Haskell.

> Is anyone else interested?

Sign me up. Marc Stiegler and I (mostly Marc) are also working on Emily - essentially the subset of O'Caml language which does not violate object-capability safety. For example, Emily has no mutable static variables. All variables at the top level of a module - all per module values - may only be transitively immutable. Likewise, modules that provide ambient authority for accessing the world outside the program, like opening a file, must be suppressed.

The Emily implementation is essentially O'Caml with an extra verifier in front of it, to ensure that submitted programs use only the object-capability-safe subset of O'Caml. I'm interested in understanding the relationship between the dynamic object-capabilities of Emily and the static capabilities of Oleg and Shan's paper. In any case, everywhere you say "O'Caml" in your list, I'm hoping to say "Emily" instead.

> Let me highly recommend working through Pierce's "Types and Programming Languages" [TAPL]

I have made it about half way through Pierce's TAPL, and it is indeed excellent. However, until recently, I've been quite skeptical of the value of static type systems, for reasons explained in my thesis. (See especially section 26.4 on SCOLL.) This skepticism is also reflected in the E design, which has only dynamic type safety and soft typing. Now that Oleg has explained to me some of the magic expressible with static type systems, I'll go back and try to complete Pierce's TAPL. Thanks.

Skepticism is good; it's the vital engine that drives Popperian scientific philosophy. "Let's Do It!" is my rallying cry to respond to the challenge and see if some of the loose ends that seem to be so tantalizingly close to each other can in fact be tied together. There are some initial solutions in the increasingly-misnamed "Advantages of Soft Typing" thread that I hope you have the opportunity to examine. This is exciting stuff!

In particular, AFAICT, the type system described in Shroff and Smith's Type Inference for First-Class Messages with Match-Functions, either by itself or in combination with Lightweight Static Capabilities, is still not be expressive enough to allow the membrane pattern.

Can a membrane be built on transparent forwarding? If so, then I believe the theory in the cited paper is sufficient. Assuming I have this right, at most you simply wrap each argument of a message in a transparent forwarder. That forwarder then wraps everything returned via itself in another such forwarder (whether it's pure data, or it carries authority). IIRC, the destruction of a membrane invalidates all capabilities passed through it, thus, each forwarder requires at most a reference to the base forwarder (membrane) to ensure its validity. This is like a "viral Caretaker" pattern. I think that would work, but I haven't completely thought through all the implications.

Can a membrane be built on transparent forwarding?

By this I meant "transparent, revocable forwarders" of course.

For any tuple, (a, b), the call (wrap (a, b)) must yield the tuple (wrap(a), wrap(b)). Similarly, and especially if we're using polymorphic variants as messages, then (wrap (`MsgName a b)) must yield (`MsgName wrap(a) wrap(b)). In order to do this, we'd need to, for example, iterate over a tuple as a heterogenous list. How would one do that?

Btw, what's the relationship is between match-functions and GADTs? Given GADTs, can one express Shroff and Smith's match-functions directly?

Polymorphic variants seem essential to allow different objects to accept different sets of message.

GADTs can provide the limited dependent typing needed, but you would need to provide a witness to the mapping between message type and result type somehow. I think passing around witnesses directly would be basically equivalent to hardcoding the result type into the types of first class messages. If you're willing to do that, Daan Leijen's work in First-class labels for extensible rows can provide the polymorphism.

The mapping from label + argument types to result type could probably be computed with the type functions from Sheard's Omega, or the interaction between fancy type classes and GADTs proposed in A Framework for Extended Algebraic Data Types.

I'm dubious about doing it with (current) GHC Haskell, but I think a satisfactory implementation in Omega might be possible.

GADTs do appear to be isomorphic to match-types (the type equivalent of match-functions). However, the key difference seems to be that type inference of GADTs, as presented in paper titled "Simple Unification-based Type Inference for GADTs", relies significantly on programmer annotations as opposed to match-types which can be inferred without any programmer declarations. However, the closure algorithm for the type inference of match-functions is constraint based, that is, the type inference results in a set of constraints. The simplification of this constraint set to generate a human readable type (as given by say the Caml top loop) is non-trivial.

The type inference algorithm presented by Simon Peyton Jones in the above mentioned paper might be a practical solution for incorporating first-class messages in existing languages.