OCaml 2.0

OCaml 2.0

[Vladimir Vyskocil]

Bonjour,

Suite a la sortie de la version 2.0 d'Objective Caml, nous nous sommes
lance dans le "portage"
de notre logiciel depuis la version 1.07 avec l'aide de ocaml1to2. Nous
avons rencontre les
problemes suivants :

- Nous avons des classes marquees closed qui posent probleme avec
Ocaml2.0, l'explication donnee
dans le fichier README de ocaml1to2 :
   <<It usually suffices to introduce coercions (self :> c) from the
        self type to a known closed class type c >>
n'est pas tres parlante pour nous, pourriez vous donner un exemple
simple ?

- Dans l'exemple suivant :

class a =
    object (self)
    method call_pipo x = x#pipo self
    end
  ;;
Some type variables are unbound in this type:
  class a : object ('a) method call_pipo : < pipo : 'a -> 'b; .. > -> 'b
end
The method call_pipo has type
  < pipo : < call_pipo : 'a; .. > -> 'b; .. > -> 'b as 'a
where 'c is unbound

Le type 'c n'apparait pas dans la signature de la classe, a quoi
correspond t'il ?

- Dans l'exemple suivant :

class a =
  object (self)
  method call_pipo (x:b) = x#pipo self
  end
and b a =
  object
  method pipo (x:a):a = x
  end;;
This expression has type < call_pipo : b -> 'a; .. >
but is here used with type 'b
Self type cannot escape its class

pourriez vous expliquer ce message d'erreur et donner une maniere de
re-ecrire cela ?

                        Merci par avance

--
Vyskocil Vladimir
vvyskoci@sophia.inria.fr
http://www.inria.fr/safir/WHOSWHO/Vladimir.html

Re: OCaml 2.0

[Jerome Vouillon]

Bonjour,
 
On Wed, Aug 26, 1998 at 04:18:35PM +0200, Vladimir Vyskocil wrote:
> - Nous avons des classes marquees closed qui posent probleme avec
> Ocaml2.0, l'explication donnee
> dans le fichier README de ocaml1to2 :
>    <<It usually suffices to introduce coercions (self :> c) from the
>         self type to a known closed class type c >>
> n'est pas tres parlante pour nous, pourriez vous donner un exemple
> simple ?

Il y a un exemple dans le manuel, dans l'introduction aux objets
(http://caml.inria.fr/ocaml/htmlman/node3.html, section "Using
coercions"). Les exemples donnes a la fin de ce message doivent egalement
pouvoir vous aider.

> - Dans l'exemple suivant :
> 
> class a =
>     object (self)
>     method call_pipo x = x#pipo self
>     end
>   ;;
> Some type variables are unbound in this type:
>   class a : object ('a) method call_pipo : < pipo : 'a -> 'b; .. > -> 'b
> end
> The method call_pipo has type
>   < pipo : < call_pipo : 'a; .. > -> 'b; .. > -> 'b as 'a
> where 'c is unbound
> 
> Le type 'c n'apparait pas dans la signature de la classe, a quoi
> correspond t'il ?

Le type 'c represente en fait l'un des '..'. Vous devez preciser le
type de la method call_pipo afin que les types objets ouverts soient
instancies, ou bien soient lies par des parametres de la classe. Par
exemple :

      class ['a] a = object (self)
	method call_pipo (x : 'a) = x#pipo self
      end;;

> - Dans l'exemple suivant :
> 
> class a =
>   object (self)
>   method call_pipo (x:b) = x#pipo self
>   end
> and b a =
>   object
>   method pipo (x:a):a = x
>   end;;
> This expression has type < call_pipo : b -> 'a; .. >
> but is here used with type 'b
> Self type cannot escape its class
> 
> pourriez vous expliquer ce message d'erreur et donner une maniere de
> re-ecrire cela ?

La "row variable" ('..') du type de self doit pouvoir etre generalise
une fois que la classe a est typee, afin que le type reste extensible.
Pour cela, il ne faut pas qu'elle s'echappe de la classe.  Par
consequent, le type de self ne peut etre unifie avec une partie du
type de b, dont la portee est aussi bien la classe a que la classe b.

Il y a plusieurs facons de contourner ce probleme. La premiere est de
masquer la row variable par une coercion. Une difficulte est que l'on
voudrait faire une coercion vers le type a, ce qui n'est pas possible
car ce type n'est pas completement defini a cet endroit. Par
consequent, il faut definir explicitement le type de la coercion, en
utilisant par exemple un type de classe :

      class type a0 = object
	method call_pipo : b0 -> a0
      end and b0 = object
	method pipo : a0 -> a0
      end;;
      class a = object (self)
	method call_pipo (x:b) = x#pipo (self : #a0 :> a0)
      end and b a = object
	method pipo (x:a):a = x
      end;;

Une autre solution est de supprimer la recursion entre les classes a
et b en donnant un type plus general a la classe b :

      class ['a] b a = object
	method pipo (x:'a) = x
      end
      class a = object (self)
	method call_pipo (x : 'a b) = x#pipo self
      end

-- Jerome

Re: OCaml 2.0

[boos]

[sorry, no english version today :(]

Bonjour,

Vladimir Vyskocil writes:
 > Bonjour,
/.../
 > Some type variables are unbound in this type:
 >   class a : object ('a) method call_pipo : < pipo : 'a -> 'b; .. > -> 'b
 > end
 > The method call_pipo has type
 >   < pipo : < call_pipo : 'a; .. > -> 'b; .. > -> 'b as 'a
 > where 'c is unbound
 >
 > Le type 'c n'apparait pas dans la signature de la classe, a quoi
 > correspond t'il ?
 >

Il correspond au ".." qui apparait dans la classe.
Pour faire apparaître explicitement cette paramétrisation (notez la contrainte)

# class ['a] a =  object (self) method call_pipo (x : 'a)= (x#pipo self) end ;;
class ['a] a :
  object ('b)
    constraint 'a = < pipo : 'b -> 'c; .. >
    method call_pipo : 'a -> 'c
  end
#

------------------------------------------------------------------

 > - Dans l'exemple suivant :
 >
 > class a  >   object (self)
 >   method call_pipo (x:b) = x#pipo self
 >   end
 > and b a  >   object
 >   method pipo (x:a):a = x
 >   end;;
 > This expression has type < call_pipo : b -> 'a; .. >
 > but is here used with type 'b
 > Self type cannot escape its class
 >
 > pourriez vous expliquer ce message d'erreur et donner une maniere de
 > re-ecrire cela ?
 >


Ces problèmes sont discutés dans le manuel de référence, pages 34 à 37.
C'est vrai que le message d'erreur n'est pas très explicite, il
devrait au minimum dire qu'il s'agit d'un problème épineux et qu'il
faut lire la doc ...

Il faut se rendre compte que le type de self est non pas "a", mais
celui de la classe où 'self' est utilisé, ce qui inclut "a" mais
également toute classe héritant de "a".

Premier problème rencontré : la méthode "pipo" entraîne une contrainte
de type clairement non respectée ici. Il faudrait restreindre le type
de self à "a".

Second problème : une telle coercition n'est pas évidente à écrire.

(self : #a :> a) ne convient pas,  car le type "a" n'est pas encore
entièrement défini à ce moment là.
Pour préciser le type que l'on désire obtenir, on peut utiliser une
classe virtuelle (1), ou un type de classe (2).

(1) # class virtual ['a]  va 	object
		method virtual call_pipo : 'a -> 'a va
	end;;

class virtual ['a] va : object method virtual call_pipo : 'a -> 'a va end


(2) # class type ['a] ta = object method call_pipo : 'a -> 'a ta end;;

class type ['a] ta = object method call_pipo : 'a -> 'a ta end


On pourrait ensuite écrire la coercition (self :> b va) (1) ou (self :> b
ta) (2), mais cela ne fonctionne pas parce que self ne peut pas être
unifiée directement avec un type clos. En effet, le fait d'unifier
(self : <call_pipo : 'a -> 'a va; ..> as 'a) avec le type "b va"
impliquerait que self soit lui-même de type "b va", ce qui est faux
(self est de type "a", sous-type de "b va").
Il est nécessaire ici de préciser  explicitement le domaine de self.
Il faut donc écrire (self : b #va :> b va) (1), ou (self : b #ta :> b ta) (2).

L'exemple complet devient :

(1) #  class a 	object (self)
		inherit [b] va   (* cet héritage n'est pas nécessaire *)
		method call_pipo (x:b) = x#pipo (self : b #va :> b va)
	end
 and b 	object
		method pipo (x:a):a = x
	end;;

class a : object method call_pipo : b -> b va end
class b : object method pipo : b va -> b va end


(2) # class a 	object (self)
		method call_pipo (x:b) = x#pipo (self : b #ta :> b ta)
	end
	 and b 	object
		method pipo (x:a):a = x
	end;;

class a : object method call_pipo : b -> b ta end
class b : object method pipo : b ta -> b ta end


En tout cas, voilà qui fût un problème fort intéressant dont l'exploration
m'a amené (je pense !) à comprendre plus complètement ces questions.


-- Christian