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