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

[Mikhail Mandrykin <mandrykin@ispras.ru>]

Hello,
> but is there some clever way to only have the socket annotated with 
> one type while keeping only one send and one recv function?
> 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]
>
> there is no "(client, client) socket" or "(server, server) socket";
>
The closest solution I can suggest is with a recv signature

val recv : ('a, 'b) recv_t -> 'a socket -> 'b message

(one extra argument while socket is annotated with only one type and 
there's only one send and recv function). This uses GADTs:

type 'a socket =
| Client_socket : ... -> client socket
| Server_socket : ... -> server socket

type 'a message =
| Client_message : ... -> client message
| Server_message : ... -> server message

let send =  ...

type (_, _) recv_t =
   | From_client : (server, client) recv_t
   | From_server : (client, server) recv_t

let recv : type a b. (a, b) recv_t -> a socket -> b message =
   function
   | From_client -> fun Server_socket -> ... Client_message (...)
   | From_server -> fun Client_socket -> ... Server_message (...)

The "[server socket -> client message | client socket -> server message] 
" (without an extra argument) looks like a dependent type (in spirit of 
" 'a socket -> (reverse 'a) message"), which makes me doubt about 
whether it's possible in OCaml.

Regards,
Mikhail

On 07/24/2015 02:01 PM, Markus Weißmann wrote:
> Hello OCaml list,
>
> I'm trying to do something clever regarding the interface for a 
> communication library:
> There is a server and a client which can only send "client" (client to 
> server) and "server" (server to client) messages.
> The current idea is to use a phantom type to annotate the socket as 
> either being "client to server" or "server to client";
>
> type client
> type server
>
> type ('a, 'b) socket
> type 'a message
>
> I've got a bunch of functions that only work on either "client 
> messages", "server messages" or some on both. Something like:
>
> val p1 : 'a message -> int
> val p2 : server message -> float
> val p3 : client message -> char
>
> 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
>
> but is there some clever way to only have the socket annotated with 
> one type while keeping only one send and one recv function?
> 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]
>
> there is no "(client, client) socket" or "(server, server) socket";
>
>
> regards
> -Markus
>
> PS: Under the hood its basically
>
> type 'a message = bytes
> type ('a, 'b) socket = mysocket
>
> But the underlying system allows me to add filters that guarantee me 
> the aforementioned properties of send/receive.
>
> regards
> Markus
>


-- 
Mikhail Mandrykin
Linux Verification Center, ISPRAS
web: http://linuxtesting.org
e-mail: mandrykin@ispras.ru