[cap-talk] Abstractions that subsume capabilities

[Kevin Reid]

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.

The way I have thought of doing a capability version of Haskell is to  
leave the IO monad alone, but make its *operators* require non-global  
authorities. That is, instead of the current

   type FilePath = String
   readFile :: FilePath -> IO String
   hPrint :: Show a => Handle -> a -> IO ()
   stdout :: Handle

   main = do
     s <- readFile "/etc/passwd"
     hPrint stdout s

, access to files and standard output would be explicitly passed, and  
start out as an argument to 'main' much like the privilegedScope in E:

   data FilePath = ...unexported constructor or opaque functions...
   pathToFile :: World -> String -> FilePath
   stdout :: World -> Handle

   main world = do
     let f = pathToFile world "/etc/passwd"
     s <- readFile f
     hPrint (stdout world) s

(I'm not sure if pathToFile ought to be ... -> IO String.)

This approach so far isn't sufficient to support substitutability  
(for e.g. membranes or test frameworks), unless FilePath is a record- 
of-functions or replaced with a typeclass, but it would require the  
least modification to existing Haskell programs.

-- 
Kevin Reid                            <http://homepage.mac.com/kpreid/>