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

Dear Gabriel,

I agree with you on the basics.
But maybe not on the importance of syntax :-)

On 2012/03/23, at 19:25, Gabriel Scherer wrote:

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

Indeed, this understanding is basically fine.
You only need to understand that this is syntactic sugar when you want
to get back to the definition.

> 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 do not agree there.
There is a syntax to bind type variables to annotations, which is

   'a 'b. ....

We intentionally introduced a new syntax, close to the (type a) notation,
to make clear that the scope extends to the right.

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

I agree with the desire for minimality. But honestly, the notation

   let rec f (type a b) : a t -> a = ...

doesn't strike me as the right solution.
This problem with type annotations is congenital to ML, but for GADTs it
is essential to be able to write function types in an intuitive way.

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

I'm afraid there is no clear distinction between warning and errors.
I see at least 2 criteria.
* whether this is a question of programming style (then it can be a warning)
* whether this can be detected in a complete (then it can be an error)

To me the above is not a question of programming style, and can be detected
exhaustively, so it is more natural to have an error. But you are also right
that the definition requires to understand the syntactic sugar, which is not so
nice. On the other, we would have exactly the same problem with a warning.

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

This is indeed a strong reason. I am not really happy with the current
situation, so it is best to keep all avenues open.

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

Sorry, but I buy the first one anytime.
This makes clear that we are writing the type of length, while in the second
one we are writing the return type of some function. Probably fine for Coq
users, but not really user friendly.

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

Two problems here:
* this is even worse than before: variables and types are mingled in an
  utterly unreadable way. (I don't say that this should be prohibited, just
  that I don't think users should have to write things this way, which is
  unfortunately the ML way)
* we then need a specification of how much of the function is analyzed
  to determine the recursive type. Imagine when you mix that with optional
  arguments with defaults.

OK, this is a difficult problem, and I have no ideal solution.
Maybe we could support indeed your first syntax too:
	let rec length (type a b) : (a,b) l -> a = function

	Jacques