From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <mandrykin@ispras.ru>
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 0D7C27EEBF;
	Sat, 25 Jul 2015 17:55:16 +0200 (CEST)
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  mandrykin@ispras.ru) identity=pra; client-ip=83.149.199.79;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="mandrykin@ispras.ru";
  x-sender="mandrykin@ispras.ru"; x-conformance=sidf_compatible
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  mandrykin@ispras.ru) identity=mailfrom;
  client-ip=83.149.199.79;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="mandrykin@ispras.ru";
  x-sender="mandrykin@ispras.ru"; x-conformance=sidf_compatible
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@smtp.ispras.ru) identity=helo;
  client-ip=83.149.199.79;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="mandrykin@ispras.ru";
  x-sender="postmaster@smtp.ispras.ru";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: A0CqBQCfsLNV/0/HlVNcgxVUaQG9b4MRgmgCgTpMAQEBAQEBgQuEJAEBAwE4AjgHBQsEBwk9VwYBGhECiAsMCc9UAQsBH4tOgmyBUEsHhCwBBI0yhzeBP4M5h0mCC4Y4kGMmhABsgkwBAQE
X-IPAS-Result: A0CqBQCfsLNV/0/HlVNcgxVUaQG9b4MRgmgCgTpMAQEBAQEBgQuEJAEBAwE4AjgHBQsEBwk9VwYBGhECiAsMCc9UAQsBH4tOgmyBUEsHhCwBBI0yhzeBP4M5h0mCC4Y4kGMmhABsgkwBAQE
X-IronPort-AV: E=Sophos;i="5.15,542,1432591200"; 
   d="scan'208";a="171614295"
Received: from smtp.ispras.ru ([83.149.199.79])
  by mail2-smtp-roc.national.inria.fr with ESMTP; 25 Jul 2015 17:55:14 +0200
Received: from mail.ispras.ru (mail.ispras.ru [83.149.199.45])
	by smtp.ispras.ru (Postfix) with ESMTP id 5170A21582;
	Sat, 25 Jul 2015 18:55:12 +0300 (MSK)
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII;
 format=flowed
Content-Transfer-Encoding: 7bit
Date: Sat, 25 Jul 2015 18:55:12 +0300
From: mandrykin <mandrykin@ispras.ru>
To: Oleg <oleg@okmij.org>, edwin+ml-ocaml@etorok.net, caml-list@inria.fr
Cc: caml-list-request@inria.fr
In-Reply-To: <20150725124250.GA2259@Magus.sf-private>
References: <20150725124250.GA2259@Magus.sf-private>
Message-ID: <00260dc5e1bf970e84ccc99948acea6d@ispras.ru>
X-Sender: mandrykin@ispras.ru
User-Agent: Roundcube Webmail/1.1.2
Subject: Re: [Caml-list] Clever typing for client-server communication?

> This is probably a folklore, but it was mentioned on this list more 
> than
> a decade ago by Jacques Garrigue. We have used this trick extensively
> in
> 
>         http://okmij.org/ftp/meta-programming/HPC.html#GE-generation
> 

For me actually knowing the trick used in the paper alone was not enough 
to quickly come up with this solution. I had already used this object 
constraints several times in even in real-life code, but that didn't 
help much(. To me the key idea here (in the Jeremy Yallop's solution) is 
the ability to express the "negation" function on type level with a pair 
of mutually-recursive types and a constraint. This can actually be also 
done with polymorphic variants instead of object types:

type client = [`cs of server * [`client]]
   and  server = [`cs of client * [`server]]
type 'a rev = 'b constraint 'a = [`cs of 'b * _] (* rev is the function 
*)

This ensures the relations client rev = server, server rev = client and 
client <> server. This approach seems powerful enough to express any 
finite permutation group, e.g. for 2 elements:

type z = [`t of [`e1] * [`e2] * z] (* initial permutation *)

type 'e e1 = [`t of 'e1 * 'e2 * 'e e1] (* neutral permutation *)
  constraint 'e = [`t of 'e1 * 'e2 * _ ]
and 'e e2 = [`t of 'e2 * 'e1 * 'e e2] (* reverse permutation *)
  constraint 'e = [`t of 'e1 * 'e2 * _]

type 'a inv = 'b constraint 'a = [`t of _ * _ * 'b]

Here "-e1 - e2 - e3 - ... - en + e1' + e2' + ... + em'" (using `+' for 
the group operation and `-' for the inverse) can be encoded as "z e1 e2 
... en inv e1' e2' ... em'". By Cayley's theorem (states that every 
finite group G is isomorphic to a subgroup of the symmetric group acting 
on G) this means (if I got it right) that in fact any finite group 
operation (and the corresponding inverse) is encodiable in OCaml as 
type-level function!

Regards,
Mikhail