Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

include et application de foncteur #8451

Closed
vicuna opened this issue Jan 21, 2004 · 3 comments
Closed

include et application de foncteur #8451

vicuna opened this issue Jan 21, 2004 · 3 comments

Comments

@vicuna
Copy link

vicuna commented Jan 21, 2004

Original bug ID: 2049
Reporter: administrator
Status: closed (set by @xavierleroy on 2013-08-31T10:46:13Z)
Resolution: fixed
Priority: normal
Severity: feature
Fixed in version: 3.12.0
Category: ~DO NOT USE (was: OCaml general)
Monitored by: "Julien Signoles"

Bug description

Full_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

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

@vicuna
Copy link
Author

vicuna commented Feb 17, 2004

Comment author: administrator

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

@vicuna
Copy link
Author

vicuna commented Feb 17, 2004

Comment author: administrator

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

@vicuna
Copy link
Author

vicuna commented Jan 27, 2012

Comment author: @xavierleroy

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant