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 3FCC07EEBF for ; Fri, 24 Jul 2015 22:24:13 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of octa@polychoron.fr) identity=pra; client-ip=217.70.183.197; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="octa@polychoron.fr"; x-sender="octa@polychoron.fr"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of octa@polychoron.fr) identity=mailfrom; client-ip=217.70.183.197; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="octa@polychoron.fr"; x-sender="octa@polychoron.fr"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@relay5-d.mail.gandi.net) identity=helo; client-ip=217.70.183.197; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="octa@polychoron.fr"; x-sender="postmaster@relay5-d.mail.gandi.net"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0ALAQBonrJVnMW3RtlchFiDHaUyBo4ujD4CgUpMAQEBAQEBEgEBAQEBBg0JCSEuhCQBAQQSEQQRQBELGgIFFgsCAgkDAgECAUUGAQwIAQEeiAoGA68FiiSWDwwggSKEfIUvhDxSgmmBQwEElGOBP5NPjFeDeQIXhA6CNIEEAQEB X-IPAS-Result: A0ALAQBonrJVnMW3RtlchFiDHaUyBo4ujD4CgUpMAQEBAQEBEgEBAQEBBg0JCSEuhCQBAQQSEQQRQBELGgIFFgsCAgkDAgECAUUGAQwIAQEeiAoGA68FiiSWDwwggSKEfIUvhDxSgmmBQwEElGOBP5NPjFeDeQIXhA6CNIEEAQEB X-IronPort-AV: E=Sophos;i="5.15,540,1432591200"; d="scan'208";a="141122791" Received: from relay5-d.mail.gandi.net ([217.70.183.197]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 24 Jul 2015 22:24:12 +0200 Received: from mfilter25-d.gandi.net (mfilter25-d.gandi.net [217.70.178.153]) by relay5-d.mail.gandi.net (Postfix) with ESMTP id 258E441C061; Fri, 24 Jul 2015 22:24:12 +0200 (CEST) X-Virus-Scanned: Debian amavisd-new at mfilter25-d.gandi.net Received: from relay5-d.mail.gandi.net ([217.70.183.197]) by mfilter25-d.gandi.net (mfilter25-d.gandi.net [10.0.15.180]) (amavisd-new, port 10024) with ESMTP id XhBQ9VeZaAwa; Fri, 24 Jul 2015 22:24:10 +0200 (CEST) X-Originating-IP: 41.13.228.4 Received: from [192.168.42.219] (vc-gp-n-41-13-228-4.umts.vodacom.co.za [41.13.228.4]) (Authenticated sender: octa@polychoron.fr) by relay5-d.mail.gandi.net (Postfix) with ESMTPSA id EC74C41C054; Fri, 24 Jul 2015 22:24:09 +0200 (CEST) To: =?UTF-8?Q?Markus_Wei=c3=9fmann?= , caml-list@inria.fr References: From: octachron Message-ID: <55B29EC7.2070202@polychoron.fr> Date: Fri, 24 Jul 2015 22:23:35 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.1.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] Clever typing for client-server communication? 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.