From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id LAA20911; Tue, 9 Sep 2003 11:28:32 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id LAA19134 for ; Tue, 9 Sep 2003 11:28:31 +0200 (MET DST) Received: from kraid.nerim.net (smtp-102-tuesday.nerim.net [62.4.16.102]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id h899SVT07042 for ; Tue, 9 Sep 2003 11:28:31 +0200 (MET DST) Received: from karryall.dnsalias.org (karryall.dnsalias.org [62.4.18.180]) by kraid.nerim.net (Postfix) with ESMTP id 5CF4440FA5; Tue, 9 Sep 2003 11:28:30 +0200 (CEST) Received: by karryall.dnsalias.org (Postfix, from userid 500) id 1DF201A0603; Tue, 9 Sep 2003 11:28:30 +0200 (CEST) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <16221.40253.994424.109094@karryall.dnsalias.org> Date: Tue, 9 Sep 2003 11:28:29 +0200 From: Olivier Andrieu To: Christophe Raffalli Cc: caml-list@inria.fr Subject: Re: [Caml-list] Bug ? + Mutable list in OCaml 3.07beta2... using type inference to infer mutability In-Reply-To: <3F5D7629.7060901@univ-savoie.fr> References: <07510479.20030904212106@mail.ru> <3F5D7629.7060901@univ-savoie.fr> X-Mailer: VM 7.17 under Emacs 21.2.1 X-Loop: caml-list@inria.fr X-Spam: no; 0.00; andrieu:01 andrieu:01 caml-list:01 bug:01 3.07:01 inference:01 infer:01 mutability:01 raffalli:01 infer:01 inference:01 bug:01 acc':01 acc':01 mutated:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Christophe Raffalli [Tuesday 9 September 2003] : > Here is an implementation of mutable list where we use the typing of > polymorphic variant (but no polymorphic variant) to infer if a program > can mute a list ! > > And even better, you can program the tail_rec version of map using > set_cdr and have the type inference telling you that it does not mute > its argument ... but I think this is a bug ? (if it is not, how to get > the same type for append ?) no I don't think it's a bug : > let append l l' = match l with > Nil -> l' > | Cons(x,l) -> > let acc0 = Cons(x,Nil) in > let rec fn acc = function > Nil -> set_cdr acc l' > | Cons(x,l) -> > let acc' = Cons(x,Nil) in > set_cdr acc acc'; > fn acc' l > in fn acc0 l; acc0 here, the set_cdr acc l' in the second Nil causes l' to have type (_, [>`MutCdr]) since it comes as second argument of set_cdr. I think the problem is with your set_cdr function. The second argument shouldn't have the same 'mute parameter than the first one since the second argument is not mutated. val set_cdr : ('a, [> `MuteCdr ]) mlist -> ('a, 'b) mlist -> unit With this type, append has the "right" type. The appendq type can come right too but the function must be modified a bit : ,---- | let rec appendq l l' = match l with | | Nil -> l' | | Cons(_,_) -> | let rec fn l = match l with | Nil -> assert false | | Cons(_, Nil) -> | set_cdr l l' ; l | | Cons(_, l) -> | fn l | in | fn l `---- Anyway, as usual with phantom types, they don't enfore much until the type representation is abstracted. And if you had abstracted the mlist definition with module constraint, you wouldn't be able to come up with these types : for instance, the return type of map would be ('b, [> `MuteCdr ]) mlist since you return a cell that was set_cdr'ed (and the type of the second argument of append would be ('b, [> `MuteCdr ]) mlist again). -- Olivier ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners