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

[Markus Mottl <markus.mottl@gmail.com>]

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