caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: Nicolas Ojeda Bar <n.oje.bar@gmail.com>
To: "Markus Weißmann" <markus.weissmann@in.tum.de>
Cc: caml-list@inria.fr
Subject: Re: [Caml-list] Clever typing for client-server communication?
Date: Fri, 24 Jul 2015 13:20:55 +0200	[thread overview]
Message-ID: <CAPunWhCFeo9MoGjPToqFiw3G7UQKhvX1EeVMXFRiC3yOTiiYHQ@mail.gmail.com> (raw)
In-Reply-To: <c44d210f0c2b3f58a45e95a8d81ddb2d@in.tum.de>

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

  reply	other threads:[~2015-07-24 11:21 UTC|newest]

Thread overview: 10+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2015-07-24 11:01 Markus Weißmann
2015-07-24 11:20 ` Nicolas Ojeda Bar [this message]
2015-07-24 18:41 ` Mikhail Mandrykin
2015-07-24 20:23 ` octachron
2015-07-24 20:25 ` Jeremy Yallop
2015-07-24 20:57   ` Török Edwin
2015-07-25 12:42     ` Oleg
2015-07-25 15:55       ` mandrykin
2015-08-08 21:39   ` Markus Mottl
2015-08-09 13:04     ` Jacques Garrigue

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=CAPunWhCFeo9MoGjPToqFiw3G7UQKhvX1EeVMXFRiC3yOTiiYHQ@mail.gmail.com \
    --to=n.oje.bar@gmail.com \
    --cc=caml-list@inria.fr \
    --cc=markus.weissmann@in.tum.de \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).