Re: functors and type constraints

[Christian Boos <boos@arthur.u-strasbg.fr>]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 3003 bytes --]

Pierre BOULET writes:
 > [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 :
 
<< meme exemple repris dans la suite >>

Votre probleme est le suivant : vous definissez des contraintes de partage
de type au niveau de la definition des types des foncteurs. Ces contraintes 
ne sont pas apparentes dans les types des modules utilises par ces foncteurs.
Or, lorsque vous instanciez vos modules, vous le faites avec une coercition 
vers la signature correspondante, ce qui n'est pas obligatoire et qui a 
comme effet "pervers" de rendre les types qui y sont definis abstraits.
C'est pourquoi lors de la creation de modules en utilisant les foncteurs,
le compilateur ne peut plus verifier cette egalite des types. La solution est
donc de definir les modules sans les typer explicitement.

Voila l'exemple complet (pret a passer a ocaml !) :


  module type TAG =
    sig
      type t
      val const : t
    end;;
  
  module type ARBRE =
    sig
      type tag
      type quast
      val create : tag -> quast
      val get_tag : quast -> tag
    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}
	let create t = { tag = t }
	let get_tag q = q.tag
      end;;
  
  
  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
	let f q1 = A2.create (T.f (A1.get_tag q1))
      end;;
  

(* Dans l'instanciation de module, il est inutile (et indesirable !) 
   de typer 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;;

  Au lieu de cela, il faut ecrire :
*)
   

  module T1 = struct type t = int let const = 1 end;;
  module T2 = struct type t = float let const = 1. end;;
  module A1 = Make_arbre (T1);;
  module A2 = Make_arbre (T2);;
  
  module Trad_Tag = 
    struct 
      type from = T1.t
      type into = T2.t
      let f t1 = float t1
    end;;
  
  
  module Trad_Arbre : TRAD = Make_trad (A1) (A2) (Trad_Tag);;


--- 

Sorry, no english version today (there's an english version in the initial
posting, and the code above solves the problem).


-- Christian Boos