[cap-talk] Abstractions that subsume capabilities

Sandro Magi naasking at higherlogics.com
Sun Mar 9 13:00:35 EDT 2008


Kevin Reid wrote:
> On Mar 9, 2008, at 11:26, Sandro Magi wrote:
> 
>> Both capabilities and RT techniques impose restrictions on the use  
>> of effects which affect the "world", ie. via devices. In Haskell,  
>> this distinction is not very fine-grained at the moment, as most  
>> effects simply live in the "IO" monad, but there is no reason why  
>> these effects couldn't be made more fine-grained, ie. IO => DelDir,  
>> SendPacket, etc.
> 
> 
> That type of subdivision is not sufficient, since it does not readily  
> permit specifying *which* directory is deleted, or *where* the packet  
> is sent. It expresses an essentially static access policy.

There are other considerations, true. I would want the filesystem root 
to be encapsulated within the monad, thus enabling more modular patterns 
("FileSystem" is a private namespace). I think this is a question of 
modularity as much as access control. I imagine my structure would be 
similar to yours, where the filesystem must be an explicit parameter 
like your World.

I do think Haskell's API is still a little too impure due to openFile, 
readFile and the like. I'm still working on how to frame this as a a 
violation of RT, as well as FFI as a whole. All such languages can be 
given an interpretation within a monadic semantics, and I think this 
perspective will provide a more rigourous foundation for capabilitiy 
principles Re: devices.

Sandro


More information about the cap-talk mailing list