From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 2707F7EF37 for ; Fri, 24 Jul 2015 13:21:00 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of n.oje.bar@gmail.com) identity=pra; client-ip=209.85.212.178; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="n.oje.bar@gmail.com"; x-sender="n.oje.bar@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of n.oje.bar@gmail.com designates 209.85.212.178 as permitted sender) identity=mailfrom; client-ip=209.85.212.178; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="n.oje.bar@gmail.com"; x-sender="n.oje.bar@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wi0-f178.google.com) identity=helo; client-ip=209.85.212.178; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="n.oje.bar@gmail.com"; x-sender="postmaster@mail-wi0-f178.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0DHBADPHrJVlbLUVdFbgzQ1aQaDHakIhFWKVoIohgECgTwHTAEBAQEBARIBAQEBBw0JCR8whCQBAQMBEhEEGQEbEgsBAwELBgULGh0CAiIBEQEFAQoSBhMIChCHdgEDCggNpkyBLD4xiz+BbIJ5ixoKGScDCleEWAEBAQcBAQEBAQEWAQUOiz+EPEcEB4JpgUMFhWEMjnaEdodGgguVTxIjgRURBoIaH4FVPDGCSwEBAQ X-IPAS-Result: A0DHBADPHrJVlbLUVdFbgzQ1aQaDHakIhFWKVoIohgECgTwHTAEBAQEBARIBAQEBBw0JCR8whCQBAQMBEhEEGQEbEgsBAwELBgULGh0CAiIBEQEFAQoSBhMIChCHdgEDCggNpkyBLD4xiz+BbIJ5ixoKGScDCleEWAEBAQcBAQEBAQEWAQUOiz+EPEcEB4JpgUMFhWEMjnaEdodGgguVTxIjgRURBoIaH4FVPDGCSwEBAQ X-IronPort-AV: E=Sophos;i="5.15,538,1432591200"; d="scan'208";a="141080017" Received: from mail-wi0-f178.google.com ([209.85.212.178]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 24 Jul 2015 13:20:55 +0200 Received: by wibud3 with SMTP id ud3so23432255wib.0 for ; Fri, 24 Jul 2015 04:20:55 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=QGaB/KYlQhdTCn7m6KWu2maDs0tx7CJM+3GqCxvNx4E=; b=sW1+1OvVrhTQhpiZvLR+qcfbW0XiJ7OkvuBssSrbXMM3Tr81/zbA9ML6dIRVDTPeFk aWj3698dnYk1oOtqt5YAgmcBn0F2AMzI2hDESvnH0v/INDhySo8/ALZXn9X81aT3OyhY v39LTsDlcLmQ/i9Sg2OzE68kuYowh+UO8XG3w4nEX5u6pe/D+fpN/t90GJP9dgFrbrcw HASXgq4CRazatl9VG6DxPYxHgaw9h1u/435n3V9WeCHN6xwibFlihOMEsMtUe72rc7fr BmHi0pSMBAoPJCpkr/DzkGsy/kkMS3XBbIgACz81TPMywAKv+zijmqyUO8UCuk1yYYf7 lrjg== MIME-Version: 1.0 X-Received: by 10.180.103.69 with SMTP id fu5mr5839747wib.95.1437736855112; Fri, 24 Jul 2015 04:20:55 -0700 (PDT) Received: by 10.194.166.200 with HTTP; Fri, 24 Jul 2015 04:20:55 -0700 (PDT) In-Reply-To: References: Date: Fri, 24 Jul 2015 13:20:55 +0200 Message-ID: From: Nicolas Ojeda Bar To: =?UTF-8?Q?Markus_Wei=C3=9Fmann?= Cc: caml-list@inria.fr Content-Type: multipart/alternative; boundary=f46d044281328794c4051b9d3245 Subject: Re: [Caml-list] Clever typing for client-server communication? --f46d044281328794c4051b9d3245 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 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 =3D | ClientServer : mysocket -> (client, server) socket | ServerClient : mysocket -> (server, client) socket Best wishes, Nicolas On Fri, Jul 24, 2015 at 1:01 PM, Markus Wei=C3=9Fmann 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 =3D bytes > type ('a, 'b) socket =3D mysocket > > But the underlying system allows me to add filters that guarantee me the > aforementioned properties of send/receive. > > regards > Markus > > -- > Markus Wei=C3=9Fmann, M.Sc. > Technische Universit=C3=A4t M=C3=BCnchen > Institut f=C3=BCr 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 > --f46d044281328794c4051b9d3245 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
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 =3D
=C2=A0 | ClientServer : mysocket -> (= client, server) socket
=C2=A0 | ServerClient : mysocket -> (se= rver, client) socket

Best wishes,
Nicola= s


On Fri, Jul 24, 2015 at 1:01 PM, Markus Wei=C3=9Fmann <markus.weissmann@in.tum.de> wrote:
Hello OCaml list,

I'm trying to do something clever regarding the interface for a communi= cation library:
There is a server and a client which can only send "client" (clie= nt 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 mes= sages", "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&qu= ot; 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 typ= e 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) s= ocket";


regards
-Markus

PS: Under the hood its basically

type 'a message =3D bytes
type ('a, 'b) socket =3D mysocket

But the underlying system allows me to add filters that guarantee me the af= orementioned properties of send/receive.

regards
Markus

--
Markus Wei=C3=9Fmann, M.Sc.
Technische Universit=C3=A4t M=C3=BCnchen
Institut f=C3=BCr Informatik
Boltzmannstr. 3
D-85748 Garching
Germany
http://wwwknoll.in.tum.de/


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

--f46d044281328794c4051b9d3245--