On architectural specifications

[pdmosses@brics.dk]

[This message is from an ordinary member of the Language Design Task
Group.  Kindly ignore the fact that the author happens to be the
moderator of the cofi-language mailing list and the overall CoFI
coordinator: all replies will be forwarded to the list uncensored!
--PDM]

It is with some trepidation that one approaches the topic of
architectural specifications, considering how strongly some of the
CoFI participants feel about the details...  But most of the other
controversial issues (subsorting, parametrization, compound
identifiers, cyclic library sections) seem to be settling down, and
time is running out, so there's no excuse for postponing it further!

Anyway, I've now written a small study-note on architectural
specifications [PDM-2].  It has been installed together with the other
Language Design Study Notes, and is available via the CoFI WWW pages,
both in HTML for browsing, URL:
http://www.brics.dk/Projects/CoFI/StudyNotes/Lang/PDM-2.html, and as
Postscript, URL:
ftp://ftp.brics.dk/pub/BRICS/Projects/CoFI/StudyNotes/Lang/PDM-2.ps.Z.

My original aim was merely to provide a few simple examples, showing
that one could at least specify some straightforward cases, not
involving sharing constraints on parameters.  But then I finally
understood (I hope!) the relationship between the higher-order
"pi-specification" approach (as advocated by Bernd Krieg-Brueckner,
Don Sannella, and Andrzej Tarlecki, on the basis of Extended ML and
SPECTRAL) and the first-order approach (advocated by Michel Bidoit, on
the basis of PLUSS, and described in his note on structuring
constructs).  This has resulted in a somewhat more ambitious note.

My note suggests that:

  what we already have in CoFI v0.93 is perfectly adequate 
  for expressing architectural specifications - even with 
  sharing constraints on the parameters!

(This was what Michel Bidoit was claiming all the time, but I never
really understood how it worked until I saw the examples.)

There is just one assumption: that implementations resulting from
applying functional modules always extend their parameters - any
hiding or renaming to be done is left to when implementations are
composed.  If you think that this is an unreasonable assumption, or
has unfortunate methodological or semantic implications, please react
(with examples of the problems); without it, I wouldn't know how to
proceed. 

The crux of the argument is simple: when an implementation extends two
parameter implementations, it must preserve both parameters, and this
can only be done when the common symbols of the parameter signatures
are interpreted identically.  Thus a functional specification such as
LIST >< SET -> RESULT, with LIST, SET, and RESULT all including ELEM,
can be interpreted as a class of functions on this restricted domain -
without involving names or dependent products at all.

The interpretation of LIST >< SET -> RESULT as *all* functions would
motivate the use of dependent products to express sharing.  This may
be needed in higher-order extension languages, but I don't see why it
should be needed for the main CoFI-language-still-without-a-name...

> Date: Fri, 11 Oct 1996 19:00:48 +0100
> From: bkb@Informatik.Uni-Bremen.DE (Bernd Krieg-Brueckner)
> 
> >> (2) I am still not sure I understand architectural specs. What seems to be
> >> missing though are names for the formal parameters of UNIT-FUN-SPECs such
> >> that they can be referred to in subsequent parameters. At the same time,
> >> the SPEC of a formal parameter must be able to refer to a previous
> >> parameter; this is what Pi-specs are about.
> >
> >It seems to me the mood at Munich (and later at Dagstuhl) was that one
> >would like full pi-specs in an extension language, but only a
> >restricted version of them in X.
> 
> I wonder; at least extension MUST be possible in a smooth way

I believe that it is - without using pi-specs at all!

> >> Consider the standard example:
> >>
> >>         UFS: (X: ELEM) -> (LX: LIST X) -> S X LX
> >
> >Please clarify what UFS is supposed to be (I couldn't match it to
> >anything in the study notes by you, Don, Andrzej).  My guess would be
> >that you are implementing lists by sets, but I don't know what S is.
> >Just refer me to the right page in the relevant note, if I simply
> >missed it.
> 
>          Set: (X: ELEM) -> (LX: LIST X) -> SET X = body (X, LX)
> 
> is more or less the example used in my previous notes (or some examples
> regarding Sort), where LIST and SET are parametrized structured specs,
> "coerced" here.

Then I think that might look something like this (in very ad hoc
notation):

 arc spec Set =
   decl X: ELEM
   decl LX:LIST[ELEM]
   decl F: ELEM >< LIST[ELEM] -> SET-AS-LIST[ELEM]
   compose F(X,LX){hiding List}
 end spec

or, avoiding names for implementations, perhaps:

  arc spec Set = 
    implement ELEM
    implement LIST[ELEM]
    (extend ELEM, LIST[ELEM] to SET-AS-LIST[ELEM]){hiding List}
  end spec

> Date: Tue, 15 Oct 1996 11:18:58 +0200
> From: Andrzej Tarlecki <tarlecki@mimuw.edu.pl>
> ...
> ARCHITECTURAL SPECIFICATIONS:
> 
> I think the way things are stated there now makes some sense, and
> allows some basic cases to be expressed as required.

Agreed!  :-)

> ****** WHAT FOLLOWS IS NOT A COMMENT DIRECTLY ON THE LANGUAGE SUMMARY,
> BUT YET ANOTHER ?DELICATE? ATTEMPT TO CHANGE IT TO WHAT I WOULD LIKE
> EVEN MORE, AS FOR EXAMPLE CALLED FOR BY BERND A FEW WEEKS AGO. SORRY,
> I CANNOT QUITE RESIST :-) IF YOU FEEL THIS IS NOT WORTH DISCUSSING
> ANY MORE, SKIP TO THE NEXT SEQUENCE OF FEW ASTERISKS...
> 
> If you read on here, let me state once more that the result only
> approaches my favourite solution, and I believe it does not allow the
> user to express some of the rather typical dependencies in the most
> natural way (see a simple example from Bernd's message last week ---
> has somebody undertaken to express something like this in the current
> X?).  

Sorry for the delay...

> Just to remind you: we (at least Don, Bernd and me) have been
> proposing from the very beginning that individual algebras (okay, we
> give up their explicit definitions from scratch, in form of some
> "abstract programs" or whatever they were called when they were voted
> out of the formalism) be present in X; currently they only sneaked in
> as names of units in architectural specifications.

Please see the discussion in the note concerning whether even these
names of units are needed...

Anyway, now you have in [PDM-2] my examples using the CoFI v0.93
constructs.  What I would like to see next [Bernd, I hope you agree!]
are some examples of architectural specifications that *cannot* be
expressed in a similar style.  Then we can assess how important it is
for CoFI to cater for those examples, and consider whether or not to
adopt Andrzej's proposal.  However:

> The idea is that
> 	alg-par-spec (SP1 ... SPn) BY-SPEC
> defines a function that takes algebras A1, ..., An in model classes
> of SP1, ..., SPn, respectively, and maps them to the class of all
> algebras that model
> 	extension (of-spec SP1 ... of-spec SPn) BY-SPEC
> and in addition expand A1, ..., An (I guess a semantics could be
> given without the use of extension and an explicit reference to
> reducts of the resulting models).

- it seems that also you are assuming that parameters always get
included in the results?

Looking forward to all the reactions - please send to
cofi-language@brics.dk,

Peter Mosses

P.S. Unfortunately Don, Andrzej, and Michel were all too busy this
week to react to a draft of [PDM-2], so I'm sending this now in the
hope that I haven't misunderstood too much from their previous notes...