[cap-talk] Capabilities for immutable data

[Sandro Magi]

On 2011-02-18 3:46 AM, David Wagner wrote:
> The thrown exception is not an externally observable effect. It causes
> the program to terminate early and reduces the time it takes for the
> program to execute, but as you mentioned, we are not treating the running
> time of the program as a relevant change to the world.

Whether the program completes at all, or completes with a value seems a
relevant change. Non-termination and exceptions are both side-effects in
programming language theory.

> I'm not familiar enough with purely functional operating systems to
> comment with any confidence, but here's my impression about how this
> kind of thing works.  I believe you can write a "purely functional"
> Haskell program that does I/O.  You might be asking, what the heck?
> Isn't that a contradiction in terms?  It's not a contradiction.
> To resolve the paradox, you have to understand what it means for the
> program to be "purely functional", and how it does I/O. 

I wasn't even considering monads or linear typing because those map
trivially to traditional capabilities. Consider instead an OS where
checkpointing is performed by the garbage collector. Now everything is
an immutable value in memory which is slowly migrated to disk, and there
are no explicit "handles" to perform I/O; I/O happens naturally as part
of the trusted runtime during tracing. Where are the capabilities here?

The only sensible answer seems to be "everywhere". And if it's
"everywhere" here, why not everywhere else? Turing tarpit and all that.

This would be a terrible OS most likely, but it shows how far you can
push immutable values into doing I/O without any notion of handles, and
which just doesn't really square with "capabilities as effects".

For that matter, there is little reason to consider IPC to another
process to be an effect, considering it's a purely in-memory message
send so it's technically "pure computation" as well, so where do you
draw the line for I/O? When it leaves main memory? When it leaves the
host entirely?

> To come back to your question, hopefully the clear line is whether the
> object reference conveys authority or not.  Whether the object reference
> should be called a "capability" is, I claim, less fundamental.  So the
> fundamental question here is, I think, what do we mean by "authority"?
> What is the definition of "authority"?  I suspect if we can agree on
> that, everything else will take care of itself.

I agree this is the fundamental question. The definition I've worked
with for years and advanced by Lightweight Static Capabilities: a
capability is an abstract data type. The abstraction maintains
invariants, and only the code internal to that abstraction can violate
those invariants. Authority is then the ability to access the internals
of an abstraction. This seems the most general definition applicable to
all domains, ie. I/O, immutable or mutable in-memory values, IPC, etc.

A language provides abstract primitive types, like integers, which have
their own invariants. Each primitive function defined by the language
conveys authority since it can manipulate the internals of primitive
values (we can only examine the alleged structure of integers via
operations provided on integers). The authority on primitives is
minimal, and generally of little interest, except when it's not, such as
array bounds checking, range checking for program verification, etc.

FFI is a way to extend the language primitives, and thus interject new
authorities into the global environment. "Capability security" is then a
constraint on the FFI to ensure new authorities conform to certain rules.

Language theory, verification and capabilities are thus all intimately
intertwined. I agree most of this authority is of little interest most
of the time, I'm just disagreeing that immutable values don't carry
authority of their own, and thus that pure computation is not exerting
some type of authority.

Sandro