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

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

[-- Attachment #1: Type: text/plain, Size: 4762 bytes --]

Today the only time where you see '_a is for variable that did not get
generalized, and as a output of the type inference, never as input. But it
would be consistent to extend their meaning to flexible variables anywhere,
regardless of whether they'll get generalized later.

Andreas' idea is to have '_a meaning "instantiate me with any suitable type
that makes this expression type-check" (including a freshly generalized
variable), and have 'a meaning instead "this type must remain a polymorphic
variable". The interpretation for '_a corresponds to the meaning it has
when printed by the type-checker today -- and the interpretation of 'a
would behave as the (type a) construct does today, minus possibly the
specific GADT interaction.

(One minor difference being that, today, the type-checker is not too
careful about respecting weak variable identity when printing them. The
weak variables appearing in the two phrases I've shown have the same name
'_a, when they in fact denote distinct flexible variables which occur in
the same scope.)




On Sun, Oct 27, 2013 at 3:43 PM, Yaron Minsky <yminsky@janestreet.com>wrote:

> But isn't this the exact opposite of Andreas' proposal?  He was
> proposing using '_a as a unification variable, which may very well be
> generalized.  It is exactly this use case for '_a that seems at odds
> with Andreas' proposal.
>
> y
>
> On Sun, Oct 27, 2013 at 10:28 AM, Gabriel Scherer
> <gabriel.scherer@gmail.com> wrote:
> >> > Note how OCaml already uses '_a for a sort of flexible variable in its
> >> > output.
> >> Where?
> >
> > '_a is used for type variables that cannot be generalized.
> >
> > # let x = ref None;;
> > val x : '_a option ref = {contents = None}
> > # let id x = x in id id;;
> > - : '_a -> '_a = <fun>
> >
> >
> >
> > On Sun, Oct 27, 2013 at 1:56 PM, Yaron Minsky <yminsky@janestreet.com>
> > wrote:
> >>
> >> On Sun, Oct 27, 2013 at 8:16 AM, Andreas Rossberg <rossberg@mpi-sws.org
> >
> >> wrote:
> >> > On Oct 25, 2013, at 22:32 , Yaron Minsky <yminsky@janestreet.com>
> wrote:
> >> >> Changing the semantics of this will, I think, break a _lot_ of code.
> >> >
> >> > Interesting. Do you have specific examples in mind?
> >>
> >> I know that I've seen many examples come up in my code.  One common
> >> use is to partially specify a type.  For example, if I wanted to
> >> ignore a return value that is a Tcp.Server.t from Async, I would
> >> probably write it like this:
> >>
> >>     (ignore server : ('a,'b) Tcp.Server.t)
> >>
> >> without specifying the sometimes rather complicated details of those
> >> types.  Similarly, if I were to ignore a Map, I might write
> >>
> >>     (ignore map : (int,string,'a) Map.t
> >>
> >> since it's not helpful here to specify the comparator type, which is
> >> what goes into the third slot here.
> >>
> >> Nowadays, I would probably use an underscore in these cases rather
> >> than an explicit type variable, but our codebase has plenty of old
> >> examples of this kind of thing.  If a change like the one you propose
> >> is changed, I presume that _ would keep its current meeting, which
> >> would address many use cases.
> >>
> >> Given the existence of such use-cases, I would hope that we could
> >> avoid making the change in a way that would non-optionally break lots
> >> of code.  If people agree this change should be made, perhaps it
> >> should be done in the mode of -strict-sequence.  That change was added
> >> as a flag, so users could take it at their own pace.
> >>
> >> >> For what it's worth, I suspect that most people who are surprised by
> >> >> this are people who were trained on Standard ML.  At Jane Street
> we've
> >> >> had a lot of people learn the language, and the complaints I've heard
> >> >> about this feature are, I think, mostly from that group.
> >> >
> >> > Maybe, but it's not my impression that this is true for most people I
> >> > see asking related questions here on the list or on SO.
> >>
> >> To be clear, my guess above is less than scientific.
> >>
> >> >> I also don't find Andreas suggestion particularly intuitive.  I would
> >> >> have guessed that (x: '_a) would constrain x to be a weakly
> >> >> polymorphic value, which is at odds with the proposal.
> >> >
> >> > Now, _that_ is something I would only expect from programmers trained
> on
> >> > SML -- ancient SML'90 to be precise. ;)
> >> >
> >> > Note how OCaml already uses '_a for a sort of flexible variable in its
> >> > output.
> >>
> >> Where?
> >>
> >> > /Andreas
> >> >
> >>
> >> --
> >> Caml-list mailing list.  Subscription management and archives:
> >> https://sympa.inria.fr/sympa/arc/caml-list
> >> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> >> Bug reports: http://caml.inria.fr/bin/caml-bugs
> >
> >
>

[-- Attachment #2: Type: text/html, Size: 6691 bytes --]