From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id KAA24375 for caml-redistribution; Thu, 14 Nov 1996 10:28:55 +0100 (MET) Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id QAA11293 for ; Wed, 13 Nov 1996 16:43:05 +0100 (MET) Received: from soleil.uvsq.fr (soleil.uvsq.fr [193.51.24.1]) by concorde.inria.fr (8.7.6/8.7.1) with ESMTP id QAA10326 for ; Wed, 13 Nov 1996 16:43:05 +0100 (MET) Received: from guillotin.prism.uvsq.fr (guillotin.prism.uvsq.fr [193.51.25.1]) by soleil.uvsq.fr (8.8.0/jtpda-5.2) with ESMTP id QAA11329 for ; Wed, 13 Nov 1996 16:43:03 +0100 (MET) Received: from morisot.prism.uvsq.fr (morisot.prism.uvsq.fr [193.51.25.80]) by guillotin.prism.uvsq.fr (8.8.0/jtpda-5.2) with ESMTP id QAA00967 for ; Wed, 13 Nov 1996 16:43:01 +0100 (MET) Received: from (bop@localhost) by morisot.prism.uvsq.fr (8.7.6/jtpda-5.1) id QAA00766 ; Wed, 13 Nov 1996 16:42:59 +0100 (MET) To: caml-list@pauillac.inria.fr Subject: functors and type constraints From: Pierre BOULET Date: 13 Nov 1996 16:42:53 +0100 Message-ID: X-Mailer: Gnus v5.2.25/XEmacs 19.14 MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit Sender: weis [An english version follows] bonjour, j'ai un problème avec certaines contraintes de type un peu compliquées avec Objective Caml version 1.02. Le plus simple est de prendre un exemple : Voici les définitions de modules. L'idée générale est de paramétrer le module ARBRE par le module TAG. Les tags sont des étiquettes caractérisant les feuilles de l'arbre. Le polymorphisme n'est pas suffisant ici car j'ai besoin de faire des opérations sur ces étiquettes quand je fais des opérations sur les arbres (des changements de variables ou des comparaisons, par exemple). module type TAG = sig type t val ... end;; module type ARBRE = sig type tag type quast val ... end;; module type MAKE_ARBRE = functor (T : TAG) -> (ARBRE with type tag = T.t);; module Make_arbre : MAKE_ARBRE = functor (T : TAG) -> struct type tag = T.t type quast = {tag : tag; ...} val ... end;; Je voudrais ensuite écrire un traducteur de A1=Make_arbre(Tag1) vers A2=Make_arbre(Tag2) à partir d'un traducteur de Tag1 vers Tag2. module type TRAD = sig type from;; type into;; val f : from -> into;; end;; module type TRAD_ARBRE = functor (A1 : ARBRE) -> functor (A2 : ARBRE) -> functor (T : TRAD with type from = A1.tag and type into = A2.tag) -> (TRAD with type from = A1.quast and type into = A2.quast);; module Make_trad : TRAD_ARBRE = functor (A1 : ARBRE) -> functor (A2 : ARBRE) -> functor (T : TRAD with type from = A1.tag and type into = A2.tag) -> struct type from = A1.quast;; type into = A2.quast;; val f ... end;; Jusqu'ici tout se compile bien. Instancions maintenant les modules. module T1 : TAG = struct ... end;; module T2 : TAG = struct ... end;; module A1 : ARBRE = Make_arbre (T1);; module A2 : ARBRE = Make_arbre (T2);; module Trad_Tag : TRAD = struct type from = T1.t type into = T2.t val f ... end;; Le problème apparaît lors de la compilation de la phrase suivante : module Trad_Arbre : TRAD = Make_trad (A1) (A2) (Trad_Tag);; Signature mismatch: Modules do not match: sig type from = Trad_Tag.from type into = Trad_Tag.into val f : from -> into end is not included in sig type from = A1.tag type into = A2.tag val f : from -> into end Type declarations do not match: type from = Trad_Tag.from is not included in type from = A1.tag Ces types sont pourtant égaux. Je vois bien un problème de définition abstraite de ces types, mais alors, comment indiquer au vérificateur de types qu'ils sont bien égaux ? cordialement, Pierre Boulet ---------------------------------------------------------------------- [english version] hello, I have a problem with some complicated type constraints with Objective Caml version 1.02. Let have an example: Here are the module definitions. The idea is to parameterize module ARBRE (the french world for tree) by module TAG. Tags add some information to the leaves of the tree ARBRE. Polymorphism is not sufficient here because I need to do some operations on these tags when doing some general operations on trees (variable substitutions or comparisons for example). module type TAG = sig type t val ... end;; module type ARBRE = sig type tag type quast val ... end;; module type MAKE_ARBRE = functor (T : TAG) -> (ARBRE with type tag = T.t);; module Make_arbre : MAKE_ARBRE = functor (T : TAG) -> struct type tag = T.t type quast = {tag : tag; ...} val ... end;; I would then like to write a translator from A1=Make_arbre(Tag1) to A2=Make_arbre(Tag2) from a translator from Tag1 to Tag2. module type TRAD = sig type from;; type into;; val f : from -> into;; end;; module type TRAD_ARBRE = functor (A1 : ARBRE) -> functor (A2 : ARBRE) -> functor (T : TRAD with type from = A1.tag and type into = A2.tag) -> (TRAD with type from = A1.quast and type into = A2.quast);; module Make_trad : TRAD_ARBRE = functor (A1 : ARBRE) -> functor (A2 : ARBRE) -> functor (T : TRAD with type from = A1.tag and type into = A2.tag) -> struct type from = A1.quast;; type into = A2.quast;; val f ... end;; Everything goes find till now. Let's instanciate the modules now. module T1 : TAG = struct ... end;; module T2 : TAG = struct ... end;; module A1 : ARBRE = Make_arbre (T1);; module A2 : ARBRE = Make_arbre (T2);; module Trad_Tag : TRAD = struct type from = T1.t type into = T2.t val f ... end;; The problem appears during the compilation of the following statement: module Trad_Arbre : TRAD = Make_trad (A1) (A2) (Trad_Tag);; Signature mismatch: Modules do not match: sig type from = Trad_Tag.from type into = Trad_Tag.into val f : from -> into end is not included in sig type from = A1.tag type into = A2.tag val f : from -> into end Type declarations do not match: type from = Trad_Tag.from is not included in type from = A1.tag These types are equal though. I imagine a problem of abstract definition of some types, but how can I signify to the compiler that these types are equal? sincerely, -- Pierre BOULET bureau : 415 Laboratoire PRiSM tel : (+33) (1) 39.25.40.71 45, av. des Etats-Unis email: Pierre.Boulet@prism.uvsq.fr 78035 Versailles Cedex WWW : http://www.prism.uvsq.fr/public/bop