[Caml-list] to Caml maillist birthday :)

[Caml-list] to Caml maillist birthday :)

[Valery A.Khamenya]

Hello caml-devels,

 If we consider the date from the following page as a start of Caml
 maillist: 
 http://pauillac.inria.fr/bin/wilma/caml-list
 
 Then here is my tiny present to Caml maillist birthday:
 http://khamenya.ru/ocaml/activity/

 P.S. I hope this my message will not come twice to a maillist... :-/

-- 
Best regards,
Valery                          mailto:khamenya@mail.ru

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

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

[Christophe Raffalli]

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

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

[Olivier Andrieu]

 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

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

[Christophe Raffalli]

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