Re: [Caml-list] Funny name for a type variable in the output: should this be filed on the BTS?

[Roberto Di Cosmo <roberto@dicosmo.org>]

Dear Jacques,
     thanks for having looked into this issue and explaining its origin:
if I understand well, this comes from a combination of two mechanisms
 
 (1) the desugaring of type a b. (a,b) l -> 'a into 'a1 'b. ('a1,'b) l -> 'a 
     that introduces the 'a1
  
 (2) the fact that the output type strives to respect the type variable
     names used in the user code : this brings the 'a1 over to the
     output type

I think (2) is a useful feature: it may be hepful to see immediately
where a type variable comes from.

I would probably, as you did, point my finger at (1): the trouble seems
to come from the fact that we can intermix unquoted type variables and
quoted type variables in the same type.

One may have very legitimate reasons to want an 'a in the type 

 type a b. (a,b) l -> 'a 

but of course we do not expect a and 'a to be the same variable...

--Roberto



On Fri, Mar 23, 2012 at 07:12:52AM +0900, Jacques Garrigue wrote:
> On 2012/03/22, at 18:51, Roberto Di Cosmo wrote:
<snip>
> > type empty
> > type nonempty
> > 
> > type ('a, 'b) l =
> >     Nil : (empty, 'b) l
> >   | Cons : 'b * ('a, 'b) l -> (nonempty, 'b) l;;
> > 
<snip>
> > let rec length : type a b. (a,b) l -> 'a = function 
> >   | Nil -> 0 
> >   | (Cons (_,r)) -> 1+ (length r);;
> > 
<snip>
> > look at the output type
> > 
> >   val length : ('a1, 'b) l -> int = <fun>
> > 
<snip>
> > The type is perfectly sound... it is just 'surprising' for
> > a regular user... do you think this should be considered a bug?
> 
> Well, since there is no specification whatsoever about type variable names
> in the output, this is hard to call it a bug.
> On the other hand, you were surprised, so something is probably wrong.
> 
> After thinking a bit more about it, actually the problem is not in the printer,
> as everybody assumed, but in the parser.
> Namely, 
> 
> 	... : type a b. (a,b) l -> 'a = ...
> 
> is just syntactic sugar for
> 
> 	... : 'a1 'b. ('a1,'b) l -> 'a = fun (type a) (type b) -> (... : (a,b) l -> 'a)
> 
> Now you see where 'a1 appears: since there is already an 'a in the type,
> we cannot use 'a for the fresh abstract type a.
> 
> However, as you already mentioned, the original type itself was erroneous.
> So a better solution would be to get an error at that point.
> Namely, if the type annotation contains a type variable with the same name
> as one of the quantified types.
> Does it sound reasonable.
> 
> At times I wonder whether the "type a b. ...." syntax is the right approach.
> Another approach would be to change the meaning of
>   ... : 'a 'b. ('a,'b) l -> 'a = ...
> to have 'a and 'b defined in the right hand side.
> The trouble is that we still need the locally abstract types internally, so this
> could be confusing.
> Also this could break some existing programs using polymorphic methods.
> 
> 	Jacques Garrigue

-- 
--Roberto Di Cosmo
 
------------------------------------------------------------------
Professeur               En delegation a l'INRIA
PPS                      E-mail: roberto@dicosmo.org
Universite Paris Diderot WWW  : http://www.dicosmo.org
Case 7014                Tel  : ++33-(0)1-57 27 92 20
5, Rue Thomas Mann       
F-75205 Paris Cedex 13   Identica: http://identi.ca/rdicosmo
FRANCE.                  Twitter: http://twitter.com/rdicosmo
------------------------------------------------------------------
Attachments:
MIME accepted, Word deprecated
      http://www.gnu.org/philosophy/no-word-attachments.html
------------------------------------------------------------------
Office location:
 
Bureau 6C08 (6th floor)
175, rue du Chevaleret, XIII
Metro Chevaleret, ligne 6
------------------------------------------------------------------