[CoFI] Proposal for named morphisms in CASL

[pdmosses@brics.dk]

Please send comments on this proposal as soon as possible, and in any
case before the 

  DEADLINE: MONDAY 9 FEBRUARY 1998!

First, here is a reminder of the background for any proposal for
incorporating named morphisms in CASL (but please do not include it
it in follow-ups, as it is available via the CoFI web pages, URL
http://www.brics.dk/Projects/CoFI/Documents/CASL/RefereeResponse):

		     Response to the Referee Report on CASL
		     by The CoFI Language Design Task Group
				 27 August 1997
  
  3.1.4 Morphisms as First Class Citizens

  In CASL morphisms are 2nd class citizens, they can only be declared in some
  very specific contexts (e.g. within rename or derive declarations) and they
  cannot be named. We think that this is a bad design decision for several
  reasons:

    1. At the "meta-level" we believe that if the A of CASL should stand for
       "algebraic", the language should be built over all the concepts,
       constructions and philosophy that has made the algebraic approach
       especially powerful. In this sense, one of the basic ideas that makes
       the "algebraic" approach more powerful than the "axiomatic" or
       "logical" approach is the role of morphisms which, in the algebraic
       approach, are always considered at the same level of importance as
       objects.
    2. At the pragmatic level, the possibility of having morphism declarations
       (just as specification declarations) and of naming them has a number of
       advantages:
	  o It makes the language more concise since. For instance, several
	    instantiations of different parameterized specifications, where
	    the formal and actual parameter are the same can rely on one
	    morphism declaration. Also one may avoid the need of explicitly
	    defining a morphism when it may be built in terms of previously
	    declared existing ones (for instance, when the new morphism is the
	    composition of two already declared ones)
	  o explicit morphism declaration provides an additional level of
	    structuring increasing the readability of specifications.
       In this sense, having the possibility of explicitly declaring morphisms
       has been highly useful in a number of existing algebraic specification
       languages (e.g. the "view" declaration in OBJ) and in some existing
       tools (e.g. Specware).

  When this issue was discussed in the WG meeting it was said that this was
  left for the "extensions" part of CASL. We do not think this is reasonable.
  In particular, we think that CASL extensions should be based in adding to
  CASL new semantic features that enrich the language semantically, so that it
  can be considered adequate for specifying a specific class of systems for
  which plain CASL could be found inadequate. In this sense, intended
  extensions for dealing with persistent objects or concurrency or for dealing
  with higher-order functions seem adequate. However, enriching CASL with
  morphism declaration would not enrich the semantics of the language in any
  way nor it will make it especially adequate for any new application area.

  Response:

       The designers have asked those among them who most strongly favour
       allowing morphisms as first-class citizens to make a proposal for
       integrating these smoothly in the next version of CASL (see CoFI
       Note L-6).

The issue was on the agenda for the Language Design meeting in Amsterdam,
September 1997.  Here is the relevant extract from the minutes:

  CoFI LANGUAGE DESIGN Task Group Meeting
  Amsterdam, September 27, 1997
  ...
  II) Reconsideration of language design issues:

  * (5) Should naming of morphisms be allowed? See Note L-6, which
    also proposes changing the treatment of instantiation and sharing.

  DB presented the three levels of his proposal.  The meeting agreed to
  incorporate the first level in CASL, allowing morphisms to be named in
  libraries and used in instantiation of generic specifications.  The
  further levels were thought to be too radical (semantic and
  methodological aspects were discussed), and left to potential
  extensions of CASL. [DB is Didier Bert, the author of Note L-6.]

Believing that the absence of reactions to this decision indicated
that it was uncontroversial, I aired the following proposal for
abstract syntax and intended semantics after the Bremen meetings
(where there had unfortunately not been time to discuss the matter):

  To: Michel.Bidoit@lsv.ens-cachan.fr, 
	  dts@dcs.edinburgh.ac.uk, tarlecki@mimuw.edu.pl
  Subject: [CoFI] Arch spec and named morphisms - abstract syntax

  ... The semantics is intended to allow the insertion of a unique defined
  view between the PARAM and ARG specs, and the abbreviation of views by
  omitting SYMB-MAPs that are uniquely determined (e.g., when the larger
  spec only has one candidate op of a particular profile). ...
  I'm appending the relevant part of the (optimized) AS grammar for
  v0.99 ...  The `?'s indicate the parts concerned with views. ...
  Any help with this (still very tentative) part of the v0.99 abstract
  syntax would be much appreciated! ...

    SPEC-DEFN        ::=  spec-defn SPEC-NAME SPEC
    SPEC             ::=  BASIC-SPEC
  !                    |  translation SPEC RENAMING
		       |  reduction SPEC RESTRICTION 
		       |  union SPEC+
  !                    |  extension SPEC+
		       |  free-spec SPEC
		       |  local-spec SPEC SPEC
		       |  SPEC-NAME
		       |  gen-spec-inst GEN-SPEC-NAME FITTING-ARG+ SYMB-MAP*
  ...
    RENAMING         ::=  symb-maps SYMB-MAP+
  ?                    |  VIEW-NAME
    RESTRICTION      ::=  hiding SYMB+
		       |  revealing SYMB-OR-MAP+
  ?                    |  VIEW-NAME
    FITTING-ARG      ::=  fitting-spec SPEC SYMB-MAP*
  ?                    |  spec-view SPEC VIEW-NAME
  ?                    |  VIEW-NAME

  ? VIEW-DEFN        ::=  view-defn VIEW-NAME VIEW
  ? VIEW             ::=  view SPEC SPEC SYMB-MAP*

I'll forward the rather negative reactions that I received to that
(from Bernd and Andrzej) in a separate message, following up on this
one.  

Let me conclude this message by trying to relate the proposal a bit to
Didier's Note L-6 - assuming that you've read sections 1-3 of it,
which also give a succinct overview of the treatment of "views" in
OBJ, the primary source of inspiration for my proposal.

First of all, I believe that both the IFIP referees and Didier
generally use the word "morphism" to mean specification morphism
rather than signature morphism - especially when considering the use
of morphisms in connection with instantiation of generic
specifications.  This fits with the OBJ notion of "views" too.

Second, a common case of instantiation is when the generic parameter
is ELEM, = {sort Elem}.  If one uses the same actual parameter
(e.g. NAT) in several instantiations, it'd be very tedious to have to
mention "NAT fitting Elem |-> Nat" each time!  If one is allowed to
define a unique view from ELEM to NAT, it should be enough just to
mention NAT as the argument in an instantiation, or, if one has
several views from ELEM to NAT around (in the case that NAT has
several sorts), to mention NAT and the intended view - or simply just
the name of the defined view, which in turn mentions NAT.  This is
exactly the 2nd and 3rd alternatives for FITTING-ARG above, and
consistent, I believe, with what Didier proposed in Section 3.2 of L-6.

Note that I am not proposing to adopt the OBJ notion of "prinicipal
sort" of a spec, since this does not seem to be a useful notion for
CASL. 

Finally, the VIEW-NAME alternatives in RENAMING and RESTRICTION
correspond to the "target" and "source" constructs in Section 2.1 of
L-6. 

I make no claim to having a proper understanding of the semantics of
the proposed constructs (I assume that Didier does!).  But let's
discuss whether the above proposal, which corresponds roughly to the
"very basic framework" proposed in L-6, is what is WANTED or not, for
methodological reasons, perhaps clarifying the intended semantics at
the intuitive level, before considering whether the design and
semantics of the rest of CASL might force us to cut down to some even
weaker (or move to a simply different) proposal.

Have a nice weekend!

Peter

PS I intend to forward Bernd's and Andrzej's reactions later this
evening (so there shouldn't be any risk of that arriving first...)