Re: [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: 3293 bytes --]

Olivier Andrieu wrote:
>  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 aggree, waht I think is a bug is the type of map:

val map : ('a -> 'b) -> ('a, 'c) mlist -> ('b, 'd) mlist

which should be (unfortunatelly)

val map : ('a -> 'b) -> ('a, 'c) mlist -> ('b, [> `Mute cdr] as 'd) mlist

This set_cdt is used on cons cells used by the result of map

> 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.

Yes but as soon as cons-cell are in the same list they must have the 
same 'mute parameters to be sure everything goes well if the list are 
mutated later.

If would be nice if they could have a different 'mute parameter before 
and the same after the qet_cdr, but his makes no sense for static typing.
> 
>   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.

that's for sure

> 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).
> 

I am not sure that's the problem with map, because I am not sure ocaml 
uses that fact that the type 'a mlist is constant. I should try that ?



-- 
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 --]