From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 365BC7EEBF for ; Sat, 8 Aug 2015 23:39:06 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of markus.mottl@gmail.com) identity=pra; client-ip=209.85.223.178; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of markus.mottl@gmail.com designates 209.85.223.178 as permitted sender) identity=mailfrom; client-ip=209.85.223.178; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-io0-f178.google.com) identity=helo; client-ip=209.85.223.178; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="postmaster@mail-io0-f178.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0A2AQAddsZVlLLfVdFbgzo1Wg8Ggx6pc5IkhXkCgR8HTAEBAQEBARIBAQEBBwsLCR8whCQBAQQSEQQZARQHEgQHAQMMBgULDQICCR0CAiEBAREBBQEKEgYTEhCHdgEDEg2pPIEuPjGLP4FsgnlPiiAKGScDCleEVQEBAQEBAQQBAQEBAQEBFQEFDoEUii+CT4FvGDMHgmmBQwWFaQyGYIg2hQKFdYFsgUlGg1+DF4lFg02CGhIjgRcXhCgiMYJMAQEB X-IPAS-Result: A0A2AQAddsZVlLLfVdFbgzo1Wg8Ggx6pc5IkhXkCgR8HTAEBAQEBARIBAQEBBwsLCR8whCQBAQQSEQQZARQHEgQHAQMMBgULDQICCR0CAiEBAREBBQEKEgYTEhCHdgEDEg2pPIEuPjGLP4FsgnlPiiAKGScDCleEVQEBAQEBAQQBAQEBAQEBFQEFDoEUii+CT4FvGDMHgmmBQwWFaQyGYIg2hQKFdYFsgUlGg1+DF4lFg02CGhIjgRcXhCgiMYJMAQEB X-IronPort-AV: E=Sophos;i="5.15,635,1432591200"; d="scan'208";a="173053682" Received: from mail-io0-f178.google.com ([209.85.223.178]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 08 Aug 2015 23:39:05 +0200 Received: by iodb91 with SMTP id b91so80182711iod.1 for ; Sat, 08 Aug 2015 14:39:03 -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:content-transfer-encoding; bh=VXrQhXfTK0kbvTKXrzvWk3W3F8gGWl1lctuFX4jILzU=; b=lEnKO8Bf/yPZyGPtYvQ8CpRLSIYlJTe7QF/A+ZNX/juGgmK0GOOZyeOyUMxX/VTIGe SrSKVIhLW61aY74VXCJNt3eTyGmo1SAPSyF3IcZD/pVPhaIOaFL6X4iYTkSS48RWY88X YU9//foUM9EePtL+QpQIvFLmMe2mJ1kllO54rk7V7Zeb/dYqAh6119TBfQj12SBY7WwC NNsAzhUXO/hEJNVja3NPprDTX5i3qajyspLmIlFQPOMiz3R4Eqb20dS4YGYrk9AS/w6A oAaZHw8PD8HNOsEtFrdzj5XYgtUjUhlWeIGZXHe1nLpsrJ7x+9qhG29KSdKcwmaMQGcJ 10uQ== MIME-Version: 1.0 X-Received: by 10.107.10.96 with SMTP id u93mr16098386ioi.172.1439069943837; Sat, 08 Aug 2015 14:39:03 -0700 (PDT) Received: by 10.79.69.68 with HTTP; Sat, 8 Aug 2015 14:39:03 -0700 (PDT) In-Reply-To: References: Date: Sat, 8 Aug 2015 17:39:03 -0400 Message-ID: From: Markus Mottl To: Jeremy Yallop Cc: =?UTF-8?Q?Markus_Wei=C3=9Fmann?= , Caml List Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] Clever typing for client-server communication? 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 =3D sig module Foo : sig type t end end type 'a t =3D 'foo_t constraint 'a =3D (module Bla with type Foo.t =3D 'f= oo_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 wrote: > On 24 July 2015 at 12:01, Markus Wei=C3=9Fmann 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 =3D < src: server; dst: client; name: [`server] > > and client =3D < 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 =3D 's constraint 'a =3D < 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 =3D 'd constraint 'a =3D < 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 --=20 Markus Mottl http://www.ocaml.info markus.mottl@gmail.com