Version française
Home     About     Download     Resources     Contact us    
Browse thread
[Caml-list] Future of labels
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Jacques Garrigue <garrigue@k...>
Subject: [Caml-list] Future of labels
Hello everybody,

A bit more than a year ago, we had a big "discussion" about presence
of labels in the standard library, and the existence of two modes
(classic and commuting labels).
The two modes were kept, but the number of labels were reduced.

Now that a more stable version was released, it may be time to assess
whether these choices were good, and what should be done in the
long-term.
As a minimum step, if the classic mode is to be kept, then its
semantics must be cleaned-up, because of the soundness problem I
exposed a few weeks ago, and also because its typing discipline is not
very well defined anyway.

Personally I see two possible directions.

(1) suppress the classic mode (and also labels in the standard library)
    advantages: now everybody can use commuting labels
    problems to solve:
      * need to provide alternative versions of some modules, were
        label mode users want to keep labels
        Not too difficult for the standard library itself, but what
        about other libraries. I particularly think of the Unix
        module, or user contributions that use labels.
      * what about people using "decorative labels", that is putting
        labels in the .mli files mainly, and only exceptionally in the
        implementation. i.e. real users of the classic mode.
      * transition for label mode users

(2) clean-up the classic mode
    This essentialy means giving a reduction semantics that matches
    more closely the typed behaviour. I give more details below.

Rather than getting immediately into a discussion about what is the
good solution (and this might be a 3rd one), it would be nice to now
really what people expect from labels.
In particular arguments for keeping a classic mode are:
* having labels in the standard library
* using decorative labels in one's own programs/interfaces
  (something people asked for before ocaml 3.00)
* allowing different styles depending on whether you care about
  commutation or not
* ...
Arguments for dumping it are:
* avoiding multiple styles
* desire for commutation, but do not want labels in the standard
  library
* ...

This would be nice if people could tell how they position themselves
on these, particularly if this is backed by experience.
Last year this discussion literally overflowed this mailing list, so
please speak in turn, and no need to repeat what the previous poster
said: this is not a vote, but a call for suggestions.

Personally, if there is no support for classic mode as it is, removing
it would simplify things. There are so few labels left in the standard
library that removing them would not be a big pain.  The problem of
other libraries, and particularly Unix, needs more work, but I would
think it could be solved, if in particular people are really ready to
write labels when they use 3rd party libraries.

Cheers,

Jacques Garrigue

P.S. Here are some possible rules for a better classic mode
(still 100% compatible with ocaml 2, and 99% compatible with the
current mode)

To keep the soundness, type annotations would have to intervene in
reductions. Before bashing about overloading, note that not inferred
types, but only syntactic type annotations are used, meaning that we
are still more or less working with an untyped semantics.

    (fun ~l:x -> e) ~l:v --> e[v/x]
    (fun ~l:x -> e) v    --> e[v/x]
    (fun ?l:x -> e) ~l:v --> e[Some v/x]
    (fun ?l:x -> e) e    --> (e[None/x]) e
    (f : l:t -> t') ~l:e  --> (f e : t')
    (f : ?l1:t1 -> ... ?ln:tn -> l:t -> t') e --> (f e : t')
    (f : ?l1:t1 -> ... ?ln:tn -> ?l:t -> t') ~l:e
       --> (f ~ln:e : ?l1:t1 -> ... ?ln:tn -> t')
    (f : ?l1:t1 -> ... ?ln:tn -> 'a) --> f

Advantage: we can now see at the semantic level that while
    (fun ~l:x -> e) ~l':e'
is not legal (stuck when l <> l'),
    let f ~l:x = e in (f : l':t -> t') ~l':e'
is legal (as it should be in classic mode, where different labels are
unifiable).
And of course this allows to discard optional arguments on the basis
of type information, solving the current soundness problem.

Problems:
 * this is a bit complex to understand in detail
 * type checking this relies on type information discrimination
   (but it should be added to the compiler anyway)
-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives: http://caml.inria.fr