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

[Olivier Andrieu <andrieu@ijm.jussieu.fr>]

 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