Re: [Caml-list] Future of labels, and ideas for library labelling

[Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp>]

From: Judicael Courant <Judicael.Courant@lri.fr>

> > [ Disclaimer: you can safely skip this message if you are not
> >   interested in labels. It is about modalities of use for people who
> >   want them. ]

> > So, is there no way out?
> > Not completely, if we accept to start from strict unification:
> [...]
> 
> I can not really assess if this solution is good. However, it sounds to
> me like a hack. I am rather suspicious of hack, be they clever as long
> as they are not proven harmless (through a metatheoretical study). What
> are the chances then that we experience bad behaviours of this hack
> because of a lack of good theoretical properties?

Just in case I confused anybody, this idea of allowing to omit some
labels is an extension of the label mode, not the classic mode. As I
explained, the classic mode itself is currently a terrible hack, and
trying to extend it is bound to fail.

For this idea, the reason it is more than  a hack is that it can be
proved unambiguous:
* the application is complete, and typing would fail otherwise
* ocaml's label mode does not allow unification between differently
  ordered function types, so that positional application is
  unambiguous
* this is of course coherent with the unlabeled case

So, you can see it as an overloading hack, but you can also build a
metatheory for it. There are even ways to make this typing
principal...

The only weakness is that it is not compatible with unification of
differently ordered function types, but this was removed from ocaml as
non conform to call-by-value semantics.

Jacques Garrigue
-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives: http://caml.inria.fr