[Camllist] to Caml maillist birthday :)

Valery A.Khamenya
 Christophe Raffalli
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Christophe Raffalli <christophe.raffalli@u...> 
Subject:  [Camllist] Bug ? + Mutable list in OCaml 3.07beta2... using type inference to infer mutability 
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 ?) All that using existing ocaml3.07beta2 (fails with 3.06)  interface file mutable_list.mli  type ('a, 'b) mlist = Nil  Cons of 'a * ('a, 'b) mlist (* The first argument is the type of the element in the list The second argument contains information about mutability: A function of type ('a, [> `MuteCdr] as 'b) mlist > ... may mute the cdr of its argument A function of type ('a, [> `MuteCar] as 'b) mlist > ... may mute the car of its argument *) val set_cdr : ('a, [> `MuteCdr] as 'b) mlist > ('a, 'b) mlist > unit val set_car : ('a, [> `MuteCar]) mlist > 'a > unit val map : ('a > 'b) > ('a, 'c) mlist > ('b, 'd) mlist (* very fun: map is tail recursive, using set_cdr in its implementation but still the type checking detects that it does not mute its arguments and it also detects (but this is easier) that the second argument shares cells with the result but not the first *) val mapq : ('a > 'a) > ('a, [> `MuteCar]) mlist > unit (* Not the expected type ! why does it works for map and not append ? *) val append : ('a, 'b) mlist > ('a, [> `MuteCdr ] as 'c) mlist > ('a, 'c) mlist val appendq : ('a, [> `MuteCdr] as 'b) mlist > ('a, 'b) mlist > ('a, 'b) mlist  implementation : mutable_list.ml  type ('a,'mute) mlist = Nil  Cons of 'a * ('a,'mute) mlist let set_cdr (l : ('a,[>`MuteCdr] as 'b) mlist) (x : ('a,'b) mlist) = match l with Nil > raise (Invalid_argument "set_cdr")  Cons(_,_) as l > Obj.set_field (Obj.repr l) 1 (Obj.repr x) let set_car (l : ('a,[>`MuteCar] as 'b) mlist) (x : 'a) = match l with Nil > raise (Invalid_argument "set_car")  Cons(_,_) as l > Obj.set_field (Obj.repr l) 0 (Obj.repr x) let map f l = match l with Nil > Nil  Cons(x,l) > let acc0 = Cons(f x,Nil) in let rec fn acc = function Nil > acc0  Cons(x,l) > let acc' = Cons(f x,Nil) in set_cdr acc acc'; fn acc' l in fn acc0 l let rec mapq f l = match l with Nil > ()  Cons(x,l') > set_car l' (f x); mapq f l 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 let rec appendq l l' = match l' with Nil > l'  Cons(_,_) > let rec fn = function Nil > assert false  Cons(x,Nil) as l > set_cdr l l'  Cons(x,l) > fn l in fn l; l  Christophe Raffalli Université de Savoie Batiment Le Chablais, bureau 21 73376 Le BourgetduLac Cedex tél: (33) 4 79 75 81 03 fax: (33) 4 79 75 87 42 mail: Christophe.Raffalli@univsavoie.fr www: http://www.lama.univsavoie.fr/~RAFFALLI  IMPORTANT: this mail is signed using PGP/MIME At least Enigmail/Mozilla, mutt or evolution can check this signature 