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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 35E58BBAF for ; Mon, 23 Jun 2008 12:27:09 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhYCABgXX0jAXQImiGdsb2JhbACSawEBAQ8gnSk X-IronPort-AV: E=Sophos;i="4.27,689,1204498800"; d="scan'208";a="12439835" Received: from discorde.inria.fr ([192.93.2.38]) by mail2-smtp-roc.national.inria.fr with ESMTP; 23 Jun 2008 12:27:08 +0200 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id m5NAQjRM027320 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Mon, 23 Jun 2008 12:27:08 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApoEAFQXX0iCNhAB/2dsb2JhbACwRg X-IronPort-AV: E=Sophos;i="4.27,689,1204498800"; d="scan'208";a="14395639" Received: from kurims.kurims.kyoto-u.ac.jp ([130.54.16.1]) by mail3-smtp-sop.national.inria.fr with ESMTP; 23 Jun 2008 12:27:07 +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 m5NAR3Lh027092; Mon, 23 Jun 2008 19:27:03 +0900 (JST) Date: Mon, 23 Jun 2008 19:27:03 +0900 (JST) Message-Id: <20080623.192703.27793304.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: <1214089919.6190.13.camel@Blefuscu> References: <1214089919.6190.13.camel@Blefuscu> X-Mailer: Mew version 5.2 on Emacs 22.1 / 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 485F7A65.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; univ-orleans:01 variants:01 ocaml:01 camlp:01 runtime:01 ocamlc:01 variants:01 ocamlc:01 cmi:01 mli:01 polymorphic:01 polymorphic:01 compile:01 encode:01 encode:01 From: David Teller > I have been thinking for some time about using polymorphic variants to > encode some aspects of a types-and-effects type system in OCaml using > Camlp4. While the idea is still quite fuzzy, I have the feeling that, if > I could have a value (let's call it "witness") with type > [> ] ref > which I could "touch" into becoming > [> `A] ref > then > [> `A | `B] ref > etc. as effects `A, `B, etc. appear in the program, it could provide > interesting information on the effects of the program. > > Now, of course, I can't define a value with type ref [> ] or even with > type ref [> `dummy]. That is, when compiling a module consisting only in > a declaration such as > let witness = ref `dummy > I'm faced with the good old "cannot be generalised" error message. This > strikes me as normal -- I'm sure that, with the right modifications on > witness, I could cause runtime type inconsistencies for any client > attempting to read the value of witness. However, in this case, I'm not > going to read any value from witness, ever. I only want to "touch" it > into becoming something a tad more complex, which I could then look at > with ocamlc -i or such. > > My question is: is there a way to hijack polymorphic variants into doing > what I wish? Or to encode this behaviour somehow? I'm not sure how far you can go with this approach, but if all you want is to know the type inferred for witness, while this type is clearly not generalizable (otherwise you won't be able to collect information), I can think of several tricks. * first remark: ocamlc -i works even with non-generalizable types, as it does not generate any .cmi. * if you want to be still able to compile, you can write a .mli file not including the witness. ocamlc -i on the .ml will still show you the witness. * other solution: put everything inside a function, so that the type variable is still generalizable after typing the function. Hope this helps, Jacques Garrigue