Re: Proposal for Generic Extensions with Import Clauses

[Hubert Baumeister <hubert@mpi-sb.mpg.de>]

Dear Andrzej and Michel,

Andrzej Tarlecki wrote:
> 
> Dear Hubert,
> 
> We have just had another look at your proposal for generic extensions.
> 
> One issue arose: conservativity.
> 
> First, you do not mention what is the semantics of
> 
>         GEN-CONS-EXT ::= gen-cons-ext IMPORT? PARAMS SPEC+
> 
> We presume that the conservativity requirement applies here to the
> subsequent extensions of PARAMS (by SPEC+), right?

Yes, that seems to me the natural extension of the current semantics of
gen-cons-ext. In the current semantics the body extends the parameter
conservatively. In the new proposal the only difference is that the
parameter may be an extension of an optional import. But nothing is said
about whether this extension is conservative or not.

> 
> Another option would be to make this to apply also to the "first
> step", ie, to the extension of IMPORT by PARAMS. 

I see another possibility, where, regardless whether there is a
gen-cons-ext or a gen-extension, it is always required that parameter
and argument are conservative extensions of the import. This would fit
with the view that the import is a specification, which should not be
modified. Do you know of any examples, where one would like to modify
the import?

Of course, the option you propose below is more general.

> However, instead of
> proposing this, we suggest that perhaps we could consider a more
> general solution, where we might have two forms of import, indicating
> whether its further extension is required to be conservative or not.
> 
> Even though at least one of us (guess who) in general questions the
> necessity of the conservativity requirements in structured specs, this
> would seem uniform with the way conservativity may be imposed
> elsewhere in CASL.

I agree. Is there a way to express this similarity in the abstract
syntax? For example:

GEN-EXTENSION ::= gen-extension PARAMETER SPEC+
GEN-CONS-EXTN ::= gen-cons-extn PARAMETER SPEC+

PARAMETER ::= PARAMS | IMPORT-EXTENSION | IMPORT-CONS-EXTN
PARAMS ::= params SPEC+
IMPORT-EXTENSION ::= import-extension SPEC PARAMS
IMPORT-CONS-EXTN ::= import-cons-extn SPEC PARAMS

Greetings,
	Hubert