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

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2012/03/22, at 18:51, Roberto Di Cosmo wrote:

> I was playing around some more with GADTs, preparing my next course
> on functional programming, and came across an example on
> which the type checker outputs a type containing a funny name
> for a type variable. 

Dear Roberto,

Thanks for testing the new features.
There certainly are some rough edges left.

> I do not know if this qualifies as a bug, so before filing it, I'd
> love some feedback.
> 
> Here we are: I am writing an example to show how one can code
> a well typed length function for empty/nonempty list; we start
> with the type definition
> 
> type empty
> type nonempty
> 
> type ('a, 'b) l =
>     Nil : (empty, 'b) l
>   | Cons : 'b * ('a, 'b) l -> (nonempty, 'b) l;;
> 
> then we move on to the length function
> 
> let rec length : type a b. (a,b) l -> 'a = function 
>   | Nil -> 0 
>   | (Cons (_,r)) -> 1+ (length r);;
> 
> Hey, you say, the natural type to declare for length should be
> 
>   type a b. (a,b) l -> int
> 
> but as you see, for some mysterious reason I ended
> up writing something silly (dont ask why, I am just
> very well known to step on strange bugs as easily
> as I breath)
> 
>   type a b. (a,b) l -> 'a
> 
> The type checker is happy anyway: 'a will be instantiated
> to int, and the declaration of length is accepted... but now
> look at the output type
> 
>   val length : ('a1, 'b) l -> int = <fun>
> 
> Why do we get 'a1, and not 'a, in the type?
> 
> Well, probably, since 'a is instantiated to int during
> type checking, it may be the case that 'a, as type name, is
> still marked as taken during the type output, so we get ('a1,'b)
> 
> 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