Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002049OCamlOCaml generalpublic2004-01-21 15:042013-08-31 12:46
Reporteradministrator 
Assigned To 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version3.12.0 
Summary0002049: include et application de foncteur
DescriptionFull_Name: Julien Signoles
Version: 3.06 / 3.07
OS: Linux
Submission from: pc8-123.lri.fr (129.175.8.123)



Bonjour,

Il semble y avoir un bug dans l'application de foncteurs et les includes.
Le code joint ci-dessous ne compile pas. Or il compile avec succès si

1. on remplace "module W=V module S=Set.Make(W)" par "module S=Set.Make(V)"
   (cf le premier commentaire)

ou bien si

2. on remplace manuellement "include G" par ce qu'il est censé faire
   (cf le second commentaire)

Cordialement,
--
Julien Signoles et Jean-Christophe Filliâtre


--------------------------------------------------------------

module type COMPARABLE = sig
  type t
  val compare : t -> t -> int
  val hash : t -> int
  val equal : t -> t -> bool
end

module type S = sig
  module Vertex : COMPARABLE
  type t
  val iter_edges : (Vertex.t -> unit) -> t -> unit
end

module Iterator(G : S) = struct

  module P = struct
    type t = G.Vertex.t
    let compare _ _ = assert false
    let equal _ _ = assert false
    let hash _ = assert false
  end

  module H = Hashtbl.Make(P)

  let iter_edges f g =
    let h = H.create 97 in
    G.iter_edges (fun v1 -> H.add h v1 ()) g
end

module Labeled (V: COMPARABLE) : S =
struct
  module G = struct
    module Vertex = V

    module W = V
    module S = Set.Make(W)
(* ceci marche:
module S = Set.Make(V)
*)

    type t = S.t
    let iter_edges = S.iter
  end

  include G
(* une inclusion manuelle fonctionne ?galement:
  module Vertex = G.Vertex
  module W = G.W
  type t = G.t
  let iter_edges = G.iter_edges
*)

  include Iterator(G)
end

TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000198)
administrator (administrator)
2004-02-17 15:31

Bonjour Julien,

> Il semble y avoir un bug dans l'application de foncteurs et les includes.
> Le code joint ci-dessous ne compile pas. Or il compile avec succès si
> 1. on remplace "module W=V module S=Set.Make(W)" par "module S=Set.Make(V)"
> (cf le premier commentaire)
> ou bien si
> 2. on remplace manuellement "include G" par ce qu'il est censé faire
> (cf le second commentaire)

Tu es tombé sur une faiblesse connue des modules applicatifs. En
résumé, si F est un foncteur avec un type abstrait "t" dans son résultat,
et si on fait:

        module A = F(X)
        module Y = X
        module B = F(Y)

alors A.t = F(X).t et B.t = F(Y).t, mais on n'a pas F(X).t = F(Y).t,
et donc A.t et B.t sont incompatibles. La raison profonde est que
le système de modules ne sait pas exprimer que X = Y, mais seulement
que toutes les composantes de types de X sont égales aux composantes
correspondantes de Y...

Dans ton exemple, on voit apparaître le problème avec les types
suivants de la structure résultat du foncteur Labeled. Dans le code
d'origine,

        t = S.t = Set.Make(W).t
        G.t = G.S.t = Set.Make(G.W).t

alors que le reste du code exige t = G.t.

Avec l'include expansé à la main, le "strengthening" est fait sur
chaque composante du module G et non pas sur G tout entier, et coup de
pot ça fait ce que tu veux:

        t = S.t = Set.Make(G.W).t
        G.t = G.S.t = Set.Make(G.W).t

Et si tu changes "module W=V module S=Set.Make(W)" par "module S=Set.Make(V)",
comme c'est le même V partout dans le module, et on a aussi ce que tu veux:

        t = S.t = Set.Make(V).t
        G.t = G.S.t = Set.Make(V).t

Enfin, si on met une contrainte de signature pour oublier tout ce
bazar de foncteurs applicatifs, ça marche aussi:

module Labeled (V: COMPARABLE) : S =
struct
  module G = struct
    module Vertex = V
    module W = V
    module S : (Set.S with type elt = W.t) = Set.Make(W) (* <--- *)
    type t = S.t
    let iter_edges = S.iter
  end
  include G
  include Iterator(G)
end

Bref, c'est la pagaille, mais je ne vois pas comment corriger cela
sans changements profonds dans les règles du système de modules
(i.e. ou bien on vire les modules applicatifs, ou bien on ajoute des
notions d'équivalence entre modules, et non plus juste entre types).

Amitiés,

- Xavier

(0000199)
administrator (administrator)
2004-02-17 15:32

This boils down to F(A).t != F(B).t even if A is defined as equal to B. The
current module system just cannot express this. Unlikely to change any time
soon, but I'll leave it as a feature wish just in case. -XL, 2004-02-17
(0006822)
xleroy (administrator)
2012-01-27 12:04

Option -no-app-funct, introduced in 3.12.0, is effective here and in many similar examples: the given code sample typechecks fine with -no-app-funct.

- Issue History
Date Modified Username Field Change
2005-11-18 10:13 administrator New Issue
2012-01-27 12:04 xleroy Note Added: 0006822
2012-01-27 12:04 xleroy Status acknowledged => resolved
2012-01-27 12:04 xleroy Resolution open => fixed
2012-01-27 12:04 xleroy Fixed in Version => 3.12.0
2012-01-27 12:04 xleroy Description Updated View Revisions
2013-08-31 12:46 xleroy Status resolved => closed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker