Re: functors and type constraints

Re: functors and type constraints

[Jocelyn Serot]

Hello,

In his last post, P. Boulet <Pierre.Boulet@prism.uvsq.fr> says:

> hello,
> 
> I have a problem with some complicated type constraints with Objective
> Caml version 1.02. Let have an example:
> 
> [stuff deleted]
> 
> 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?

I understand your problem as follows: given a function f to convert between
TAGs, you want to build a function to convert between ARBREs.

I recently came across a very similar problem dealing, respectively,
with PIXELs and IMAGEs.
Here's the solution i finally wrote, adapted a bit to fit to your definitions:

----------------------------- trad.ml ------------------------------------------

module type TAG = sig type t end;;

module type ARBRE = sig type tag type quast 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}
    end;;

module type TRAD = sig type t1 type t2 val f : t1 -> t2 end;;

module type Make_trad = functor
	(A1 : ARBRE) -> functor
	(A2 : ARBRE) -> functor
	(F  : sig val f : A1.tag -> A2.tag end)
	-> TRAD with type t1 = A1.tag and type t2 = A2.tag;;

module T1 : TAG = struct type t = float end;;
module T2 : TAG = struct type t = int end;;
module A1 : ARBRE = Make_arbre(T1);;
module A2 : ARBRE = Make_arbre(T2);;

module Trad = Make_trad (A1) (A2) (struct let f = truncate end);;

----------------------------- trad.ml ------------------------------------------

Hope that helps.

-------------------------------------------------------------------------------
E-mail: jserot@epcc.ed.ac.uk (->Nov 29 1996) ................................
S-mail: LASMEA - URA 1793 CNRS, Universite Blaise Pascal, 63177 Aubiere cedex
Tel: (33) 73.40.73.30 - Fax: (33) 73.40.72.62 ...............................
.... http://wwwlasmea.univ-bpclermont.fr/Personnel/Jocelyn.Serot/Welcome.html
-------------------------------------------------------------------------------

functors and type constraints

[Pierre BOULET]

[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

Re: functors and type constraints

[Christian Boos]

[-- 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