Re: [Caml-list] Equality between abstract type definitions

[Andreas Rossberg <rossberg@mpi-sws.org>]

On 10/25/2013 01:09 PM, Gabriel Scherer wrote:
> However, I think that the current syntax of implicitly-introduced
> variables with heuristically-defined scoping rules is bad in any case.
> My own toy experiment with explicit syntaxes always use an explicit
> binding syntax for both rigid and flexible variables (eg. "forall a b c
> in ..." and "some a b c in ..."). In this regard, the ('a 'b . ty) or
> (type a) syntaxes are definite improvements -- if only we had applied
> those explicit binding forms to GADT constructor types as well... So I
> think that even with Andreas' proposed change, people would still be
> surprised by things like the following:
>
>    let id : 'a -> 'a = fun x -> x
>
>    let dup (x : 'a) ('a * 'a) =
>      let result = (x, x) in
>      (id : 'a -> 'a) result  (* fails, while (id : 'b -> 'b) works *)

Yes, I agree that implicit scoping is a bit of an ugly hack. That said, 
I don't expect anybody to be truly surprised about the example above. At 
least I never heard this being an issue for SML programmers. People 
probably hardly ever write anything like the above, or avoid shadowing 
for clarity anyway.

/Andreas