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

[Markus Weißmann]

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

--
Markus Weißmann, M.Sc.
Technische Universität München
Institut für Informatik
Boltzmannstr. 3
D-85748 Garching
Germany
http://wwwknoll.in.tum.de/


--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Nicolas Ojeda Bar]

Hi,

This is not exactly what you asked, but you can use GADTs to constrain the
phantom type (_, _) socket:

type client
type server

type (_, _) socket =
| ClientServer : mysocket -> (client, server) socket
| ServerClient : mysocket -> (server, client) socket

Best wishes,
Nicolas

[Mikhail Mandrykin]

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

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

[octachron]

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.

[Jeremy Yallop]

On 24 July 2015 at 12:01, Markus Weißmann <markus.w...@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.

[Török Edwin]

On 07/24/2015 11:25 PM, Jeremy Yallop wrote:
> 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 is very useful to know, thanks!

It'd be interesting to know how you come up with these solutions :)
They are easy to understand as you've explained, but I wouldn't have thought of this solution
although I guessed there had to be a solution with objects (after reading [1]), and I understand (simple) phantom types and (mostly) understand object types and GADTs by now.

Is there some (fundamental) knowledge I'm missing that would allow me to construct solutions to problems like these
(if so could you point to some papers, lecture notes or books please), or is it just that I very rarely use objects/GADTs and lack the experience?

Best regards,
--Edwin

[1] http://stackoverflow.com/questions/10779283/when-should-objects-be-used-in-ocaml/10780681#10780681

[Oleg]

> > 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 is very useful to know, thanks!

> It'd be interesting to know how you come up with these solutions :)

This is probably a folklore, but it was mentioned on this list more than
a decade ago by Jacques Garrigue. We have used this trick extensively
in

http://okmij.org/ftp/meta-programming/HPC.html#GE-generation

(see the description on p11 of the SCP-metamonads.pdf paper, and many
applications starting from p21)

[mandrykin]

> This is probably a folklore, but it was mentioned on this list more
> than
> a decade ago by Jacques Garrigue. We have used this trick extensively
> in
>
> http://okmij.org/ftp/meta-programming/HPC.html#GE-generation
>

For me actually knowing the trick used in the paper alone was not enough
to quickly come up with this solution. I had already used this object
constraints several times in even in real-life code, but that didn't
help much(. To me the key idea here (in the Jeremy Yallop's solution) is
the ability to express the "negation" function on type level with a pair
of mutually-recursive types and a constraint. This can actually be also
done with polymorphic variants instead of object types:

type client = [`cs of server * [`client]]
and server = [`cs of client * [`server]]
type 'a rev = 'b constraint 'a = [`cs of 'b * _] (* rev is the function
*)

This ensures the relations client rev = server, server rev = client and
client <> server. This approach seems powerful enough to express any
finite permutation group, e.g. for 2 elements:

type z = [`t of [`e1] * [`e2] * z] (* initial permutation *)

type 'e e1 = [`t of 'e1 * 'e2 * 'e e1] (* neutral permutation *)
constraint 'e = [`t of 'e1 * 'e2 * _ ]
and 'e e2 = [`t of 'e2 * 'e1 * 'e e2] (* reverse permutation *)
constraint 'e = [`t of 'e1 * 'e2 * _]

type 'a inv = 'b constraint 'a = [`t of _ * _ * 'b]

Here "-e1 - e2 - e3 - ... - en + e1' + e2' + ... + em'" (using `+' for
the group operation and `-' for the inverse) can be encoded as "z e1 e2
.. en inv e1' e2' ... em'". By Cayley's theorem (states that every
finite group G is isomorphic to a subgroup of the symmetric group acting
on G) this means (if I got it right) that in fact any finite group
operation (and the corresponding inverse) is encodiable in OCaml as
type-level function!

Regards,
Mikhail