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/23, at 14:52, Gabriel Scherer wrote:

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

The point here is that the "type a b. ..." syntax is syntactic sugar.
Rather than putting efforts in making it "hygienic", at the cost of
mangling type variable names, isn't it simpler to define precisely
how it expands, and prohibit ambiguous types?
I would argue that this is actually simpler to explain it that way
(if you want to give an exact specification).

I have committed this in trunk and 4.00, and the output now is a syntax
error:

Error: In this scoped type, variable 'a is reserved for the local type a.

It is of course possible to make it a warning (by doing two passes and generating
fresh names), but I don't see the point: you can always choose your names so
that no conflict happens, so why risk the confusion?
A similar case occurs with value fields in classes: not only you cannot access them
from other value fields, but they actually hide external values.

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

Backward compatibility is of course a concern.
On the other hand, polymorphic methods are not used that often,
and problems only occur with code that is ambiguous to read.

For me the main problem is that it hides the fact those type variables
are really locally abstract types. And the idea behind using locally
abstract types was to avoid introducing yet another kind of type
variable.

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

This is certainly doable, but in my opinion it would not replace the
"type a b. ..." syntax, which is more readable.

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

Easy to do.
Actually I'm not sure why it wasn't defined that way to start with.
Not enough System F-ish?

Jacques Garrigue