[CoFI] CASL v0.99 - Views (corrected version)

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

Dear Peter and Don,

just after I sent the previous mail and went for a bike ride, I
noticed that my mail contained some misunderstandings on my part.

So here is the corrected version.  [My comments are unchanged. --PDM]

Greetings,
	Hubert

Dear all,

I just checked the new design of views and tried to give it a
semantics, however, I have some problems to understand the intended
semantics of generic views.

[Right!  And as I wrote yesterday to cofi-semantics:
 "The syntax and semantics of views are still quite tentative, since the
  changes agreed in Lisbon had an impact on the way that generic views
  had been provided.  (The discussion of the detailed design better be
  on the cofi-language mailing list, I suppose.)"
 I must apologize personally for the vagueness in this revised part of
 the Summary, which indeed reflects some doubt about how the semantics
 should be.  I think the changes to the ordinary views worked out OK -
 now relying on signatures of specs instead of their names - but in
 Lisbon I hadn't realized how much this might complicate having views
 whose targets are generic.  Anyway, this is the essentially the only
 part of CASL v0.99 still open to discussion, and anyone should feel
 free to propose how best to deal with this issue!  Any changes needed
 in the syntax would surely be limited to one or two of the given
 productions for views, and not affect the rest of CASL at all. --PDM]

Given

view VN [SP1] ... [SPn] : SP to SP' = SM 

what is the relationship between SPi (1 <= i <= n), SP' and SP? Is SP'
intended to be an extension of the union of the SPi's? Then, the local
environment given to SP' is the union of the SPi's, similar to
generics?

Given an instantiation of a generic view

view VN [FA1] ... [FAn]

how are source and target specifications defined and what is the
symbol map of the resulting view? I would guess that SP' is viewed as
defining a generic specification with parameters the SPi's and as body
Sp'.  The source of the result of the instantiation of a generic view
is SP and the target is SP' instantiated by the FA1 ... FAn,
yielding the following diagram:

   sm'
 +------->SP'[SPa] <--- SPa
 |          ^            ^
 |      fm' |    po      | fm
 |   sm     |            |
 SP -----> SP' <------- SPp

where SPp is the union of the parameters SPi and SPa the union of the
corresponding argument specifications determined by FAi.

However, I would expect similar problems to those that led to the
introduction of imports to generic specifications, ie., instantiations
that should be pushouts are not pushouts.

On page 46 [Sect. 6.3.2] of the summary it reads:

"Generic views can also be implicitly instantiated: if there is a
unique definition of a generic view VN which for some instantiation
of its parameters is from SP to SP' ... "

This seems to imply that searching for a matching generic view requires 
guessing the appropriate arguments to the generic view?

It seems that the requirement, that the reduct of the models of the
target of a view are contained in the source, is not needed anymore,
since application of views only depend on the signatures of the
involved specifications and thus checking that the models of the
argument of an instantiation of a generic specification are contained
in the parameter has to be done regardless whether the fitting
argument is a view or not.

It is a pity that I haven't been to Lisbon and couldn't take part in
the discussions.  Maybe someone can summarize the discussions dealing
with views?

[In fact I'm still hoping to find time to send a brief summary of *all*
 the significant changes made since the draft of v0.99, but I may not
 manage it before I leave for a (10-day, net-less) trip early tomorrow.  
 I realize that this must make it difficult to understand the
 motivations for some of the changes - sorry!  --PDM] 

Thanks,
	Hubert