parametrized specification issues: compound identifiers

[Don Sannella <dts@dcs.ed.ac.uk>]

This is a response to a specific point in Bernd's message and a
preceding one on the issue of compound identifiers.  Sorry that I have
not had time to react to all the other CoFI e-mail -- I'm simply
OVERWHELMED by other matters at the moment.  I hope to get back to
normal eventually and provide lots of messages of my own for all of
you to read and respond to :-)

In a message to cofi-language dated Mon, 7 Oct 1996 14:18:32, Bernd
writes:

> (1) compound identifiers are too close to parametrized types and
> polymorphic functions to be introduced as such; Don has also
> uncovered some severe problems based on his experience and
> apparently problems the Larch people had. We should drop them and
> perhaps think again about convenient renaming upon instantiation or
> the sharing issue in general.

He repeats this in his message of Mon, 21 Oct 1996 09:05:42, and Peter
responds:

> [Bernd, please clarify just what these problems in Larch are.  Jim
> Horning in his Oslo paper [LNCS 1130, p.64] refers to some problems
> that structured sort names did not solve, and suggests [ibid, p.68]
> that structured operator names might help; is that what you have in
> mind? --PDM]

Bernd is referring to something I mentioned in my comments on v0.92
and discussed with him on the telephone thereafter.  Sorry to Bernd
and everybody else if I wasn't clear enough.

Here is the relevant comment on v0.92 and Peter's response:

    Don> Hiding/exporting: If there is a compound sort like set(nat),
    Don> what happens when one hides just nat?  Or when one exports
    Don> just nat?  Can one hide/export just set?  (I guess not.)
    
    Peter>My understanding was that hiding nat would hide set(nat),
    Peter>but not vice versa.  Michel?

(BTW, I don't know what "vice versa" means exactly here.)
[That hiding set(nat) would not hide nat. --PDM]

Now concerning "severe problems based on [my] experience and
apparently problems the Larch people had": I can't point to an example
which shows that Peter's response is wrong.  But what it reminds me of
(and this is what I told Bernd on the telephone) is the semantics of
hiding in the first(?) version of LSL, years ago.  There, hiding a
type or function in a trait was a purely syntactic operation that
simply erased everything in the trait which mentioned that
type/function.  The problem with this is that then
	[[SP]]=[[SP']] =/=> [[hide f in SP]]=[[hide f in SP']]
where [[..]]  refers to the semantics of specifications.  Needless to
say (I hope), this is not a desirable feature.

LSL no longer has a hiding operation, and I read the following excerpt
from the above-mentioned paper by Jim Horning (p62) as a hint that
this problem with the proposed semantics is one reason for its removal:

    Reading specifications is important.  And people read syntactic
    objects (texts), rather than semantic objects (theories).  So we
    generally thought of LSL's combining operators as operators on
    specifications, producing new specifications, rather than as
    operators on theories or models, producing new theories or models.
    [...]
    We defined inclusion and parameterization as syntactic operations
    on (the text of) traits.  To us, this seemed easier to explain
    than operations on theories.  LSL's combining operations apply to
    simple, tangible objects; ...
    [...]
    Although we originally allowed hiding as one of our operators on
    traits, we eventually removed it from LSL.  "Hidden" operators
    cannot be completely hidden, since they must be read to understand
    the specification, and they are likely to appear in reasoning
    based on the specification.

(Before somebody suggests that we remove hiding/exporting: the
two-tiered-ness of Larch means that hiding on the LSL tier is not so
important: the way that LSL traits are used in interface language
specs means that the required hiding happens at that level.)

Summarizing: There is an unpleasant interaction between compound
identifiers and hiding/exporting.  There are possible pitfalls in
picking a solution out of a hat.  One way out is to forget about
compound identifiers, as Bernd suggests.  My own opinion is that this
is a frill that we can do without and that the onus is on people who
want this feature to be included to convince the rest of us that it is
important.

Best regards, Don