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

[octachron <octa@polychoron.fr>]

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";
>

I see one way to do this, but I am not sure I would call it a clever way.

The idea is to try to encode (-1),(1) and (~-) at the type level. With 
this encoding, it is possible
to define send and recv as

type 'a socket
val send : 'n socket -> 'n message -> unit
val recv : 'n socket -> '-n message

A working encoding would be:

type head
type tail
type 'a socket = ... (constraint  'a = 'b * 'c)
type 'a message = ... (constraint  'a = 'b * 'c)

where you can use either gadt or abstract value to enforce that 'a is 
only head*tail ( = 1 ) or tail*head ( = -1 ).

Then -( 'a * 'b ) can be translated to ('b *' a), i.e.

val send : 'n socket -> 'n message -> unit
val recv: ('a * 'b) socket -> ('b * 'a) message

With this encoding, you only need to decompose the type parameter of 
socket or message when you need to flip it. However, I am not sure that 
this slim advantage is worth the added complexity (and one could argue 
that I added a type parameter to message rather than removed one from 
socket).

Regards,
octachron.