Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0003520OCamlOCaml generalpublic2005-03-07 14:312005-03-08 05:33
Reporteradministrator 
Assigned To 
PrioritynormalSeverityfeatureReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0003520: mutable fields and interfaces
Description
Dear ocaml developpers,

I don't know whether it is a bug report or a feature request.

I would like not to include the "mutable" modifier of a record field
in an interface, as in

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.

Note: I would like to do it also when the type t is "private" in the
interface.

Best regards,
--
Jean-Christophe

TagsNo tags attached.
Attached Files

- Relationships

-  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


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker