Re: [Caml-list] Clever typing for client-server communication?

[mandrykin <mandrykin@ispras.ru>]

> 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