functors and type constraints

Pierre BOULET (Pierre.Boulet@prism.uvsq.fr)
13 Nov 1996 16:42:53 +0100

To: caml-list@pauillac.inria.fr
Subject: functors and type constraints
From: Pierre BOULET <Pierre.Boulet@prism.uvsq.fr>
Date: 13 Nov 1996 16:42:53 +0100

[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