[Haskell-cafe] Suggestion for Network.Socket in regards to PortNumber

[Johan Tibell]

On Mon, Jun 22, 2009 at 7:27 PM, Tim Sheard <sheard at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090624/2207b203/attachment.html