Re: Syntax for label, NEW PROPOSAL

[Frank Atanassow <franka@cs.uu.nl>]

Damien Doligez writes:
 > I agree, and I would even go further.  I think the current labeling of
 > the standard library is way too verbose.  "fun" should not be "func"
 > or even "fn", but simply "f".  That's the usual name for a generic
 > function.  Likewise, we should replace char:char with c:char and so
 > on (maybe even the predicate function in List.for_all should be
 > labeled f).

If you hold that the point of labels is to provide extra "type checking", then
naming labels according to the type they annotate is exactly the wrong way to
proceed. For example, if you have a function f : char -> char -> t, you would
want to disambiguate the role of the two characters, since the type checker
cannot catch it, but using the generic label name 'c' will not help you here.

By that token, a convention for picking label names should distinguish
arguments according to their "role" (some semantics above and beyond what can
be expressed with the type system), not their type.

BTW, this thought just occurred to me regarding semantics: you might view
labels as a class of unary type constructors which are the identity on
types. This implies you would write:

  val pow : int Base -> int Exp -> int

The capitalization distinguishes these "identity" constructors from abstract
and primitive ones.

To define pow, you restrict the argument patterns explicitly:

  let pow (b:'a Base) (e:'a Exp) = ...

To use pow, we can either restrict the argument types explicitly:

  pow (2:'a Base) (3:'a Exp)

or rely on type inference. Of course, this doesn't address the issue of
reordering (IMHO the idea of reordering is a little dubious, esp. considering
the interaction with side-effects) and having to insert the type variables is
ugly, but at least it provides some documentation and a less ad hoc approach
to the syntax. Anyway, it's only the germ of an idea.

Another idea is to stipulate a class of kinds (in the sense of "type of a
type") of labels, and distinguish the syntax for kind restriction of values,
say term :: kind (bad choice, I know) from the syntax for type restriction for
values, term : type. However, kind restriction of types is still written
":". Then you write something like:

  val pow : int : base -> int : exp -> int
  let pow (b :: base) (e :: exp) = ..
  pow (b :: base) (e :: exp)

Also you must demand that every label kind is a subkind of the kind Type so
that, for example, (->) can operate on labelled types.

Does this make sense? I'm a little too tired to think very clearly... One
thing I don't like about this is that the label names don't get declared
anywhere, they just seem spring into existence. I guess you could insist that
they get declared somewhere with a new syntactic construct, but I don't see
much point in it.

-- 
Frank Atanassow, Dept. of Computer Science, Utrecht University
Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands
Tel +31 (030) 253-1012, Fax +31 (030) 251-3791