[Caml-list] Bug ? + Mutable list in OCaml 3.07beta2... using type inference to infer mutability

[Christophe Raffalli <christophe.raffalli@univ-savoie.fr>]

[-- Attachment #1: Type: text/plain, Size: 3361 bytes --]


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 ocaml-3.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 Bourget-du-Lac Cedex

tél: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
---------------------------------------------
IMPORTANT: this mail is signed using PGP/MIME
At least Enigmail/Mozilla, mutt or evolution
can check this signature
---------------------------------------------


[-- Attachment #2: Type: application/pgp-signature, Size: 252 bytes --]