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

> 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 agree that not having to deal with name shadowing makes the
macro-expansion explanation simpler. Furthermore, treating this as an
error instead of a warning also makes the implementation simpler,
which is a point in favor of your change.

I'm not totally convinced by the idea that "type a b . ..." won't
cause trouble to users because it is syntactic sugar:

1. To explain it directly as syntactic sugar, you have to explain the
users both the polymorphic recursion notation and the rigid variable
abstraction (type a) (is this a good name? I like "System F
quantification" and prefer to avoid mumbles like "variables that are
type constructors rather than type variables because of implementation
reasons"); that's reasonable if you're giving a lecture where you have
the opportunity to introduce new concepts in your preferred order and
at your pace, but may not be practical in the random context of
someone asking "hey, what is this (type a b . ...) code doing?". In
practice I expect most non-expert users to consider it as a new,
rather than derived, concept.

2. The syntax still suggests a semantic that is different from the
actual one (ie. that the variables are bound locally to the type
annotation), which could confuse users that don't even ask about it
but simply assume it works somehow as they expect.

I understand there are compromises at play here and am not too
dissatisfied with this syntax, but still if it could be made
unecessary by making the (type a) one scale to polymorphic recursion,
I think that would be even better.

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

In my opinion, errors should be for semantic errors, and warnings for
"things that look like mistakes but are actually meaningful". In
particular, errors are part of the language specification, while
warnings are not. Making this cosmetic choice of "discouraging
shadowing" an error makes it part of the semantic of the construct,
while leaving it as a warning give it equivalent visibility, but with
less urge to make sure that everyone really understands the situation.
I also believe making part of the language semantics makes it even
more difficult to get a clear and exhaustive mental model of the
status of type variables: we already have 'a, '_a and a, maybe we
don't also need non-uniform rules about when name conflicts and when
they don't.
(However, there is the argument that making this an error now leaves
the option open to degrade it into a warning, while the reverse
direction would break compatibility. I can understand the benefit
keeping it that way for a coming release, even if those decisions
usually have the unfortunate effect of keeping those warts with us
much longer than originally hoped.)

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

Indeed, instance values syntax is horrible -- I would be very
frustrated if they were actually used.
That's certainly not a good argument to introduce similar things, but
I think you're pessimistic and the present situation is not as bad --
or maybe I haven't understood it in its full glory yet.

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

Frankly, I don't think the extremely meager readability benefits
outweigh the need to explain yet another kind of type annotation to
the code readers. Compare:

  let rec length : type a b. (a,b) l -> 'a = function
  let rec length (type a b) : (a,b) l -> 'a = function

And that's in the defavorable case of "function" which is friendly to
function types annotations. In other situations you could replace the
relatively awkward
  : a b . foo -> bar -> baz = fun x y -> ....
by something like
  (type a b) (x : foo) (y : bar) : baz = ...
in the cases where it is more readable -- you don't need to emphasize
the whole function type.
(Assuming, always, that the type-checker can detect the polymorphism
for polymorphic recursion.)

On Fri, Mar 23, 2012 at 7:45 AM, Jacques Garrigue
<garrigue@math.nagoya-u.ac.jp> wrote:
> 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