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.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 108E5BC0A for ; Wed, 6 Jun 2007 23:23:01 +0200 (CEST) Received: from smtp3-g19.free.fr (smtp3-g19.free.fr [212.27.42.29]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l56LMwUa011315 for ; Wed, 6 Jun 2007 23:23:00 +0200 Received: from Tocksi.local (lns-bzn-61-82-250-109-73.adsl.proxad.net [82.250.109.73]) by smtp3-g19.free.fr (Postfix) with ESMTP id 711F95A229; Wed, 6 Jun 2007 23:22:58 +0200 (CEST) Message-ID: <466725B0.2010308@univ-savoie.fr> Date: Wed, 06 Jun 2007 23:22:56 +0200 From: Christophe Raffalli User-Agent: Thunderbird 2.0.0.0 (Macintosh/20070326) MIME-Version: 1.0 To: David Teller , caml-list@yquem.inria.fr Subject: Re: [Caml-list] Labelling trees References: <1181158983.9266.12.camel@Blefuscu> In-Reply-To: <1181158983.9266.12.camel@Blefuscu> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit X-Miltered: at concorde with ID 466725B2.002 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; christophe:01 raffalli:01 christophe:01 raffalli:01 univ-savoie:01 checker:01 syntax:01 annotations:01 checker:01 annotations:01 intuitively:01 functors:01 univ-savoie:01 val:01 val:01 David Teller a écrit : > Hi everyone, > I'm currently in the very first stages of writing down a prototype > implementation of a type checker. At the moment, I'm looking for "the > nicest" way of labelling my abstract syntax tree with type annotations > -- without corrupting the AST at all, if possible. > > > Say I have > > type my_expression = ESomeConstructor of ... > | ESomeConstructor2 of ... > | ESomeConstructor3 of my_function > and my_function = FSomeConstructor ... > > > A first idea would be to replace this structures with > > type 'a my_expression = ESomeConstructor of ... > | ESomeConstructor2 of ... > | ESomeConstructor3 of 'a my_function > and 'a my_function = FSomeConstructor ... > > That would let me annotate instances of my_expression or my_function > with informations of type 'a. However, this won't scale in case I decide > that my static checker will need annotations of different types for > my_expression and my_function. Of course, my AST is actually a tad more > complex and would require about 15 type arguments, which I don't > consider very nice. > > Intuitively, using functors will yield the same kind of half-satisfying > results. > > Any suggestions ? > > I can't ressit ... use pml (http://www.lama.univ-savoie.fr/~raffalli/repos/pml) in one week from now (I am currently implementing what you need, this is why I am answering). You will be able to write things like : type AST = Nope[] | App[AST,AST] val rec decorate_with_size ast = Nope[] -> { Nope[] with val size = 0 } (* Here I am lying pml does not support native int yet, nor it will in one week *) | App[u,v] -> let u' = decorate_with_size u and v' = decorate_with_size v in { App[decorate u, decorate v] with val size = 1 + u'.size + v'.size } Moreover, the result type of decorate_with_size (which is {AST with val size : int }) is a subtype of AST and this subtyping is completely implicit (no typecast needed) ... OK, pml does not have native int (it has multiprecision nat) and no IO yet, it is interpreted (but not that slow), probably buggy ... But you will soon be able to specify and prove your code too ... Cheers, Christophe