Version française
Home     About     Download     Resources     Contact us    
Browse thread
functors and type constraints
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Pierre BOULET <Pierre.Boulet@p...>
Subject: functors and type constraints
[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