No Subject

[Andrzej Tarlecki <tarlecki@mimuw.edu.pl>]

From: Till Mossakowski <till@Informatik.Uni-Bremen.DE>
To: cofi-methodology
Subject: Note on arc specs - comments

Dear Michel, Don, and Andrzej,

I have read your revised note on architectural specifications with great
pleasure - the examples make it much easier to follow the intuitions.

Here are my comments.

Contents:
- Implementations
- Instantiation with fitting morphisms (8.3)
- Generativity
- minor comment

Greetings,
Till

[ Thanks a lot for Till's prompt and careful reading. We have taken
the liberty to edit the message and provide our answers to Till's
comments, since we felt that a separate answer would be more difficult
to follow by the reader. All our comments are included into [], the
rest is Till's original message - Andrzej, Don and Michel ]


Implementations
---------------

Consider the implementation of sets as lists from
Peter's study note about arc specs (L-33)
(in slightly anachronistic notation):

spec LIST = enrich ELEM by
  sort List == nil | cons(Elem,List)
end spec

spec SET-AS-LIST = enrich LIST by
  opns empty:              -> List
       add:   Elem >< List -> List
       ...
  axioms empty = nil
         add(a,B) = ...cons(a,B)...
         ...
end spec

arc spec I-SET =
  decl L: LIST
  decl S: LIST -> SET-AS-LIST
  compose S(L){renaming List to Set}{hiding nil, cons}
end spec


I think this is a rather typical case of an implementation.
Now in many cases, the functor S realizing the implementation
can be defined independently of any programming language.
(Indeed, its specification is often just an extension by definitions.)
I think it is worth while to consider to have some means
of expressing the definition of S in a programming-language
independent way. This should be considered when designing
interfaces between CASL and particular programming languages.

A theoretical underpinning may be found in
M. Cerioli, E. Zucca: Implementation of derived programs
(almost) for free, 12th WADT, LNCS 1376, p.141-155.


[ No specific comment from our side on this, but: after a lot of
discussions during the early design of CASL, it has been decided that
there would be no "abstract programs" in CASL in any form. However,
the door is open to an extension of CASL with abstract programs,
possibly designed along the above lines, possibly in some other way :-)
AT + DS + MB ]

Instantiation with fitting morphisms (8.3)
------------------------------------------

I have to cite my comment to cofi-language from 9th April:

>In Lisbon, I proposed to have reductions along
>non-injective signature morphisms, because they
>may occur when there is the need to duplicate
>a component of a given unit (say, an implementation
>of natural numbers) and use it for two or more
>components of some generic unit (say, graphs
>with egdes and nodes, in order to obtain
>a graph of the successor function. Pairs of elem1 and elem2
>are another example, but here one could argue
>that it is better to have one separate specification
>for both elem1 and elem2).
>
>Now it seems that this possibility is already there.
>
>If I understand correctly, in the specification
>
>arch spec Graph_of_increasing_discrete_time =
>units
>  N:NAT 
>  Gr = lambda G:GRAPH . G
>result
>   Gr[NAT fit nodes |-> nat, edges |-> nat, 
>              source |-> id, target |-> succ]
>end
>
>the symbols nodes, edges, source and target have to occur in GRAPH, 
>whereas nat, id and succ have to occur in NAT.
>That is, NAT is reduced along the symbol map to GRAPH,
>and thereby the nat-component of NAT is duplicated
>and used for both the nodes component and the egdes
>component of the resulting UNIT-TERM.
>(Practically, one might argue that GRAPH is too loose
>to be implemented meaningfully in this way, but then
>consider an extension of graph stating some more
>properties of the graph of "increasing discrete time".)
>
>If I have misunderstood the paragraph on Unit
>Applications, then please formulate it more
>precisely. And in this case, I would still
>vote for allowing non-injective signature morphisms
>in UNIT-REDUCTIONs.
>I.e. the symbols right to |-> must be all distinct,
>while those left to |-> need not to be.
>This has a straightforward semantics: namely form
>the signature morphism mapping each symbol right
>to |-> to the corresponding symbol left to |->,
>and take the reduct along it.
>For uniformity reasons, the same should hold
>also for REDUCTIONs in structured specs.

OK. After reading section 8.3 of the arc spec note,
I see that I have misunderstood the paragraph in the
language summary.
So I would still vote for allowing non-injective signature 
morphisms in UNIT-REDUCTIONs to be able to cover examples
as above. Another example is the application of a generic
implementation of pairs to natural numbers.

spec Elem1 = sort elem1 end
spec Elem2 = sort elem2 end
spec Pair [Elem1] [Elem2] = 
     type pair[elem1,elem2] ::= make_pair(elem1,elem2) end

arc spec NatPair =
units N:Nat
      P:Elem1 * Elem2 -> Pair [Elem1] [Elem2]
result P [N fit elem1 |-> nat] [N fit elem2 |-> nat]
end

This seems to be ruled out now.

[ *** start of AT + DS + MB answer here ***

No, the above example is correct and works as expected according to the
current design of arch specs in CASL. In the "explicit form" it would be

{P [N reveal nat |-> elem1] [N reveal nat |-> elem2]
	with elem1 |-> nat, elem2 |-> nat} and N

and everything here works as expected.

Note, however, that things become a bit more awkward if we change the
above example into:

spec ElemS = Elem1 and Elem2
spec Pair [ElemS] = type pair[elem1,elem2] ::= make_pair(elem1,elem2) end

arch spec NatPair'=
units N:Nat
      P: ElemS -> Pair [ElemS]
result P [ N fit elem1 |-> nat, elem2 |-> nat ]

The above is correct (fitting morphisms are not required to be injective),
but the equivalence with the "explicit form" is a bit more awkward, since
the explicit form to be considered is:

{P [ { N reveal nat |-> elem1 } and { N reveal nat |-> elem2 } ]
   with elem1 |-> nat, elem2 |-> nat}
and N

(rather than perhaps more immediate from our text:

{P [ N reveal nat |-> elem1, nat |-> elem2 ]
   with elem1 |-> nat, elem2 |-> nat}
and N

which indeed is ill-formed according to what reveal can be --- sorry
about not being careful enough in the note.)

An alternative would be to indeed allow for reductions along
("against":-) non-injective signature morphisms, and use it here. Even
if we choose reducts with non-injective signature morphisms to be
used in the semantics (rather than our above explanation with
"name-by-name" reducts amalgamated later), we suggest it stays just
there --- in the semantics, with no need for an extra new construct
that would break the pleasing symmetry between structured specs and
unit constructs. In fact, the semantics is likely to do things
explicitly for this case, rather than referring to simpler constructs
anyway.

Of course, in this way we do not provide the possibility of expressing
reduction along non-injective signature morphisms --- but this was a
decision taken a while ago uniformly for structured specifications and
unit terms.

 *** end of AT + DS + MB answer here *** ]

Generativity
------------

On page 14, you write:

>For instance, functors (generic modules) in
>Standard ML have such a ``generative'' semantics: each time a functor
>is instantiated to an argument, the new types it builds are generated
>anew and are kept distinct from those built by other instantiations,
>even if the arguments were the same each time. A similar phenomenon occurs
>with Ada generic packages.
>
>Therefore, for safety, we will assume that new symbols introduced by a
>generic unit are not shared between its instantiations, even when
>its arguments are the same in each case. Auxiliary
>unit definitions may be used in CASL
>to avoid repetition of unit instantiation.

Perhaps you should add that CASL arc specs nevertheless work also
with programming language module systems with an applicative
instead of generative behaviour.

[ This observation is correct, and that is why we say "for safety".
Maybe this needs to be clarified in the text.  The assumption of
generativity doesn't invalidate the use of arch specs for applicative
module systems, just makes their use marginally more awkward than if
we had assumed applicativity instead.  The opposite (assuming
applicativity) would however invalid their use for generative module
systems.   AT + DS + MB ]

To make my next point clear, I cite some paragraphs of the thesis (p.13f.)
of Jun Liu who did his PhD in Bremen.

>In SML, structures are transparent; signatures ascribed to structures do 
>not hide the representations used in the structures. Sort abstratction,
>called type abstraction in SML, is achieved via the generativity of
>datatype declarations. (...)
>
>Functors in SML are also generative: each time a functor application
>is elaborated, it gives rise to a structure with a unique identity.
>This implies that F(N) =/= F(N) for any two occurrences of the same
>functor application. Hence, a functor application must be assigned
>to a structure name, for example, by writing
>
>	structure S = F(N)
>	
>before we can refer to its components via the structure name S.
>For the same reasons, functors cannot be applied to functor applications;
>we shall write G(S) instead of G(F(N)).

So it seems that SML forbides nested applications because
they suggest an applicative behaviour. Does the same argument
hold for CASL architectural specs, since their sharing properties
also follow the generativity principle?

[ We don't understand the above quotation: SML definitely doesn't
forbid nested applications.  Perhaps the author is speaking about some
non-standard version of ML of his own that he is studying in the
thesis?  CASL doesn't forbid nested applications either, but of course
the user has to take care of the sharing rules, which often might lead
to intermediate "let" or unit definitions, at least in the non-unary
cases.   AT + DS + MB ]

Jun Liu continues:

>Generativity is implemented in the SML type system by a means of a
>complicated, non-declarative, and hard to reason about mechanism
>that uses so-called stamps [66]. The generativity of datatype
>declaration serves as a core-level abstraction mechanism in SML.
>Understanding sort abstraction in this way is a too operational
>point of view. In some recent developments of SML-style module
>systems, generativity is stopped being considered as a key notion:
>in R. Harper and M. Lillibridge's system [28], there is no such notion,
>and in Leroy's system [52], the generative behaviour of functors
>is replaced by an applicative one.
>The generativity of modules is only important for structure-sharing
>constraints, an SML feature similar to type-sharing constraints
>that allows requiring that two modules are identical; because of
>the generativity of program modules, the test for module equality
>is not whether two modules contain the same components, which is
>in general undecidable, but whether they were created from the same
>elaboration step, which is decidable. Structure-sharing constraints
>are not considered to be very useful and recent proposals for a
>new version of SML [30,76] suggest dropping them from the language.
>
>[28] R. Harper and M. Lillibridge. A type-theoretic approach to
>     higher-order modules with sharing. 21st POPL, 123-137, 1994.
>[30] R. Harper and C. Stone. A type theoretic account of 
>     standard ML 1996. Technical report CUM-CS-96-136R, Carnegie
>     Mellon University, 1996.
>[52] X. Leroy. Higher-order functors with transparent signatures.
>     22nd POPL, p. 142-153, 1995.
>[66] R. Milner, M. Tofte and R. Harper. The definition of standard ML.
>     MIT Press, 1990.
>[76] A. Patal and C. Stone. Minutes of the ML2000 meeting at
>     King's Beach (unpublished), August 1996.

This sounds to me as that generativity is not a feature with a great
future (though admittedly, there are not many programming languages
supporting genericity at all).
Perhaps a future version of CASL should me more liberal wrt sharing?
 
[ There is indeed a possibility for more flexibility w.r.t. sharing,
but we think the current design is sophisticated enough and usable
enough. The fact that CASL is less permissive than some (either
existing or yet to be defined) programming languages does not seem to
be a problem --- whatever can be correctly developed in CASL will work 
correctly in these languages as well, as mentioned above.  Don can't
resist advertising his student Claudio Russo's very recent Ph.D.
thesis "Types For Modules", see
	http://www.dcs.ed.ac.uk/lfcsreps/EXPORT/98/ECS-LFCS-98-389
which is required reading for anybody who is interested in ML-style
module systems.    AT + DS + MB ]

Minor comments
--------------

On p. 17, line 2, you assume some notion of well-formedness in
context \gamma. I tried to trace it back and found it a bit
confusing that in the second paragraph of p. 16, well-formedness
is informally defined wrt some context, and in the last paragraph
of p.16, contexts are introduced again and named \gamma.
It would have helped me to find a \gamma and/or and italicized
"context" already in the second paragraph of page 16.

p. 24, l.-12
combinedto ==> combined to

[ Thanks for the careful reading. We will change as appropriate in the
next release of the note. AT + DS + MB ]