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

[Gabriel Scherer <gabriel.scherer@gmail.com>]

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

I'd rather use a warning here. There are enough subtleties with (type
a b . foo) already, I possible I would be glad not to have to explain
different scoping rules from the rest of the language.

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

That would be quite strange. I already find it dubious that (type a b
. ....) would escape its natural scope, but our nice old type
variables had not been affected by those changes yet, and I think it's
better that they keep their natural meaning of local quantification.

Could we get the type-checker to understand that
    let rec length (type a) (type b) : (a, b) l -> _ = function ...
or let rec length (type a) (type b) (li : (a, b) l) = ...
is polymorphic enough to be a case of polymorphic recursion? This way
we could get rid of the (type a b . ....) syntax altogether have
clearer scoping rules.

(On my wishlist:   ... (type a) (type b) ... could be written ...
(type a b) ...)

On Thu, Mar 22, 2012 at 11:12 PM, Jacques Garrigue
<garrigue@math.nagoya-u.ac.jp> wrote:
> 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
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>