0003520: mutable fields and interfaces

Notes
(0000249) administrator (administrator) 2005-03-07 15:09	Salut Jean-Christophe, > I don't know whether it is a bug report or a feature request. A mon avis ca rentre dans la categorie "bug request"... > module Foo : sig > type t = { a : int; b : int } > end = struct > type t = { a : int; mutable b : int } > end > > but this is currently rejected by the ocaml compiler. Il a bien raison, le compilo: si on l'accepte ca permet de creer une reference polymorphe et donc de casser le systeme de types. > Note: I would like to do it also when the type t is "private" in the > interface. La c'est plus facile: si le type t est "private" alors tu ne peux pas faire d'affectation sur ses champs, donc ton programme les voit deja comme non-mutables (sauf pour generaliser les valeurs polymorphes au niveau du typage). -- Damien

(0000250) administrator (administrator) 2005-03-07 16:07	Salut, > A mon avis ca rentre dans la categorie "bug request"... > > > module Foo : sig > > type t = { a : int; b : int } > > end = struct > > type t = { a : int; mutable b : int } > > end > > > > but this is currently rejected by the ocaml compiler. > > Il a bien raison, le compilo: si on l'accepte ca permet de creer une > reference polymorphe et donc de casser le systeme de types. Je n'avais pas vu ce problème potentiel... > > Note: I would like to do it also when the type t is "private" in the > > interface. > > La c'est plus facile: si le type t est "private" alors tu ne peux pas faire > d'affectation sur ses champs, donc ton programme les voit deja comme > non-mutables (sauf pour generaliser les valeurs polymorphes au niveau > du typage). Je ne comprends pas en quoi le caractère "private" aiderait, car je pourrais de toutes façons exporter une fonction de création qui soit polymorphe, non ? -- Jean-Christophe

(0000251) administrator (administrator) 2005-03-08 10:35	From: Jean-Christophe.Filliatre@lri.fr > > A mon avis ca rentre dans la categorie "bug request"... > > > > > module Foo : sig > > > type t = { a : int; b : int } > > > end = struct > > > type t = { a : int; mutable b : int } > > > end > > > > > > but this is currently rejected by the ocaml compiler. > > > > Il a bien raison, le compilo: si on l'accepte ca permet de creer une > > reference polymorphe et donc de casser le systeme de types. > > Je n'avais pas vu ce probleme potentiel... > > > > Note: I would like to do it also when the type t is "private" in the > > > interface. > > > > La c'est plus facile: si le type t est "private" alors tu ne peux pas faire > > d'affectation sur ses champs, donc ton programme les voit deja comme > > non-mutables (sauf pour generaliser les valeurs polymorphes au niveau > > du typage). > > Je ne comprends pas en quoi le caractere "private" aiderait, car je > pourrais de toutes facons exporter une fonction de creation qui soit > polymorphe, non ? Oui, mais la value restriction garantit que le resultat de cette fonction ne sera pas polymorphe, lui. Avec la "relaxed restriction", il faut aussi se mefier de la variance des parametres. Mais justement, dans 3.09 la variance des types prives est explicite. Donc module Foo : sig type 'a t = private {x:'a} val create : 'a -> 'a t val set : 'a t -> 'a -> unit end = struct type 'a t = {mutable x:'a} let create x = {x=x} let set r x = r.x <- x end serait "sound", et la modification "type +'a = private {x:'a}" (unsound) refusee pour variance incorrecte. Reste que ca veut dire que l'interface ment sur la semantique, declarant immutable un champ qui est mutable. C'est un choix a faire. Et ca n'ajoute que si on decide que meme dans un type prive', on a le droit d'assigner aux champs mutables, sinon c'est juste une syntaxe differente pour la semantique actuelle (dans les types prives, on ne peut pas muter les champs directement). Autrement dit, l'idee serait de rafiner la semantique des types prives, pour permettre de choisir explicitement quels champs sont rendus immutables; ce n'est pas absurde. Jacques

(0000252) administrator (administrator) 2005-03-14 12:07	> From: Jean-Christophe.Filliatre@lri.fr [...] > > Je ne comprends pas en quoi le caractere "private" aiderait, car je > > pourrais de toutes facons exporter une fonction de creation qui soit > > polymorphe, non ? > > Oui, mais la value restriction garantit que le resultat de cette > fonction ne sera pas polymorphe, lui. > Avec la "relaxed restriction", il faut aussi se mefier de la > variance des parametres. Mais justement, dans 3.09 la variance des > types prives est explicite. [...] > Reste que ca veut dire que l'interface ment sur la semantique, > declarant immutable un champ qui est mutable. C'est un choix a faire. > Et ca n'ajoute que si on decide que meme dans un type prive', on a > le droit d'assigner aux champs mutables, sinon c'est juste une syntaxe > differente pour la semantique actuelle (dans les types prives, on ne > peut pas muter les champs directement). > Autrement dit, l'idee serait de rafiner la semantique des types > prives, pour permettre de choisir explicitement quels champs sont > rendus immutables; ce n'est pas absurde. > > Jacques Ce n'est pas absurde, mais il est toujours dangereux de ``mentir sur la sémantique'': le compilo pourrait (avec raison) optimiser les valeurs constantes immédiates d'un type (qu'il croit être) sans champ mutable, en les partageant par exemple. Évidemment, le résultat d'un tel partage serait incompréhensible si les champs sont en fait mutés. La sémantique ``menteuse'' des interfaces invaliderait donc la CSE et le constant folding des valeurs pures (sans champ mutable); sauf à exiger de connaître l'implémentation des modules pour compiler le code qui en dépend, afin de certifier que les types déclarés non mutables dans les interfaces le sont réellement dans leur implémentation. Cela signifie donc qu'on perdrait un peu de la compilation séparée. Ce ``raffinement'' n'est donc pas anodin et peut-être même pas souhaitable du tout! Pierre

Issue History
Date Modified	Username	Field	Change
2005-11-18 10:13	administrator	New Issue

Relationships