Re: OCaml 2.0

[boos@arthur.u-strasbg.fr]

[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