Re: [Caml-list] Clever typing for client-server communication?

[Jeremy Yallop <yallop@gmail.com>]

On 24 July 2015 at 12:01, Markus Weißmann <markus.weissmann@in.tum.de> wrote:
> but is there some clever way to only have the socket annotated with one type
> while keeping only one send and one recv function?

One way to achieve this is to add some structure to the 'server' and
'client' types, by turning your descriptions of the desired behaviour
into code.  For example, you say

> There is a server and a client which can only send "client" (client to
> server) and "server" (server to client) messages.

which you might encode as follows:

type server = < src: server; dst: client; name: [`server] >
 and client = < src: client; dst: server; name: [`client] >

These are object types, but there's no need to actually use object
values in your code.  The object type syntax is simply a convenient
way to label the different components of the type so that they can be
retrieved later.

Once you have these types you might write type-level functions to
retrieve the components.   Here's a function that retrieves the 'src'
component:

   type 'a src = 's constraint 'a = < src: 's; .. >

This can be read as follows: src is a function that maps 'a to 's,
where 'a is an object type with a src key, and 's is the value of that
key.

Similarly, here's a function to retrieve the 'dst' component:

   type 'a dst = 'd constraint 'a = < dst: 'd; .. >

> You can only send "client messages" on the "client socket" and "server
> messages" on the "server socket".
>
> val send : ('a, _) socket -> 'a message -> unit
>
> You can get these messages only on the respective other side.
>
> val recv : (_, 'b) socket -> 'b message
>
> Something in the spirit of this:
>
> type 'a socket
> val send : 'a socket -> 'a message -> unit
> val recv : [server socket -> client message | client socket -> server
> message]

You might then write

  val send : 's socket -> 's src message -> unit
  val recv : 's socket -> 's dst message

and OCaml will enforce the constraints you describe.

Kind regards,

Jeremy.