On Mon, Jun 22, 2009 at 7:27 PM, Tim Sheard <she...@cs.pdx.edu> wrote:
> My idea is to use types to ensure that any > sequence of operations adheres to a path on > a finite state automata. For example > if we wanted to implement the following > automata (This needs to read in a fixed width font) > Here's the reply Oleg gave me when I asked about using monadic regions to enforce similar constraints (published with Oleg's permission): Oleg writes: > First of all, protocols of using API functions are essentially > session types, right? Thus various implementations of session types > could be taken advantage of (including the one presented by Jesse Tov > on Haskell 2008 Symposium). Aliasing is responsible for a lot of the > complexity: if the variable 's' is bound to a value of the type socket > and we execute "do s' <- bindS s" so to bind the socket, the old > variable s is still available and could be used. But it should not be > used because bindS "consumed" the unbound socket and produced the new > one. To properly describe these resource restrictions (a resource can > be consumed and after that it is not available any more), we need > linear, affine or various other kinds of substructural logics and type > systems. It seems they all can be emulated in Haskell, but with some > hackery (see for example Sec 6 of our monadic regions > paper). Parameterized monads are necessary. > > The lightweight monadic regions paper relied on a simple > session protocol: open -> (read+write)* -> close. That protocol can be > ensured without parameterized monads: the only aliasing to mind is > the accessibility of the file handle after the closing operation. We > can get rid of `close' (make it implicit ar region's exit) and use > rank-2 types to prevent file handles from leaking out. There is some > dynamic overhead, in the function open. However, the most frequent > operation, reading and writing from the handle, involves no overhead > and its correctness ensured statically. > > That design can be extended to sockets. For example: > > data Socket sort = Socket Int > > data UnconnectedSocket > data ConnectedSocket s > > connect :: RMonadIO (m s) => SocketProto -> SAddress -> > m s (Socket (ConnectedSocket s)) > > sendto :: RMonadIO (m s) => (Socket (ConnectedSocket s)) -> Buffer > -> m s (ReturnCode) > > -- polymorphic in the socket sort > send :: MonadIO m => Socket sort -> Buffer -> m ReturnCode > > > In this design, the operation of creating a socket and connecting it > are bundled together -- which is very common and is the case for > System V, I think (where it is called openActive, I think). If you for > some reason want to keep 'socket' and 'connect' separate, then > 'connect' has to check at run-time that the socket in question is not > connected yet. Still, the most common operations like send and write > should be overhead-free. Cheers, Johan
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
