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

[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/

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

[Nicolas Ojeda Bar]

[-- Attachment #1: Type: text/plain, Size: 2472 bytes --]

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


On Fri, Jul 24, 2015 at 1:01 PM, Markus Weißmann <markus.weissmann@in.tum.de
> 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
>
> --
> 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
>

[-- Attachment #2: Type: text/html, Size: 3650 bytes --]

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

[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

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

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

[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.

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

[Jeremy Yallop]

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.

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

[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

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

[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)

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

[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

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

[Markus Mottl]

The object type trick is pretty neat and can actually be used with
module types, too.  The advantage there is that whereas object types
are "flat", module types support more structure via submodules, e.g.:

  module type Bla = sig module Foo : sig type t end end
  type 'a t = 'foo_t constraint 'a = (module Bla with type Foo.t = 'foo_t)

Sadly, there is one significant shortcoming here: there does not seem
to be any way to exploit subtyping with module types.  Not sure, but
the only reason for this seems to be that values of module type (i.e.
first-class modules) cannot be reasonably implemented with subtyping,
because unlike objects they don't carry around a dictionary at runtime
for looking up entries in the module.

Please correct me if I'm wrong, but from a pure typing perspective I
think that there should be no reason to disallow support for
expressing subtyping with module types.  The compiler is already able
to infer whether module signatures satisfy subtyping relationships
anyway.

Would it be possible to support this in the type system?  Or is there
already some ingenious hack that can give comparable results with the
existing type system?

Regards,
Markus

On Fri, Jul 24, 2015 at 4:25 PM, Jeremy Yallop <yallop@gmail.com> wrote:
> 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.
>
> --
> 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



-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com

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

[Jacques Garrigue]

On 2015/08/09 06:39, Markus Mottl wrote:
> 
> The object type trick is pretty neat and can actually be used with
> module types, too.  The advantage there is that whereas object types
> are "flat", module types support more structure via submodules, e.g.:
> 
>  module type Bla = sig module Foo : sig type t end end
>  type 'a t = 'foo_t constraint 'a = (module Bla with type Foo.t = 'foo_t)
> 
> Sadly, there is one significant shortcoming here: there does not seem
> to be any way to exploit subtyping with module types.  Not sure, but
> the only reason for this seems to be that values of module type (i.e.
> first-class modules) cannot be reasonably implemented with subtyping,
> because unlike objects they don't carry around a dictionary at runtime
> for looking up entries in the module.
> 
> Please correct me if I'm wrong, but from a pure typing perspective I
> think that there should be no reason to disallow support for
> expressing subtyping with module types.  The compiler is already able
> to infer whether module signatures satisfy subtyping relationships
> anyway.


The problem is that if you allow expression subtyping for module types,
then I see no way to avoid its being applied to … modules. Which we want to
avoid, since the semantics of subtyping for modules is not the same as
for expressions (i.e., modules require coercions).

By the way, you can also define deep structures with object types, so
I don’t see the advantage of using module types. For an example of
nested object structures, you can see lablgtk, with its sub-object approach
for signals.

Jacques Garrigue