On Mon, Jun 22, 2009 at 7:27 PM, Tim Sheard <sheard@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.