From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.1 required=5.0 tests=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id A28E3BBAF for ; Fri, 27 Jun 2008 08:38:59 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApoEALgnZEjAXQIm/2dsb2JhbACyaw X-IronPort-AV: E=Sophos;i="4.27,714,1204498800"; d="scan'208";a="14478529" Received: from discorde.inria.fr ([192.93.2.38]) by mail1-smtp-roc.national.inria.fr with ESMTP; 27 Jun 2008 08:38:59 +0200 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id m5R6cwXb012830 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Fri, 27 Jun 2008 08:38:59 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApoEAPQmZEiCNhAB/2dsb2JhbACyaw X-IronPort-AV: E=Sophos;i="4.27,714,1204498800"; d="scan'208";a="26768377" Received: from kurims.kurims.kyoto-u.ac.jp ([130.54.16.1]) by mail4-smtp-sop.national.inria.fr with ESMTP; 27 Jun 2008 08:38:57 +0200 Received: from localhost (orion [130.54.16.5]) by kurims.kurims.kyoto-u.ac.jp (8.13.8/8.13.8) with ESMTP id m5R6crNk013359; Fri, 27 Jun 2008 15:38:53 +0900 (JST) Date: Fri, 27 Jun 2008 15:38:41 +0900 (JST) Message-Id: <20080627.153841.27021948.garrigue@math.nagoya-u.ac.jp> To: David.Teller@univ-orleans.fr Cc: caml-list@inria.fr Subject: Re: [Caml-list] Polymorphic variant as a witness? From: Jacques Garrigue In-Reply-To: <1214546451.6510.5.camel@Blefuscu> References: <1214089919.6190.13.camel@Blefuscu> <20080623.192703.27793304.garrigue@math.nagoya-u.ac.jp> <1214546451.6510.5.camel@Blefuscu> X-Mailer: Mew version 4.2 on Emacs 22.2 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 48648B02.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; semantics:01 monadic:01 polymorphism:01 functors:01 functors:01 cheers:01 polymorphic:01 rec:01 rec:01 parameterize:01 typing:01 caml-list:01 functions:01 functions:01 tuples:01 > > * other solution: put everything inside a function, so that the > > type variable is still generalizable after typing the function. > > In that case, the witness remains invisible, doesn't it? No, the idea is to give the witness as argument to the function, so that its type is inferred and generalized. Of course this means that no side effects will occur until the function is called, so the semantics is preserved. And this way you can combine several such functions later by passing the same witness to all of them. Something like: let touch (x:[> ] as 'a) (y:'a) = () let m1 w = let rec f1 ... = ... touch `A w ... and f2 ... = ... touch `B w ... in let r1 = ... and r2 = ... in (f1, f2, r1, f2) let m2 w (f1, f2, r1, r2) = let rec f3 ... = ... in let r3 = ... in (f3, r3) let m1_then_m2 w = m2 w (m1 w) These modules encoded as functions are combined in something close to monadic style, but inside them you can just use your trick with "touch w", with no need to sequence the witness. By the way, since w is a function argument, it doesn't need to be of type "[> ..] ref" here. Note that the above approach is not going to be very precise. If you share directly w, then m1 will have type [> `A | `B] -> ... independently of whether f1 and f2 are actually used. If you want to be more precise, you must parameterize functions with witnesses. let m1 w = let rec f1 w ... = ... touch `A w ... and f2 w ... = ... touch `B w ... in ... This way you get a bit more control on when to merge effects. Thanks to let polymorphism, it looks like you just get the same power as with an effect system (you're still limited a bit by the value restriction). Also, you may have realized that the above code just uses functions to do that same thing as functors. Functors would be syntactically nicer, but they wouldn't let you infer the type of w, which is the whole point. If getting data out of tuples proves to be a pain, you could also return an immediate object. Cheers, Jacques Garrigue