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