[Caml-list] RFH: type / consistency problem

[Caml-list] RFH: type / consistency problem

[Goswin von Brederlow]

Hi,

I have two C types like this:

   struct Request {
     uint32_t cmd_type;
     uint32_t size;
     uint8_t  data[];
   };

   struct Reply {
     uint32_t reply_type;
     uint32_t cmd_type; // the cmd_type of the request this reply is for
     uint32_t size;
     uint8_t  data[];
   };

Note: The C types are given and they do not have a request ID or
anything that can be matched to a reply, only the cmd_type. 2 requests
with the same cmd_type must not happen concurrently.

Now in the ocaml bindings this becomes maybe:

   type request = Foo of string | Bar of int | Baz
   type cmd_type = Foo | Bar | Baz
   type msg = Error of string | Buzz of float | Burr
   type reply = { cmd_type : cmd_type; msg : msg; }

Or should I rather keep track of request on the C side, match replies
to requests and use requests in the reply type like this?

   type reply = { req : request; msg : msg; }

On top of that there is a connection between request and reply
contents. A Foo request can get an Error or Buzz while Bar/Baz can get
Error or Burr. Anything else would be invalid. It would be nice if the
type system would prevent creating a Burr reply to a Foo request.


So here is my request for your ideas:

How do I match requests to replies with that? How do I ensure that
request and cmd_type remain in-sync over time when new variants get
added? I'm wondering if there is some magic that could be used to
ensure correct types? Maybe something with GADTs? Something that would
bind requests and replies together in some way to ensure corectness.
Other tricks?

MfG
	Goswin

Re: [Caml-list] RFH: type / consistency problem

[Erkki Seppala]

Something like this?

module Protocol : sig
  type 'a request
  type 'a reply
  type session

  val issue : session -> 'a request -> 'a

  type foo_response = { fr_s : string }
  val foo : string -> foo_response request

  type bar_response = int
  val bar : int -> bar request

  type baz_response = unit
  val baz : unit -> baz request
end = struct
  type 'a reply = string -> 'a
  type 'a request = {
    req_type : int;
    req_data : string;
    req_handle : 'a reply
  }

  type foo_response = { fr_s : string }
  
  let issue session request =
    send (request.req_type, request.req_data);
    request.req_handle (receive ())

  let foo int = 
    let handle_foo_response str =
      { fr_s = str }
    in
      { req_type = 42; req_data = Printf.sprintf "hello %d" int;
        req_handle = handle_foo_response }

  (* etc *)
end

The nice thing about this is that you can support synchronous and
asynchronous communication with essentially the same interface of
constructing messages, you just have a different kind of issue function.

-- 
  _____________________________________________________________________
     / __// /__ ____  __               http://www.modeemi.fi/~flux/\   \
    / /_ / // // /\ \/ /                                            \  /
   /_/  /_/ \___/ /_/\_\@modeemi.fi                                  \/

Re: [Caml-list] RFH: type / consistency problem

[Goswin von Brederlow]

On Mon, May 13, 2013 at 03:11:05PM +0300, Erkki Seppala wrote:
> Something like this?
> 
> module Protocol : sig
>   type 'a request
>   type 'a reply
>   type session
> 
>   val issue : session -> 'a request -> 'a
> 
>   type foo_response = { fr_s : string }
>   val foo : string -> foo_response request
> 
>   type bar_response = int
>   val bar : int -> bar request
> 
>   type baz_response = unit
>   val baz : unit -> baz request
> end = struct
>   type 'a reply = string -> 'a
>   type 'a request = {
>     req_type : int;
>     req_data : string;
>     req_handle : 'a reply
>   }
> 
>   type foo_response = { fr_s : string }
>   
>   let issue session request =
>     send (request.req_type, request.req_data);
>     request.req_handle (receive ())
> 
>   let foo int = 
>     let handle_foo_response str =
>       { fr_s = str }
>     in
>       { req_type = 42; req_data = Printf.sprintf "hello %d" int;
>         req_handle = handle_foo_response }
> 
>   (* etc *)
> end
> 
> The nice thing about this is that you can support synchronous and
> asynchronous communication with essentially the same interface of
> constructing messages, you just have a different kind of issue function.

There is no connection between the 'a of a request, req_type and the
req_data. req_data isn't even the raw data anymore but, I assume,
already the serialized data ready for sending. So you have gone from 2
independet types to 3. I could create a foo_responce request with
req_type = Bar containing the data for type Buzz.

And what about the server? It reads requests from the network and has
to send out matching replies. I'm actually more interested in that
side, but both should work and have the same common type.

MfG
	Goswin