Re: Syntax for label, NEW PROPOSAL

From: Frank Atanassow (franka@cs.uu.nl)
Date: Sat Mar 18 2000 - 22:07:33 MET

  • Next message: John Prevost: "Re: Syntax for label, NEW PROPOSAL"

    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
    



    This archive was generated by hypermail 2b29 : Tue Mar 21 2000 - 15:20:30 MET